Доказательство правильности алгоритма
Мне было интересно, если кто-нибудь может помочь мне ответить на этот вопрос. Это из предыдущей экзаменационной работы, и я смог узнать ответ, готовый к экзамену этого года.
Этот вопрос кажется настолько простым, что я полностью теряюсь, что именно он просит? Является ли следующий алгоритм, чтобы найти максимальное значение правильно?
{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 )}
Ответ должен быть основан на расчете самой слабой предпосылки для алгоритма.
Как вы это проверяете? Вроде все просто.
Благодарю.
2 ответа
Этот вопрос кажется настолько простым, что я полностью теряюсь, что именно он просит?
Вопрос состоит в том, чтобы вы формально доказали, что программа ведет себя так, как указано, путем строгого применения заранее определенного набора правил (в противоположность чтению программы и утверждению, что она, очевидно, работает).
Как вы это проверяете?
Программа выглядит следующим образом:
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)}
Можете ли вы завершить ???
заполнители?
@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)}