loops.mlw 731 Bytes
Newer Older
1
module M
2

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

6 7
(** 1. A loop increasing [i] up to 10. *)

8
parameter i : ref int
9

10 11
let loop1 (u:unit) =
  { !i <= 10 }
12
  while !i < 10 do
13
    invariant { !i <= 10 } variant { 10 - !i }
14 15
    i := !i + 1
  done
16
  { !i = 10 }
17 18 19 20


(** 2. The same loop, followed by a function call. *)

21
parameter x: ref int
22

23
let negate (u:unit) = {} x := - !x { !x = - (old !x) }
24

25 26
let loop2 (u:unit) =
  { !x <= 10 }
27
  begin
28
    while !x < 10 do invariant { !x <= 10 } variant { 10 - !x }
29 30
      x := !x + 1
    done;
31
    assert { !x = 10 };
32
    if !x > 0 then (negate ());
33
    assert { !x = -10 }
34 35 36
  end
  {}

37
end
38 39

(*
40
Local Variables:
41
compile-command: "unset LANG; make -C ../../.. bench/programs/good/loops"
42
End:
43
*)