Логика Хоара

Question

Дайте доказательство правильности следующего.

{n != 0}    
if n<0 then 
n= -n 
{n>0} 

Следующее правило вывода должно помочь

{B and P} S {Q}, (not B) and P=>Q 
---------------------------------
{P}if B then S{Q} 

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

Стр. 148-160

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

Эти ссылки также могут быть полезны. Спасибо, 10 баллов!

http://en.wikipedia.org/wiki/Hoare_logic

Answer 1

Если вы внимательно прочитаете книгу, вы увидите, что правило fule для выражения выбора выглядит так:

{B and P} S1 {Q}, {(not B) and P} S2 {Q}
--------------------------------------
{P} if B then S1 else S2 {Q}

Вы можете найти довольно очевидный факт в книге, что

первое логическое утверждение над строкой представляет предложение then; второй представляет предложение else.

Так что если у вас есть только тогда, то правило меняется на

{B and P} S {Q}, {not B and P} {Q}
--------------------------------------
{P} if B then S {Q}

Это очень логичное правило. Вы достигнете последовательности S тогда и только тогда, когда B истинно. Таким образом, вы можете добавить его в предварительное условие.

В вашем случае правило вывода выглядит так:

{n < 0 and n != 0} n = -n {n > 0}, {n >= 0 and n != 0} {n > 0}
--------------------------------------------------------------
{n != 0} if n < 0 then n = -n {n > 0}

Если мы докажем логические утверждения выше линии, мы докажем утверждение ниже линии.

утверждение

{n < 0 and n != 0} n = -n {n > 0}

может быть доказано аксиомой назначения, которую можно найти на странице 150 в книге.

n = -n {n > 0}

Мы должны заменить n на n = -n в постусловии. Итак, мы имеем

{-n > 0}

что равно

{n < 0}

что в свою очередь удовлетворяет предварительному условию.

утверждение

{n >= 0 and n != 0} {n > 0}

очевидно, тоже правильно. Что ж, мы убедились, что оба оператора над строкой верны, поэтому оператор под строкой также корректен.