Commit d23e9cd8 authored by Andrei Paskevich's avatar Andrei Paskevich

use "return" in several examples

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