proof - 使用 Hoare-Rules 显示 PRECONDITION 在一个简单的程序中意味着 POSTCONDITION（只有 2 个作业）

Question

使用霍尔规则我想表明我可以暗示

{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