Как построить и обосновать цикл-инвариант, который позволяет показать частичную корректность - PullRequest
Новая
       62

Как построить и обосновать цикл-инвариант, который позволяет показать частичную корректность

0 голосов
/ 12 декабря 2018

Мне нужно построить и обосновать инвариант цикла с заданной спецификацией: 

{n > 0} P {q = | {j: a[j]=x and 0 <= j < n} |}

, где | A | - количество элементов множества A. Это означает, что q равно числу элементов из массива a , которые равны x .

код P указан как: 

{
int i = 0, q = 0;
while (i != n){
    if (a[i] == x)
        q = q + 1;
    i = i + 1;
}

Я знаю, что инвариант цикла должен быть истинным:

  • до начала цикла
  • перед каждой итерацией цикла
  • после завершения цикла

, но я понятия не имею, как мне найти правильный инвариант цикла, который позволил бы мне показать частичную корректность P впоследствии.Я уже пытался просмотреть каждую отдельную итерацию цикла и переменных для случайных n , x и a [0 ... n-1] , чтобы увидетькакие значения являются постоянными во время работы цикла, но это не помогло.

1 Ответ

0 голосов
/ 12 декабря 2018

Внимательно посмотрите на свой код.В начале, q равно 0, и оно увеличивается только тогда, когда вы найдете новые элементы, которые == x.Так что

q = | {j: a[j]=x and 0 <= j < i} |

является частью вашего инварианта.Обратите внимание, что в вашей спецификации у вас было < n вместо < i.Также обратите внимание, что при завершении цикла i == n.Так что это также будет действовать в начале.Это также будет правдой в любой момент: пока все хорошо.Что-то еще отсутствует?Да, мы также должны заявить, что

0 <= i <= n - потому что это описывает диапазон значений i (в противном случае i будет свободен выходить за пределы массива).

Isэто все?Да - нет другого состояния цикла, чтобы описать.Следовательно, ваш полный инвариант выглядит так:

q = | {j: a[j]=x and 0 <= j < i} | and 0 <= i <= n

При решении этих упражнений вы можете попробовать выполнить следующие 2 шага:

  • попытаться описать простым текстом, чтоАлгоритм продолжается: «Я перемещаю i от 0 до n-1, останавливаясь на n, и в каждый момент я сохраняю в q количество x, которое я нашел в массиве».Все переменные, включенные в цикл, должны быть упомянуты!.
  • переводит этот простой текст в математику, а также следит за тем, чтобы ваше постусловие отражалось в инварианте, обычно заменяя n на счетчик цикла (в этом случае i)

В качестве мысленного эксперимента попробуйте вместо этого написать инвариант с эквивалентным циклом (но итерируя от конца к началу): 

{
int i = n-1, q = 0;
while (i >= 0){
    if (a[i] == x)
        q = q + 1;
    i = i - 1;
}

Наведите курсор мыши для ответа (но сначала попытайтесь выяснить это).

...