证明以下是正确的。
{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分！
If you read carefully the book you will see that fule rule for selection statement looks like:
{B and P} S1 {Q}, {(not B) and P} S2 {Q}
--------------------------------------
{P} if B then S1 else S2 {Q}
You can find quite obvious fact in the book that
first logical statement above the line represents the then clause; the second represents the else clause.
So if you have only then section the rule changes to
{B and P} S {Q}, {not B and P} {Q}
--------------------------------------
{P} if B then S {Q}
It's very logic rule. You will reach sequence S if and only if B is true. So you can add it to the precondition statement.
In your case the inference rule looks like:
{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}
If we prove logical statements above the line we will prove statement below the line.
Statement
{n < 0 and n != 0} n = -n {n > 0}
can be proved by assignment axiom which can be found on page 150 in the book.
n = -n {n > 0}
We have to substitute n with n = -n in the postcondition. So we have
{-n > 0}
which equals to
{n < 0}
which in turn satisfies precondition.
Statement
{n >= 0 and n != 0} {n > 0}
obviously is correct too. Well, we've ensured that both statements above the line are correct so statement below the line correct as well.