这是示例:
x = y + 1;
y = y - 2;
{y < 3}
这个例子最弱的前提是什么?
我想也许 y < 3 是一个答案。
如果没有,你能详细告诉我为什么吗?
这是示例:
x = y + 1;
y = y - 2;
{y < 3}
这个例子最弱的前提是什么?
我想也许 y < 3 是一个答案。
如果没有,你能详细告诉我为什么吗?
这是我基于快速阅读谓词转换器语义的答案的第一次错误尝试
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识别我的语法中的错误,尤其是:=
vs=
因为这使得我更容易错误地分配方程式,这是我最初困惑的一部分。