Определить инвариант цикла?

Question

Я не совсем понимаю, как определить инвариант цикла. Я понимаю, что это то, что верно до цикла, после цикла и во время каждой итерации цикла, но это все. Вот примерная проблема, над которой я работаю, как бы вы нашли инвариант этого цикла?

i, temp : integer; 
values : array[1..100] of integer; 

x := 1; 

while x < 100 loop 

if values[x] > values[x+1] then begin 

temp := values[x]; 

 values[x] := values[x+1]; 

 values[x+1] := temp; 

 end if; 

 x := x + 1; 

end loop; 

Answer 1

1 <= x <= 100 является инвариантом цикла. Всегда верно до и после каждой повторения цикла.

Инвариант цикла должен быть истинным при входе в цикл и гарантированно оставаться истинным после каждой итерации цикла. Это означает, что при выходе из цикла могут быть гарантированы как инвариант цикла, так и условие завершения цикла.

См. Раздел логики Флойда-Хоара с простым примером цикла x<10: http://en.wikipedia.org/wiki/Loop_invariant

Answer 2

Проще говоря, инвариант цикла - это некоторый предикат (условие), который сохраняет значение true (true) для каждой итерации цикла.

В вашем случае инвариант цикла будет:

x >= 1 && x < 100

Учитывая условие завершения, приведенное выше выражение всегда будет оставаться true на протяжении всего цикла. Если это станет falseцикл заканчивается.

Answer 3

Вы определение цикла инварианта не совсем правильно. По сути, это должно быть верно только до и после каждого повторения цикла. У WikiPedia есть хорошее определение.

Инвариант этого цикла будет: the values[x] and values[x + 1] are maybe not sorted or x is the last index это верно до и после каждой итерации цикла. И это все еще верно сразу после цикла в сочетании с false для условия цикла:

i, temp : integer; 
values : array[1..100] of integer; 

x := 1; 

while x < 100 loop 
    // the values[x] and values[x + 1] are maybe not sorted or x is the last index - true
    if values[x] > values[x+1] then begin 
        temp := values[x]; 
        values[x] := values[x+1]; 
        values[x+1] := temp; 
    end if; 
    x := x + 1; 
    // the values[x] and values[x + 1] are maybe not sorted or x is the last index - true
end loop; 

// the values[x] and values[x + 1] are maybe not sorted or x is the last index - true
// and x >= 100 - true

естественно, инвариант цикла должен быть связан с телом цикла и задачей, которую он выполняет. Инвариант цикла гарантирует, что на каждом шаге цикла у вас есть одинаковые условия для выполнения тела цикла.