Commit dcac9198 authored by MARCHE Claude's avatar MARCHE Claude

LCP: a few proofs using coq

parent 3b5be0bb
......@@ -250,7 +250,6 @@ let compare (a:array int) (x y:int) : int
le a data[m-1] data[m] ->
sorted_sub a data l u
(*
lemma sorted_sub_set:
forall a data:array int, l u i v:int.
sorted_sub a data l u /\ u <= i ->
......@@ -260,7 +259,6 @@ let compare (a:array int) (x y:int) : int
forall a data:array int, l u i v:int.
sorted_sub a data l u /\ u <= i ->
sorted_sub a { length = a.length; elts = Map.set data.elts i v } l u
*)
predicate sorted (a : array int) (data:array int) =
sorted_sub a data 0 data.length
......@@ -279,24 +277,30 @@ let compare (a:array int) (x y:int) : int
let j = ref i in
while !j > 0 && compare a data[!j-1] data[!j] > 0 do
invariant { 0 <= !j <= i }
invariant { array_bounded data a.length }
invariant { permut (at data 'Init) data }
invariant { sorted_sub a data 0 !j }
invariant { sorted_sub a data !j (i+1) }
invariant { forall k1 k2:int. 0 <= k1 < !j /\ !j+1 <= k2 <= i ->
le a data[k1] data[k2] }
invariant { array_bounded data a.length }
'L:
assert { le a data[!j] data[!j-1] };
assert { forall k:int. !j+1 <= k <= i -> le a data[!j-1] data[k] };
assert { sorted_sub a data 0 (!j-1) };
assert { sorted_sub a data (!j+1) (i+1) };
let b = !j - 1 in
let t = data[!j] in
assert { sorted_sub a data 0 (!j-1) };
data[!j] <- data[b];
assert { sorted_sub a data 0 (!j-1) };
assert { sorted_sub a data (!j+1) (i+1) };
assert { forall k:int. !j <= k <= i -> le a data[!j] data[k] };
assert { sorted_sub a data !j (i+1) };
data[b] <- t;
assert { le a data[!j-1] data[!j] };
assert { forall k:int. !j <= k <=i -> le a data[!j] data[k] };
assert { exchange (at data 'L) data (!j-1) !j };
assert { sorted_sub a data 0 (!j-1) };
assert { sorted_sub a data !j (i+1) };
decr j
done;
assert { !j > 0 -> le a data[!j-1] data[!j] }
......
This source diff could not be displayed because it is too large. You can view the blob instead.
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