diff --git a/examples/add_list.mlw b/examples/add_list.mlw index 999c944049840d4ae81c75d0d06f45ecb73e6938..1accfd87aaf24c983955c43c80c57a88cae65917 100644 --- a/examples/add_list.mlw +++ b/examples/add_list.mlw @@ -59,30 +59,24 @@ module AddListImp use import SumList use import ref.Ref -exception Break - let sum (l: list or_integer_float) : (int, real) = returns { si, sf -> si = add_int l /\ sf = add_real l } let si = ref 0 in let sf = ref 0.0 in let ll = ref l in - try - while True do + while True do invariant { !si + add_int !ll = add_int l /\ - !sf +. add_real !ll = add_real l - } + !sf +. add_real !ll = add_real l } variant { !ll } match !ll with - | Nil -> raise Break + | Nil -> return (!si, !sf) | Cons (Integer n) t -> si := !si + n; ll := t | Cons (Real x) t -> sf := !sf +. x; ll := t end - done; - absurd - with Break -> (!si, !sf) - end + done; + absurd let main () = diff --git a/examples/binary_search.mlw b/examples/binary_search.mlw index 6d3ce8c7551ea6de4fdad172db16f9227b989de5..372a2346dab1a310a0e414aa26f0f59fce6b568e 100644 --- a/examples/binary_search.mlw +++ b/examples/binary_search.mlw @@ -11,34 +11,30 @@ module BinarySearch (* the code and its specification *) - exception Break int (* raised to exit the loop *) exception Not_found (* raised to signal a search failure *) let binary_search (a : array int) (v : int) : int requires { forall i1 i2 : int. 0 <= i1 <= i2 < length a -> a[i1] <= a[i2] } ensures { 0 <= result < length a /\ a[result] = v } raises { Not_found -> forall i:int. 0 <= i < length a -> a[i] <> v } - = try - let l = ref 0 in - let u = ref (length a - 1) in - while !l <= !u do - invariant { 0 <= !l /\ !u < length a } - invariant { - forall i : int. 0 <= i < length a -> a[i] = v -> !l <= i <= !u } - variant { !u - !l } - let m = !l + div (!u - !l) 2 in - assert { !l <= m <= !u }; - if a[m] < v then - l := m + 1 - else if a[m] > v then - u := m - 1 - else - raise (Break m) - done; - raise Not_found - with Break i -> - i - end + = + let l = ref 0 in + let u = ref (length a - 1) in + while !l <= !u do + invariant { 0 <= !l /\ !u < length a } + invariant { + forall i : int. 0 <= i < length a -> a[i] = v -> !l <= i <= !u } + variant { !u - !l } + let m = !l + div (!u - !l) 2 in + assert { !l <= m <= !u }; + if a[m] < v then + l := m + 1 + else if a[m] > v then + u := m - 1 + else + return m + done; + raise Not_found end @@ -51,7 +47,6 @@ module BinarySearchAnyMidPoint use import ref.Ref use import array.Array - exception Break int (* raised to exit the loop *) exception Not_found (* raised to signal a search failure *) val midpoint (l:int) (u:int) : int @@ -61,26 +56,23 @@ module BinarySearchAnyMidPoint requires { forall i1 i2 : int. 0 <= i1 <= i2 < length a -> a[i1] <= a[i2] } ensures { 0 <= result < length a /\ a[result] = v } raises { Not_found -> forall i:int. 0 <= i < length a -> a[i] <> v } - = try - let l = ref 0 in - let u = ref (length a - 1) in - while !l <= !u do - invariant { 0 <= !l /\ !u < length a } - invariant { - forall i : int. 0 <= i < length a -> a[i] = v -> !l <= i <= !u } - variant { !u - !l } - let m = midpoint !l !u in - if a[m] < v then - l := m + 1 - else if a[m] > v then - u := m - 1 - else - raise (Break m) - done; - raise Not_found - with Break i -> - i - end + = + let l = ref 0 in + let u = ref (length a - 1) in + while !l <= !u do + invariant { 0 <= !l /\ !u < length a } + invariant { + forall i : int. 0 <= i < length a -> a[i] = v -> !l <= i <= !u } + variant { !u - !l } + let m = midpoint !l !u in + if a[m] < v then + l := m + 1 + else if a[m] > v then + u := m - 1 + else + return m + done; + raise Not_found end @@ -95,7 +87,6 @@ module BinarySearchInt32 (* the code and its specification *) - exception Break int32 (* raised to exit the loop *) exception Not_found (* raised to signal a search failure *) let binary_search (a : array int32) (v : int32) : int32 @@ -104,27 +95,24 @@ module BinarySearchInt32 ensures { 0 <= to_int result < to_int a.length /\ a[to_int result] = v } raises { Not_found -> forall i:int. 0 <= i < to_int a.length -> a[i] <> v } - = try - let l = ref (of_int 0) in - let u = ref (length a - of_int 1) in - while !l <= !u do - invariant { 0 <= to_int !l /\ to_int !u < to_int a.length } - invariant { forall i : int. 0 <= i < to_int a.length -> - a[i] = v -> to_int !l <= i <= to_int !u } - variant { to_int !u - to_int !l } - let m = !l + (!u - !l) / of_int 2 in - assert { to_int !l <= to_int m <= to_int !u }; - if a[m] < v then - l := m + of_int 1 - else if a[m] > v then - u := m - of_int 1 - else - raise (Break m) - done; - raise Not_found - with Break i -> - i - end + = + let l = ref (of_int 0) in + let u = ref (length a - of_int 1) in + while !l <= !u do + invariant { 0 <= to_int !l /\ to_int !u < to_int a.length } + invariant { forall i : int. 0 <= i < to_int a.length -> + a[i] = v -> to_int !l <= i <= to_int !u } + variant { to_int !u - to_int !l } + let m = !l + (!u - !l) / of_int 2 in + assert { to_int !l <= to_int m <= to_int !u }; + if a[m] < v then + l := m + of_int 1 + else if a[m] > v then + u := m - of_int 1 + else + return m + done; + raise Not_found end diff --git a/examples/decrease1.mlw b/examples/decrease1.mlw index a6ca10d134d9ca2340cf2ce1fc400f0de6699a73..164c0a5bfeb1474646312f9b20838fd6b4840f1b 100644 --- a/examples/decrease1.mlw +++ b/examples/decrease1.mlw @@ -21,8 +21,6 @@ module Decrease1 variant { j - i } = if i < j then decrease1_induction a (i+1) j - exception Found - let search (a: array int) requires { decrease1 a } ensures { @@ -30,18 +28,14 @@ module Decrease1 \/ (0 <= result < length a /\ a[result] = 0 /\ forall j: int. 0 <= j < result -> a[j] <> 0) } = let i = ref 0 in - try - while !i < length a do - invariant { 0 <= !i } - invariant { forall j: int. 0 <= j < !i -> j < length a -> a[j] <> 0 } - variant { length a - !i } - if a[!i] = 0 then raise Found; - if a[!i] > 0 then i := !i + a[!i] else i := !i + 1 - done; - -1 - with Found -> - !i - end + while !i < length a do + invariant { 0 <= !i } + invariant { forall j: int. 0 <= j < !i -> j < length a -> a[j] <> 0 } + variant { length a - !i } + if a[!i] = 0 then return !i; + if a[!i] > 0 then i := !i + a[!i] else i := !i + 1 + done; + -1 let rec search_rec (a: array int) (i : int) requires { decrease1 a /\ 0 <= i } diff --git a/examples/mergesort_array.mlw b/examples/mergesort_array.mlw index 56e7385f9848c2166835732734396eb88d991e24..659f8b6774ccd4e90db084cd9e16b175ce531a98 100644 --- a/examples/mergesort_array.mlw +++ b/examples/mergesort_array.mlw @@ -228,9 +228,6 @@ module NaturalMergesort done; !i - exception Break - exception Return - let natural_mergesort (a: array elt) : unit ensures { sorted a } ensures { permut_all (old a) a } @@ -238,14 +235,12 @@ module NaturalMergesort if n >= 2 then let tmp = Array.copy a in let ghost first_run = ref 0 in - try while true do invariant { 0 <= !first_run <= n && sorted_sub a 0 !first_run } invariant { permut_all (old a) a } variant { n - !first_run } label L in let lo = ref 0 in - try while !lo < n - 1 do invariant { 0 <= !lo <= n } invariant { !first_run at L <= !first_run <= n } @@ -254,7 +249,7 @@ module NaturalMergesort invariant { permut_all (a at L) a } variant { n - !lo } let mid = find_run a !lo in - if mid = n then begin if !lo = 0 then raise Return; raise Break end; + if mid = n then begin if !lo = 0 then return; raise L end; let hi = find_run a mid in label M in merge_using tmp a !lo mid hi; @@ -263,9 +258,7 @@ module NaturalMergesort ghost if !lo = 0 then first_run := hi; lo := hi; done - with Break -> () end done - with Return -> () end (** an alternative implementation suggested by Martin Clochard, @@ -283,26 +276,24 @@ module NaturalMergesort ensures { forall j: int. 0 <= j < lo -> a[j] = (old a)[j] } variant { k } = let n = length a in - if lo >= n-1 then n else - try - let mid = ref (find_run a lo) in - if !mid = n then raise Break; - for i = 0 to k-1 do - invariant { lo + i < !mid < n } - invariant { sorted_sub a lo !mid } - invariant { permut_sub (old a) a lo (length a) } - invariant { forall j: int. 0 <= j < lo -> a[j] = (old a)[j] } - let hi = naturalrec tmp a !mid i in - assert { permut_sub (old a) a lo (length a) }; - label M in - merge_using tmp a lo !mid hi; - assert { permut_sub (a at M) a lo hi }; - assert { permut_sub (a at M) a lo (length a) }; - mid := hi; - if !mid = n then raise Break - done; - !mid - with Break -> n end + if lo >= n-1 then return n; + let mid = ref (find_run a lo) in + if !mid = n then return n; + for i = 0 to k-1 do + invariant { lo + i < !mid < n } + invariant { sorted_sub a lo !mid } + invariant { permut_sub (old a) a lo (length a) } + invariant { forall j: int. 0 <= j < lo -> a[j] = (old a)[j] } + let hi = naturalrec tmp a !mid i in + assert { permut_sub (old a) a lo (length a) }; + label M in + merge_using tmp a lo !mid hi; + assert { permut_sub (a at M) a lo hi }; + assert { permut_sub (a at M) a lo (length a) }; + mid := hi; + if !mid = n then return n + done; + !mid let natural_mergesort2 (a: array elt) : unit ensures { sorted a } @@ -312,4 +303,4 @@ module NaturalMergesort let _ = naturalrec tmp a 0 (length a) in () -end \ No newline at end of file +end diff --git a/examples/mjrty.mlw b/examples/mjrty.mlw index d7265c5867eeb4c046f14f3a70046b433bf6d04c..9c625f36a7376f1f4ac433693492187f13c74012 100644 --- a/examples/mjrty.mlw +++ b/examples/mjrty.mlw @@ -28,7 +28,6 @@ module Mjrty use import array.NumOfEq exception Not_found - exception Found type candidate @@ -57,19 +56,15 @@ module Mjrty decr k done; if !k = 0 then raise Not_found; - try - if 2 * !k > n then raise Found; - k := 0; - for i = 0 to n-1 do - invariant { !k = numof a !cand 0 i /\ 2 * !k <= n } - if eq a[i] !cand then begin - incr k; - if 2 * !k > n then raise Found - end - done; - raise Not_found - with Found -> - !cand - end + if 2 * !k > n then return !cand; + k := 0; + for i = 0 to n-1 do + invariant { !k = numof a !cand 0 i /\ 2 * !k <= n } + if eq a[i] !cand then begin + incr k; + if 2 * !k > n then return !cand + end + done; + raise Not_found end diff --git a/examples/patience.mlw b/examples/patience.mlw index fb13300a3b6f6da075a2561b4002a2cfc880a682..200a3b8f4a4ba635b751602b29a8e7099532745b 100644 --- a/examples/patience.mlw +++ b/examples/patience.mlw @@ -85,30 +85,26 @@ module PigeonHole requires { n > m >= 0 } variant { m } ensures { not (injective f n m) } - = try + = for i = 0 to n-1 do invariant { forall k. 0 <= k < i -> f k <> m-1 } - if f i = m-1 then - begin + if f i = m-1 then begin (* we have found index i such that f i = m-1 *) for j = i+1 to n-1 do invariant { forall k. i < k < j -> f k <> m-1 } - if f j = m-1 then raise Found + (* we know that f i = f j = m-1 hence we are done *) + if f j = m-1 then return done; (* we know that for all k <> i, f k <> m-1 *) let g = shift f i in assert { range g (n-1) (m-1) }; pigeon_hole (n-1) (m-1) g; - raise Found; - end + return + end done; (* we know that for all k, f k <> m-1 *) assert { range f n (m-1) }; pigeon_hole n (m-1) f - with Found -> - (* we know that f i = f j = m-1 hence we are done *) - () - end end @@ -328,7 +324,7 @@ module PatienceAbstract ensures { s.values = (old s).values[(old s).num_elts <- c] } = let ghost pred = ref (-1) in - try + try for i = 0 to s.num_stacks - 1 do invariant { if i=0 then !pred = -1 else let stack_im1 = s.stacks[i-1] in @@ -343,19 +339,15 @@ module PatienceAbstract let stack_i = s.stacks[i] in let stack_i_size = s.stack_sizes[i] in let top_stack_i = stack_i[stack_i_size - 1] in - if c <= s.values[top_stack_i] then - raise (Return i) - else - begin - assert { 0 <= top_stack_i < s.num_elts }; - assert { let (is,ip) = s.positions[top_stack_i] in - 0 <= is < s.num_stacks && - 0 <= ip < s.stack_sizes[is] && - s.stacks[is][ip] = top_stack_i && - is = i /\ ip = stack_i_size - 1 - }; - pred := top_stack_i - end + if c <= s.values[top_stack_i] then raise (Return i); + assert { 0 <= top_stack_i < s.num_elts }; + assert { let (is,ip) = s.positions[top_stack_i] in + 0 <= is < s.num_stacks && + 0 <= ip < s.stack_sizes[is] && + s.stacks[is][ip] = top_stack_i && + is = i /\ ip = stack_i_size - 1 + }; + pred := top_stack_i done; (* we add a new stack *) let idx = s.num_elts in diff --git a/examples/pigeonhole.mlw b/examples/pigeonhole.mlw index 4b771545c327f9122be8256b8a3eec7c483bf263..a56a8d3cddf88bc95f160219e7fefab71d4f5c81 100644 --- a/examples/pigeonhole.mlw +++ b/examples/pigeonhole.mlw @@ -9,8 +9,6 @@ module Pigeonhole use import set.Fset use import ref.Ref - exception Exit - let rec below (n: int) : set int requires { 0 <= n } ensures { forall i. mem i result <-> 0 <= i < n } @@ -24,15 +22,13 @@ module Pigeonhole ensures { exists i1, i2. 0 <= i1 < i2 < n /\ f i1 = f i2 } = let s = ref empty in - try for i = 0 to n-1 do invariant { cardinal !s = i } invariant { forall x. mem x !s <-> (exists j. 0 <= j < i /\ x = f j) } - if mem (f i) !s then raise Exit; + if mem (f i) !s then return; s := add (f i) !s done; let b = below m in assert { subset !s b }; absurd - with Exit -> () end end