po.mlw 1.65 KB
 Jean-Christophe Filliâtre committed Dec 29, 2010 1 ``````module M `````` Jean-Christophe Filliâtre committed May 28, 2010 2 3 4 `````` (* Tests for proof obligations. *) `````` Andrei Paskevich committed Jun 24, 2010 5 ``````parameter x : ref int `````` Jean-Christophe Filliâtre committed May 28, 2010 6 `````` `````` Jean-Christophe Filliâtre committed Dec 29, 2010 7 `````` logic q int `````` Jean-Christophe Filliâtre committed May 28, 2010 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 `````` (* basic stuff: assignment, sequence and local variables *) let p1 () = { q(!x+1) } begin x := !x + 1 end { q(!x) } let p2 () = { q(7) } begin x := 3 + 4 end { q(!x) } let p3 () = {} begin x := !x + 1; x := !x + 2 end { !x = old(!x) + 3 } let p4 () = {} begin x := 7; x := 2 * !x end { !x = 14 } let p5 () = {} 3 + 4 { result = 7 } let p6 () = {} let a = 3 in a + 4 { result = 7 } let p7 () = {} 3 + (let a = 4 in a + a) { result = 11 } (* side effects in function arguments *) let p8 () = { q(!x+1) } 3 + begin x := !x + 1; !x end { q(!x) and result = old(!x) + 4 } (* evaluation order (argument first) *) let p9 () = {} begin x := 1; 1 end + begin x := 2; 1 end { result = 2 and !x = 2 } let p9a () = {} begin x := 1; 1 end + 1 { result = 2 and !x = 1 } (* function with a post-condition *) parameter fsucc : x:int -> { } int { result = x + 1 } let p10 () = {} fsucc 0 { result = 1 } let p11 () = {} (fsucc 0) + (fsucc 3) { result = 5 } let p11a () = {} let a = (fsucc 1) in a + a { result = 4 } (* function with a post-condition and side-effects *) parameter incrx : unit -> { } unit writes x { !x = old(!x) + 1 } let p12 () = { !x = 0 } incrx () { !x = 1 } let p13 () = {} begin incrx (); incrx () end { !x = old(!x) + 2 } let p13a () = {} incrx (incrx ()) { !x = old(!x) + 2 } (* function with side-effects, result and post-condition *) parameter incrx2 : unit -> { } int writes x { !x = old(!x) + 1 and result = !x } let p14 () = { !x = 0 } incrx2 () { result = 1 } `````` Jean-Christophe Filliâtre committed Dec 29, 2010 63 64 ``````end `````` Jean-Christophe Filliâtre committed May 28, 2010 65 66 67 68 69 ``````(* Local Variables: compile-command: "unset LANG; make -C ../../.. bench/programs/good/po" End: *)``````