Commit 9356fe25 by Jean-Christophe Filliâtre

### updated examples using cool new features

parent 50123b81
 ... ... @@ -253,7 +253,7 @@ module BoundedIntegers use int.Sum function sum (a: array int63) (lo hi: int) : int = Sum.sum (fun i -> to_int a[i]) lo hi Sum.sum (fun i -> (a[i] : int)) lo hi let maximum_subarray (a: array int63) (ghost lo hi: ref int): int63 requires { "no overflow" forall l h. 0 <= l <= h <= length a -> ... ... @@ -276,7 +276,7 @@ module BoundedIntegers if !s < zero then begin s := a[!i]; l := to_int !i end else begin assert { sum a !l (!i + 1) <= max_int }; s += a[!i] end; if !s > !ms then begin ms := !s; lo := !l; hi := Int.(+) (to_int !i) 1 end; ms := !s; lo := !l; hi := to_int !i + 1 end; incr i done; !ms ... ...
 ... ... @@ -102,16 +102,15 @@ module TopDownMergesort ensures { sorted_sub a l r } ensures { permut_sub (old a) a l r } variant { r - l } = if l < r-1 then begin let m = l + (r - l) / 2 in assert { l <= m < r }; mergesort_rec a tmp l m; assert { permut_sub (old a) a l r }; label M in mergesort_rec a tmp m r; assert { permut_sub (a at M) a l r }; merge_using tmp a l m r; end = if l >= r-1 then return; let m = l + (r - l) / 2 in assert { l <= m < r }; mergesort_rec a tmp l m; assert { permut_sub (old a) a l r }; label M in mergesort_rec a tmp m r; assert { permut_sub (a at M) a l r }; merge_using tmp a l m r let mergesort (a: array elt) : unit ensures { sorted a } ... ... @@ -232,7 +231,7 @@ module NaturalMergesort ensures { sorted a } ensures { permut_all (old a) a } = let n = length a in if n >= 2 then if n <= 1 then return; let tmp = Array.copy a in let ghost first_run = ref 0 in while true do ... ...
This diff is collapsed.
No preview for this file type
 ... ... @@ -16,8 +16,7 @@ - arrays are 0-based - we assume the input array to have at least one element - we use 2x <= y instead of x <= floor(y/2), which is equivalent - we do not consider arithmetic overflows (easy, but requires the extra hypothesis length a <= max_int) *) module Mjrty ... ... @@ -31,26 +30,24 @@ module Mjrty type candidate val eq (x y: candidate) : bool val (=) (x y: candidate) : bool ensures { result <-> x = y } (* FIXME: call it (=) when we have overloading *) let mjrty (a: array candidate) : candidate requires { 1 <= length a } ensures { 2 * numof a result 0 (length a) > length a } raises { Not_found -> forall c: candidate. 2 * numof a c 0 (length a) <= length a } raises { Not_found -> forall c. 2 * numof a c 0 (length a) <= length a } = let n = length a in let cand = ref a[0] in let k = ref 0 in for i = 0 to n-1 do (* could start at 1 with k initialized to 1 *) for i = 0 to n - 1 do (* could start at 1 with k initialized to 1 *) invariant { 0 <= !k <= numof a !cand 0 i } invariant {2 * (numof a !cand 0 i - !k) <= i - !k } invariant {forall c:candidate. c <> !cand -> 2 * numof a c 0 i <= i - !k } invariant { 2 * (numof a !cand 0 i - !k) <= i - !k } invariant { forall c. c <> !cand -> 2 * numof a c 0 i <= i - !k } if !k = 0 then begin cand := a[i]; k := 1 end else if eq !cand a[i] then end else if !cand = a[i] then incr k else decr k ... ... @@ -58,9 +55,9 @@ module Mjrty if !k = 0 then raise Not_found; if 2 * !k > n then return !cand; 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 } if eq a[i] !cand then begin if a[i] = !cand then begin incr k; if 2 * !k > n then return !cand end ... ...
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!