infinite-loop - 霍尔逻辑 | 当存在无限循环时，什么后置条件有效？

Question

我的老师告诉我以下语句是有效的： {x > 3} while true (x := 3) {x = 3}

为什么这个说法有效？是因为后置条件永远不会被检查，还是后置条件现在算作不变检查？

简而言之：当存在无限循环时，后置条件可以是任何东西吗？

那么这将是有效的： {x > 3} while true (x := 3) {x = 0}

Answer 1

无限循环可以有任何后置条件（包括像 1=0 这样的完全愚蠢的东西），而且它是空洞的。事实上，永远为假的后置条件是一种强制循环永远不会退出的方式。