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

Question

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

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

 {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 )} 

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

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

Благодарю.

Answer 1

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

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

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

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

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

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

Таким образом, программа - в основном, если-тогда-еще. Логика Hoare предоставляет правило для конструкции 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)}

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

Answer 2

@Pascal Cuoq - Итак, во втором заполнителе я должен ввести ¬x > y && x > z? Это все доказательство? Наверное, мне нужно что-то еще? Не могли бы вы исправить мой ответ, если он не правильный?

P1 = if (y > x && y > z) max = y; else max = z;
{B ∧ P} S {Q}   ,   {¬B ∧ P } T {Q}
----------------------------------
   {P} if B then S else T {Q}

Instanciating the general if-then-else rule for the program at hand:

{x > y && x > z}  max = x;  {Q}    ,    {¬ (x > y && x > z)}  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)}