Hoare Logic - поиск инварианта цикла - PullRequest
Новая
       52

Hoare Logic - поиск инварианта цикла

0 голосов
/ 13 октября 2018 
x := 0; 
y := 0; 
while (x < a) 
  x := x + 2; 
  y := y + 1;

Я хочу использовать Hoare Logic, чтобы показать, что: {True} Half {x = 2 ∗ y} В приведенных ниже вопросах (и ваших ответах) мы можем ссылаться на код цикла как Loop.

1. Приведите желаемое постусловие {x = 2 ∗ y}, что является подходящим инвариантом для цикла?

Я думаю, что инвариант должен быть просто желаемым постусловием x = 2y.Это правильно?

...