booleans.mlw 1.21 KB
Newer Older
1 2 3 4 5 6 7 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 63 64 65 66 67

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

parameter x : int ref

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 () =
  { !x <> 0 }
  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
  { result = 1 -> !x <> 0 }

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

let test_not_1 () =
  { } 
  if not (!x = 0) then x := 0
  { !x = 0 }

let test_not_2 () =
  { !x <= 0 }
  while not (!x = 0) do invariant { !x <= 0 } incr x done
  { !x = 0 }

let test_all_1 () =
  { }
  (!x >= 0 && not (!x = 0) || !x >= 1)
  { result=True <-> !x>=1 }

(* from Cesar Munoz's CD3D *)

{
  logic d : int
}

parameter vx : int ref
parameter vy : int ref

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
 { result=1 -> !vx=0 and !vy=0 }


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