for.mlw 1.43 KB
 Jean-Christophe Filliâtre committed Dec 29, 2010 1 ``````module M `````` 2 `````` `````` Jean-Christophe Filliâtre committed Dec 30, 2010 3 4 5 ``````use import int.Int use import module stdlib.Ref `````` 6 ``````(* for loop with invariant *) `````` Jean-Christophe Filliâtre committed Oct 26, 2010 7 ``````let test1 () = `````` 8 9 `````` let x = ref 0 in for i = 1 to 10 do `````` Jean-Christophe Filliâtre committed Dec 30, 2010 10 `````` invariant { x = i-1 } `````` 11 12 `````` x := !x + 1 done; `````` Jean-Christophe Filliâtre committed Dec 30, 2010 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; `````` Jean-Christophe Filliâtre committed Dec 30, 2010 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 } `````` Jean-Christophe Filliâtre committed Oct 26, 2010 48 49 50 51 52 ``````(* and now downto *) let test1d () = let x = ref 11 in for i = 10 downto 1 do `````` Jean-Christophe Filliâtre committed Dec 30, 2010 53 `````` invariant { x = i+1 } `````` Jean-Christophe Filliâtre committed Oct 26, 2010 54 55 `````` x := !x - 1 done; `````` Jean-Christophe Filliâtre committed Dec 30, 2010 56 `````` assert { x = 1 } `````` Jean-Christophe Filliâtre committed Oct 26, 2010 57 58 59 60 61 62 `````` let test2d () = let x = ref 0 in for i = 1 downto 2 do x := 1 done; `````` Jean-Christophe Filliâtre committed Dec 30, 2010 63 `````` assert { x = 0 } `````` Jean-Christophe Filliâtre committed Oct 26, 2010 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 `````` `````` Jean-Christophe Filliâtre committed Dec 29, 2010 85 86 ``````end `````` 87 88 89 90 91 ``````(* Local Variables: compile-command: "unset LANG; make -C ../../.. bench/programs/good/for" End: *)``````