let rec wp q = function | Skip -> q | Assume e -> exp_implies e q | Choice(s1, s2) -> let r1 = wp q s2 in let r2 = wp q s1 in exp_and r1 r2 | Seq(s1, s2) -> let r1 = wp q s2 in wp r1 s1 | Assign(t, e) -> Let(t, e, q) | Assert e -> exp_and e q
let calculate_wp (simp:Gcl.exp->Gcl.exp) (post:Gcl.exp) (stmt:Gcl.t) = let rec wp q s k = match s with | Skip -> k q | Assume e -> k (simp(exp_implies e q)) | Choice(s1, s2) -> wp q s1 (fun x -> wp q s2 (fun y -> k(simp(exp_and x y )))) | Seq(s1, s2) -> wp q s2 (fun x -> wp x s1 k) | Assign(t, e) -> k(simp(Let(t, e, q))) | Assert e -> k (simp(exp_and e q)) in wp post stmt (fun x->x)
wp q Seq(Skip,Seq(Assume expr1,Assert expr2)) (fun x -> x) (* Initial call to wp with arbitrary post-condition q *) wp q (Seq(Assume expr1,Assert expr2)) (fun x -> wp x Skip (fun x->x)) (* Grow the continuation because of the Seq *) wp q (Assert expr2) (fun x -> wp x (Assume expr1) (fun x -> wp x Skip (fun x->x))) (* Grow the continuation because of the Seq *) (fun x -> wp x (Assume expr1) (fun x -> wp x Skip (fun x->x))) (exp_and expr2 q) (* Shrink the continuation to process the assert *) wp (exp_and expr2 q) (Assume expr1) (fun x -> wp x Skip (fun x->x)) (* Process the assume *) (fun x -> wp x Skip (fun x->x)) (exp_implies expr1 (exp_and expr2 q)) (* Shrink the continuation to because of the assume *) wp (exp_implies expr1 (exp_and expr2 q)) Skip (fun x->x) (* Process the skip *) (fun x -> x) (exp_implies expr1 (exp_and expr2 q)) (* Shrink the continuation because of the skip *) (exp_implies expr1 (exp_and expr2 q)) (* Final WP *)
let rec wp q = function
let rec wp q s = match s with
There are 31,314 total registered users.
[+] expand
Printer Friendly ...
![[+] expand](/imagery/files/soysauce_blueprint.gif){kind=link}