for.mlw 1.44 KB
Newer Older
1
module M
2

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

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