0
第9章在F* tutorial約最弱前置條件符號的問題有一個例子:一些在F *教程
b ::= x | true | false
e ::= b | let x = e1 in e2 | assert b | if b then e1 else e2
WP b P = P b
WP (let x = e1 in e2) P = WP e1 (fun x -> WP e2 P)
WP (assert b) P = b /\ P b
WP (if b then e1 else e2) P = (b ==> WP e1 P) /\ ((not b) ==> WP e2 P)
可能有人請解釋這裏的符號?我明白WP
是先決條件,P
後置條件,但是什麼是P b
?適用於b
的後續條件?從IRC頻道#fstar
你可以總結的討論?該格式使其難以閱讀。 –