mjrty example: cleaning up

parent 4c0b7fc9
......@@ -33,7 +33,7 @@ module Mjrty
clone import array.NumOfEq with type elt = candidate
let mjrty (a: array candidate)
let mjrty (a: array candidate) : candidate
requires { 1 <= length a }
ensures { 2 * numof a result 0 (length a) > length a }
raises { Not_found ->
......@@ -42,11 +42,9 @@ module Mjrty
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 *)
invariant {
0 <= !k <= numof a !cand 0 i /\
2 * (numof a !cand 0 i - !k) <= i - !k /\
forall c: candidate. c <> !cand -> 2 * numof a c 0 i <= i - !k
}
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 }
if !k = 0 then begin
cand := a[i];
k := 1
......
This diff is collapsed.
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