test-pgm-jcf.mlw 1.29 KB
Newer Older
1
module M
2

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

6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27
parameter incr : x:ref int -> { } unit writes x { !x = old !x + 1 }

parameter x : ref int

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 }
28

29 30 31 32
let test_or_2 () =
  { }
  if !x = 0 || !x = 1 then !x else 1
  { 0 <= result <= 1 }
33

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

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

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

end

51 52 53 54 55 56 57 58
(*
Local Variables:
compile-command: "unset LANG; make -C ../../.. bench/programs/good/booleans"
End:
*)



59

60
(***
61 62 63
module TestArray

  use import int.Int
64
  use import module array.Array
65 66

  (* TODO: update *)
67 68
  let f (x: array int) =
    { x.length = 2 }
69 70
    x[0] <- 1;
    x[1] <- 2
71 72 73
    { x[1] = 2 and x.length = 2 }

end
74
***)
75

76
(*
77
Local Variables:
78
compile-command: "unset LANG; make -C .. testl-ide"
79
End:
80
*)