2

我想知道是否有人可以帮助我回答这个问题。它来自以前的试卷，我可以知道为今年考试准备的答案。

这个问题似乎很简单，以至于我完全迷失了，它到底在问什么？以下算法找到最大值是否正确？

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

答案必须基于算法最弱前提的计算。

你如何验证这一点？似乎很简单。

谢谢。

4

1 回答 1

2

这个问题似乎很简单，以至于我完全迷失了，它到底在问什么？

问题是要求您通过严格应用预先确定的一组规则来正式证明程序的行为符合规定（而不是阅读程序并说它显然有效）。

你如何验证这一点？

程序如下：

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)}

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

于 2014-04-27T11:35:56.413 回答