po.mlw 1.68 KB
Newer Older
1
module M
2

3 4 5
use import int.Int
use import module stdlib.Ref

6 7
(* Tests for proof obligations. *)

8
parameter x : ref int
9

10
  logic q int
11 12 13

(* basic stuff: assignment, sequence and local variables *)

14
let p1 () = { q (x+1) } begin x := !x + 1 end { q x }
15

16
let p2 () = { q 7 } begin x := 3 + 4 end { q x }
17

18
let p3 () = {} begin x := !x + 1; x := !x + 2 end { x = (old x) + 3 }
19

20
let p4 () = {} begin x := 7; x := 2 * !x end { x = 14 }
21 22 23 24 25 26 27 28 29 30

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 () = 
31
  { q (x+1) } 3 + begin x := !x + 1; !x end { q x and result = (old x) + 4 }
32 33 34 35

(* evaluation order (argument first) *)

let p9 () = 
36
  {} begin x := 1; 1 end + begin x := 2; 1 end { result = 2 and x = 2 }
37

38
let p9a () = {} begin x := 1; 1 end + 1 { result = 2 and x = 1 }
39 40 41 42 43 44 45 46 47 48 49 50 51

(* 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 *)

52
parameter incrx : unit -> { } unit writes x { x = (old x) + 1 }
53

54
let p12 () = { x = 0 } incrx () { x = 1 }
55

56
let p13 () = {} begin incrx (); incrx () end { x = (old x) + 2 }
57

58
let p13a () = {} incrx (incrx ()) { x = (old x) + 2 }
59 60 61

(* function with side-effects, result and post-condition *)

62
parameter incrx2 : unit -> { } int writes x { x = old x + 1 and result = x }
63

64
let p14 () = { x = 0 } incrx2 () { result = 1 }
65

66 67
end

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