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

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} 

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

Page 148-160

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

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

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

Answer 1

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

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

Вы можете найти совершенно очевидный факт в книге, что

первый логический оператор над линией представляет , а затем; второй представляет еще статья.

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

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

, который приравнивает к

{n < 0} 

, который, в свою очередь удовлетворяет предусловий.

Заявление

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

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