Loop-инвариантное доказательство

Я столкнулся с проблемой, связанной с пост-условием и показывающей частичную правильность этой части кода.Loop-инвариантное доказательство

{ m = A ≥ 0 } 
    x:=0; odd:=1; sum:=1; 
    while sum<=m do 
    x:=x+1; odd:=odd+2; sum:=sum+odd 
    end while 
{ Postcondition }

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

x odd sum m (x + 1)^2 odd - x (odd - x)^2 
0 1 1 30 1   1  1 
1 3 4 30 4   2  4 
2 5 9 30 9   3  9 
3 7 16 30 16   4  16 
4 9 25 30 25   5  25 
5 11 36 30 36   6  36 

sum = (odd - x)^2

У меня есть, что исход из цикла является квадратом следующих м, но я не знаю, как написать это.

Как всегда, вся помощь приветствуется.

источник

2013-04-19 Ross Verry

Если вы видите, что последовательность сумм такой же, как последовательность совершенных квадратов, что вам еще нужно? Это состояние сообщения, которое вы ищете? Вам просто нужна помощь, доказывающая это или что-то еще? –

Ну, это то, что я имел в качестве исходного состояния, 'sum = (odd-x)^2'. Я понял это, потому что я не был уверен, что это должно быть частью инварианта цикла. Мне нужна помощь, подтверждающая это, но я не хочу, чтобы ответ был прямым. Я думаю, что у меня больше всего проблем, просто найти инвариант цикла. –

Я предпочитаю 'sum = (x + 1)^2', но они эквивалентны. Инвариант цикла, я бы предположил, индуктивный шаг в доказательстве того, что постусловие верно: другими словами, учитывая, что 'sum [n] = (x [n] +1)^2' для некоторого' n' , инвариант цикла состоит в том, что 'sum [n + 1] = (x [n + 1] +1)^2'. –

Петля инвариант:

odd = 2x+1 
sum = (x+1)^2

Доказательство:

Индукция база: тривиальная.

шаг Индукционная:

new_x = x+1 
new_odd = odd+2 = 2(x+1)+1 = 2*new_x+1 
new_sum = sum+new_odd = (x+1)^2+2(x+1)+1 = new_x^2+2*new_x+1 = (new_x+1)^2

источник

2013-04-20 05:28:17

Мне нужно пройти через этапы и доказать инвариант цикла true во всех трех шагах: Инициализация, сохранение и завершение. '{m = A ≥ 0} ⊃' '{m = A ≥ 0 ∧ 1 = 1 ∧ 1 = (1)^2}' 'x = 0'' {m = A ≥ 0 ∧ 1 = 2x + 1 ∧ 1 = (x + 1) 2} '' odd = 1' '{m = A ≥ 0 ∧ нечетное = 2x + 1 ∧ 1 = (x + 1) 2}' 'sum = 1'' {m = A ≥ 0 ∧ odd = 2x + 1 ∧ sum = (x + 1) 2} 'Это шаги для проверки инициализации, я думаю. –

ответ

Смежные вопросы