公理语义 - 如何计算最弱的前提条件

Question

示例如下：

x = y + 1;
y = y - 2;
{y < 3}

这个例子最弱的前提是什么？

我认为也许 y

如果不是，你能详细告诉我原因吗？

Answer 1

这是我基于快速阅读Predicate transformer semantics的第一次错误尝试

  WP( x := y + 1; y := y - 2, y < 3 )        # Initial problem
= WP( x := y + 1, WP( y := y - 2, y < 3 ) )  # Sequence rule
= WP( x := y + 1, y < 5 )                    # Assignment rule
= WP( x - 1 = y, y < 5 )                     # solve for y  <--- this is wrong!
= WP( x - 1 < 5 )                            # Assignment rule
= x < 6                                      # solve for x

但是正如Kris 指出的那样，因为x := y + 1 是对x 的赋值，这不会影响y，y 的最弱前提条件应该只是y < 5，所以正确答案应该是

  WP( x := y + 1; y := y - 2, y < 3 )         # Initial problem
= WP( x := y + 1, WP( y := y - 2, y < 3 ) )   # Sequence rule
= WP( x := y + 1, y < 5 )                     # Assignment rule
= y < 5                                      

还要感谢 philipxy 识别我的语法中的错误，尤其是 := 和 =，因为这让我更容易错误地分配方程式，这是我最初困惑的一部分。