exceptions.mlw 431 Bytes
Newer Older
1 2
module M

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

MARCHE Claude's avatar
MARCHE Claude committed
6 7 8 9
exception Break

let f (n : int) : int  =
  { true }
10
  let i = ref n in
MARCHE Claude's avatar
MARCHE Claude committed
11 12 13
  try
    while (!i > 0) do
      invariant { true }
14
      variant { !i }
MARCHE Claude's avatar
MARCHE Claude committed
15 16 17 18 19 20
      if (!i <= 10) then raise Break;
      i := !i - 1
    done
  with Break -> ()
  end;
  !i
21
  { result <= 10 }
22 23 24

end

25 26 27 28 29 30
(*
Local Variables:
compile-command: "unset LANG; make -C ../../.. bench/programs/good/exceptions"
End:
*)