证明算法的正确性

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-then-else。 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)}

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