po.mlw 1.65 KB
Newer Older
1
module M
2 3 4

(* Tests for proof obligations. *)

5
parameter x : ref int
6

7
  logic q int
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 }

63 64
end

65 66 67 68 69
(*
Local Variables: 
compile-command: "unset LANG; make -C ../../.. bench/programs/good/po"
End: 
*)