for.mlw 1.43 KB
Newer Older
1
module M
2

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

6
(* for loop with invariant *)
7
let test1 () =
8 9
  let x = ref 0 in
  for i = 1 to 10 do
10
    invariant { x = i-1 }
11 12
    x := !x + 1
  done;
13
  assert { x = 10 }
14 15 16 17 18 19 20

(* we don't even enter *)
let test2 () =
  let x = ref 0 in
  for i = 2 to 1 do
    x := 1
  done;
21
  assert { x = 0 }
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

exception E

(* the body raises an exception (for sure)
   subtle: the invariant is required *)
let test3 () =
  { }
  for i = 1 to 10 do invariant { i >= 2 -> false }
    raise E
  done
  { false } | E -> { true }

(* the body may raise an exception *)
let test4 x =
  { }
  try
    for i = 0 to 10 do
      invariant { x < 0 or x >= i }
      if i = x then raise E
    done;
    False
  with E ->
    True
  end
  { result=True <-> 0 <= x <= 10 }

48 49 50 51 52
(* and now downto *)

let test1d () =
  let x = ref 11 in
  for i = 10 downto 1 do
53
    invariant { x = i+1 }
54 55
    x := !x - 1
  done;
56
  assert { x = 1 }
57 58 59 60 61 62

let test2d () =
  let x = ref 0 in
  for i = 1 downto 2 do
    x := 1
  done;
63
  assert { x = 0 }
64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83

let test3d () =
  { }
  for i = 10 downto 1 do invariant { i < 10 -> false }
    raise E
  done
  { false } | E -> { true }

let test4d x =
  { }
  try
    for i = 10 downto 0 do
      invariant { x > 10 or x <= i }
      if i = x then raise E
    done;
    False
  with E ->
    True
  end
  { result=True <-> 0 <= x <= 10 }
84

85 86
end

87 88 89 90 91
(*
Local Variables: 
compile-command: "unset LANG; make -C ../../.. bench/programs/good/for"
End: 
*)