公理語義 - 如何計算最弱的前提

Question

這裏是例子：

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

什麼是這個例子中的最弱前置條件？

我想也許y < 3是一個答案。

如果不是，你能詳細告訴我爲什麼嗎？

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用於識別我的語法錯誤，尤其是:= vs =，因爲這樣可以更容易地將方程的分配誤認爲是我最初混淆的一部分。