1

我正在推理 Hoare Logic 的练习。

我应该找到满足三元组的所有布尔表达式B和所有程序S,假设 的评估不能修改存储,但执行可以修改它并改变 的值。P{true} if B then S; if B then P; {a >= 0}BSB

特别是,我不知道我能说什么a,因为它只存在于后置条件中,我从未找到过这样的例子。

谢谢你的帮助!

4

1 回答 1

0

(我之前的回答是错误的。)

这个问题有点开放式,因为有无限数量的表达式 ( B) 和程序 ( Sand P) 满足三元组。此外,三元组足够复杂,可以防止将任务简化为简单的通用答案。

基本上你可以把它分解如下:

  • 对于所有B为假的状态,a >= 0必须保持(否则整个三元组不能保持)
  • B对于是的州true,程序S; if B then P必须确保a >= 0
  • 这适用于所有人SB这样P......
    • 要么SB假的,要么a >= 0
    • 或者,S使B真实,并且...,

等等

于 2013-10-02T15:56:09.263 回答