使用Hoare规则来显示PRECONDITION意味着在一个简单的程序中使用POSTCONDITION(只有两个赋值)

Question

使用Hoare规则，我想表明我可以暗示

{x >= 0} --> {a + y = x} 

程序

// PRECONDITION
{x >= 0}
a = x; 
y = 0;
// POSTCONDITION
{a + y = x}

使用分配规则，我得到

// PRECONDITION
{x >= 0}
{x + 0 = x}   // assignment rule
a = x; 
{a + 0 = x}   // assignment rule
y = 0;
// POSTCONDITION
{a + y = x}

显示

{x >= 0} --> {a + y = x} 

因此，我需要在最后一步展示

{x >= 0} --> {x + 0 = x} 

我该如何证明这一点，或者我的证明中有什么错误？

Answer 1

您的推理是正确的。

为了正式证明一个含义，可以进行如下论证：

1. 假设先行词x >= 0
2. 通过加性恒等式，我们得到了x + 0 = x
3. 通过言外之意的介绍(从1和2(，我们得到了x >= 0 --> x + 0 = x