证明了算法的正确性

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; 的简写

所以这个程序基本上是一个if然后else。霍尔逻辑为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)}

你能完成???占位符吗？