booleans.mlw 1.26 KB
Newer Older
1
module M
2

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

6
parameter incr : x:ref int -> { } unit writes x { !x = old !x + 1 }
7

8
parameter x : ref int
9 10 11 12 13 14 15 16 17 18 19

parameter id_not_0 : x:int -> { x <> 0 } int { result = x }

parameter id : x:int -> { } int { result = x }

let test_and_1 () =
  { }
  if (incr x; !x > 0) && id !x = 1 then !x else 0+1
  { result = 1 }

let test_and_2 () =
20
  { !x <> 0 }
21 22 23 24 25 26
  if id_not_0 !x >= 1 && !x <= 1 then !x else 0+1
  { result = 1 }

let test_or_1 () =
  { }
  if (incr x; !x > 0) || !x < 0 then 1 else 2
27
  { result = 1 -> !x <> 0 }
28 29 30 31 32 33 34

let test_or_2 () =
  { }
  if !x = 0 || !x = 1 then !x else 1
  { 0 <= result <= 1 }

let test_not_1 () =
35
  { }
36
  if not (!x = 0) then x := 0
37
  { !x = 0 }
38 39

let test_not_2 () =
40 41 42
  { !x <= 0 }
  while not (!x = 0) do invariant { !x <= 0 } incr x done
  { !x = 0 }
43 44 45 46

let test_all_1 () =
  { }
  (!x >= 0 && not (!x = 0) || !x >= 1)
47
  { result=True <-> !x>=1 }
48 49 50 51 52

(* from Cesar Munoz's CD3D *)

  logic d : int

53 54
parameter vx : ref int
parameter vy : ref int
55 56 57 58 59 60

parameter sq : x:int -> {} int { result = x*x }

let test_cd3d () =
 { true }
 if !vx=0 && !vy=0 && sq !vx + sq !vy < sq d  then 1 else 2
61
 { result=1 -> !vx=0 and !vy=0 }
62

63
end
64 65

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