F *チュートリアル

Question

第9章で最弱事前条件の表記についていくつかの質問には例があります。

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から

Answer 1

ディスカッション：

20:33:49 - {AS}: let us say we have a program (let abs x = if x >= 0 then x else -x) 
20:33:58 - ollehar1: ok 
20:34:02 - {AS}: and we want to show that (fun res -> res >= 0) 
20:34:15 - {AS}: so we do 
20:34:26 - {AS}: WP (if x >= 0 then x else -x) (fun res -> res >= 0) 
20:34:28 - {AS}: right? 
20:34:32 - ollehar1: ok 
20:34:36 - {AS}: then we follow the calculations in the example 
20:34:42 - {AS}: so we apply the if-rule and get 
20:35:39 - {AS}: ((x >= 0) ==> WP x (fun res -> res >= 0)) /\ ((not b) ==> WP (- x) (fun res -> res >= 0)) 
20:35:55 - {AS}: here ==> is implication and /\ is and 
20:36:05 - ollehar1: yes 
20:36:07 - {AS}: conjunction 
20:36:17 - {AS}: so we carry on 
20:36:17 - ollehar1: but "not b" should be "not x >= 0" 
20:36:24 - {AS}: Yes, sorry :) 
20:36:39 - ollehar1: np 
20:36:43 - {AS}: not x is a basic value 
20:36:46 - {AS}: now* 
20:37:04 - {AS}: so WP x (fun res -> res >= 0) reduces to x >= 0 according to the rules 
20:37:14 - {AS}: and similarly with - x in the other side 
20:37:31 - {AS}: (they don't really have minus, so I just used the common intuition for that rule) 
20:38:05 - {AS}: so we end up with having ((x >= 0) ==> (x >= 0)) /\ (not (x >= 0) ==> (- x >= 0)) 
20:38:35 - {AS}: of course, if we simplify a bit the first conjunct is trivially true 
20:39:00 - {AS}: and if you have an integer arithmetic solver, you find out that the second is also true 
20:39:13 - {AS}: so the weakest precondition ends up being true