Chapter 9 in the F* tutorial has an example:
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)
Could someone please explain the notation here? I understand that WP
is pre-condition and P
post-condition, but what is P b
? Post-condition that is applied to b
?
Discussion from IRC channel #fstar: