Доказательство правильности алгоритма

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

Этот вопрос кажется настолько простым, что я полностью теряюсь, что именно он просит? Верен ли следующий алгоритм поиска максимального значения?

 {P: x≥0 ∧ y≥0 ∧ z≥0 } 
 if (x > y && x > z) 
 max = x; 
 else if (y > x && y > z) 
 max = y; 
 else 
 max = z; 
 {Q: max≥x ∧ max≥y ∧ max≥z ∧ ( max=x ∨ max=y ∨ max=z )}

Ответ должен быть основан на вычислении самого слабого предварительного условия для алгоритма.

Как вы это проверяете? Вроде просто.

Спасибо.


hoare-logic proof proof-of-correctness formal-methods post-conditions
person user2988649    schedule 27.04.2014    source источник
comment
Действительно, проверка программы является прямым применением логики Хоара (en.wikipedia.org/wiki/Hoare_logic). Что вы пробовали? Вы читали документы курса?   -  person Pascal Cuoq    schedule 27.04.2014
comment
Я сделал.. Я не знаю, как начать..   -  person user2988649    schedule 27.04.2014

Ответы (1)


arrow_upward
2
arrow_downward

Этот вопрос кажется настолько простым, что я полностью теряюсь, что именно он просит?

Вопрос заключается в том, чтобы вы формально доказали, что программа ведет себя так, как указано, путем строгого применения заранее определенного набора правил (в отличие от чтения программы и утверждения, что она явно работает).

Как вы это проверяете?

Программа выглядит следующим образом:

if (x > y && x > z) 
 max = x; 
else P1

с P1 сокращением для if (y > x && y > z) max = y; else max = z;

Таким образом, программа в основном представляет собой «если-то-иначе». Логика Хоара предоставляет правило для конструкции if-then-else:

{B ∧ P} S {Q}   ,   {¬B ∧ P } T {Q}
----------------------------------
   {P} if B then S else T {Q}

Экземпляр общего правила if-then-else для рассматриваемой программы:

{???}  max = x;  {Q}    ,    {???}  P1  {Q}
-------------------------------------------------------------------------------------
{true}  if (x > y && x > z) max = x; else P1  {Q: max≥x ∧ max≥y ∧ max≥z ∧ ( max=x ∨ max=y ∨ max=z)}

Можете ли вы заполнить ??? заполнителей?

person Pascal Cuoq    schedule 27.04.2014
comment
Должно быть: {x › y && x › z} max = x; {Q} , {y › x && y › z,max = z} P1 {Q} И как вычислить самое слабое предварительное условие? Спасибо за ваше время, Паскаль Куок! Я действительно наслаждаюсь этим .... - person user2988649; 27.04.2014
comment
@user2988649 user2988649 Да, вам придется доказывать {x > y && x > z} max = x; {Q} в левой части. В правой части вы допустили ошибку, когда применили ¬ к x > y && x > z. Результат не тот, что вы написали: ¬ (x > y && x > z) эквивалентно x <= y || x <= z. Самое слабое предусловие для программы и предоставленного постусловия — true. Я уже заполнил его, чтобы вам было проще. Следуя самому слабому предварительному условию, вы должны заполнить эту часть последней из того, что было заполнено в остальной части доказательства. - person Pascal Cuoq; 27.04.2014
comment
@user2988649 user2988649 Мы все еще пытаемся применить правило if-then-else к первому if на данный момент. Общее правило if-then-else гласит {¬B ∧ P } T {Q}. - person Pascal Cuoq; 27.04.2014