Commit 51034da2 authored by MARCHE Claude's avatar MARCHE Claude

linked_list_rev fully proved + sessions update

parent 82a7ba85
......@@ -3,228 +3,236 @@
<why3session
name="programs/insertion_sort_list/why3session.xml">
<prover
id="alt-ergo"
id="0"
name="Alt-Ergo"
version="0.94"/>
<prover
id="coq"
name="Coq"
version="8.3pl3"/>
<prover
id="cvc3-2.2"
id="1"
name="CVC3"
version="2.2"/>
<prover
id="cvc3-2.4"
name="CVC3"
version="2.4.1"/>
<prover
id="eprover"
name="Eprover"
version="1.4"/>
<prover
id="gappa"
name="Gappa"
version="0.15.1"/>
<prover
id="simplify"
name="Simplify"
version="1.5.4"/>
<prover
id="spass"
name="Spass"
version="3.7"/>
<prover
id="vampire"
name="Vampire"
version="0.6"/>
<prover
id="verit"
name="veriT"
version="dev"/>
<prover
id="yices"
name="Yices"
version="1.0.25"/>
<prover
id="z3-2"
name="Z3"
version="2.19"/>
<prover
id="z3-3"
name="Z3"
version="3.2"/>
<file
name="../insertion_sort_list.mlw"
verified="true"
expanded="true">
expanded="false">
<theory
name="WP M"
locfile="programs/insertion_sort_list/../insertion_sort_list.mlw"
loclnum="4" loccnumb="7" loccnume="8"
verified="true"
expanded="true">
<goal
name="WP_parameter insert"
locfile="programs/insertion_sort_list/../insertion_sort_list.mlw"
loclnum="11" loccnumb="10" loccnume="16"
expl="parameter insert"
sum="8a1ed54c3f0c362fb144098bfd668b32"
sum="84e2aa9751598370fc4d9f6f9c5b4a40"
proved="true"
expanded="true"
shape="CV1aNilapermutaConsV0V1aConsV0aNilAasortedaConsV0aNilaConsVViainfix <=V0V2apermutaConsV0V1aConsV0V1AasortedaConsV0V1apermutaConsV0V1aConsV2V4AasortedaConsV2V4IapermutaConsV0V3V4AasortedV4FAasortedV3Aainfix <alengthV3alengthV1Aainfix <=c0alengthV1IasortedV1FF">
<label
name="expl:parameter insert">
</label>
<transf
name="split_goal"
proved="true"
expanded="true">
<goal
name="WP_parameter insert.1"
locfile="programs/insertion_sort_list/../insertion_sort_list.mlw"
loclnum="11" loccnumb="10" loccnume="16"
expl="parameter insert"
sum="221159a13d4206a4460d1723c7561f5b"
sum="4a69f68c5d460749f0ef438e15442acf"
proved="true"
expanded="true"
shape="CV1aNilapermutaConsV0V1aConsV0aNilAasortedaConsV0aNilaConsVVtIasortedV1FF">
<label
name="expl:parameter insert">
</label>
<proof
prover="alt-ergo"
prover="0"
timelimit="10"
edited=""
obsolete="false">
obsolete="false"
archived="false">
<result status="valid" time="0.02"/>
</proof>
</goal>
<goal
name="WP_parameter insert.2"
locfile="programs/insertion_sort_list/../insertion_sort_list.mlw"
loclnum="11" loccnumb="10" loccnume="16"
expl="parameter insert"
sum="03780f98738f0a4d31b9f5cdafef018f"
sum="ca1192523c9f6846cbe0519ed7977850"
proved="true"
expanded="true"
shape="CV1aNiltaConsVVapermutaConsV0V1aConsV0V1AasortedaConsV0V1Iainfix <=V0V2IasortedV1FF">
<label
name="expl:parameter insert">
</label>
<proof
prover="cvc3-2.2"
prover="1"
timelimit="10"
edited=""
obsolete="false">
obsolete="false"
archived="false">
<result status="valid" time="0.01"/>
</proof>
</goal>
<goal
name="WP_parameter insert.3"
locfile="programs/insertion_sort_list/../insertion_sort_list.mlw"
loclnum="11" loccnumb="10" loccnume="16"
expl="parameter insert"
sum="bd15c5616f0e48a457c665b7daeb5133"
sum="323ba14021e983aedaa70f389a6f9ca2"
proved="true"
expanded="true"
shape="CV1aNiltaConsVVasortedV3Aainfix <alengthV3alengthV1Aainfix <=c0alengthV1Iainfix <=V0V2NIasortedV1FF">
<label
name="expl:parameter insert">
</label>
<proof
prover="cvc3-2.2"
prover="1"
timelimit="10"
edited=""
obsolete="false">
<result status="valid" time="0.00"/>
obsolete="false"
archived="false">
<result status="valid" time="0.01"/>
</proof>
</goal>
<goal
name="WP_parameter insert.4"
locfile="programs/insertion_sort_list/../insertion_sort_list.mlw"
loclnum="11" loccnumb="10" loccnume="16"
expl="parameter insert"
sum="17df99648aa521a75f2047df4cf0c6f0"
sum="3dd8034ce59793f25f60f2f400095552"
proved="true"
expanded="true"
shape="CV1aNiltaConsVVapermutaConsV0V1aConsV2V4AasortedaConsV2V4IapermutaConsV0V3V4AasortedV4FIasortedV3Aainfix <alengthV3alengthV1Aainfix <=c0alengthV1Iainfix <=V0V2NIasortedV1FF">
<label
name="expl:parameter insert">
</label>
<proof
prover="cvc3-2.2"
prover="1"
timelimit="10"
edited=""
obsolete="false">
<result status="valid" time="0.11"/>
obsolete="false"
archived="false">
<result status="valid" time="0.18"/>
</proof>
</goal>
</transf>
</goal>
<goal
name="WP_parameter insertion_sort"
locfile="programs/insertion_sort_list/../insertion_sort_list.mlw"
loclnum="19" loccnumb="10" loccnume="24"
expl="parameter insertion_sort"
sum="d28eefc56d379c5156175265bf010598"
sum="16d8a43872423232fe7bd6e35d3a5ba5"
proved="true"
expanded="true"
shape="CV0aNilapermutV0aNilAasortedaNilaConsVVapermutV0V4AasortedV4IapermutaConsV1V3V4AasortedV4FAasortedV3IapermutV2V3AasortedV3FAainfix <alengthV2alengthV0Aainfix <=c0alengthV0F">
<label
name="expl:parameter insertion_sort">
</label>
<transf
name="split_goal"
proved="true"
expanded="true">
<goal
name="WP_parameter insertion_sort.1"
locfile="programs/insertion_sort_list/../insertion_sort_list.mlw"
loclnum="19" loccnumb="10" loccnume="24"
expl="parameter insertion_sort"
sum="71173457dcb476b018a44d47d231ad49"
sum="94c7e6b8ec2a0a739033d3bd222c577f"
proved="true"
expanded="true"
shape="CV0aNilapermutV0aNilAasortedaNilaConsVVtF">
<label
name="expl:parameter insertion_sort">
</label>
<proof
prover="cvc3-2.2"
prover="1"
timelimit="10"
edited=""
obsolete="false">
<result status="valid" time="0.00"/>
obsolete="false"
archived="false">
<result status="valid" time="0.01"/>
</proof>
</goal>
<goal
name="WP_parameter insertion_sort.2"
locfile="programs/insertion_sort_list/../insertion_sort_list.mlw"
loclnum="19" loccnumb="10" loccnume="24"
expl="parameter insertion_sort"
sum="17e9acde476c648319587d89cd36c1c8"
sum="59f3bde7dbb179dd4ba4e0943bb955c7"
proved="true"
expanded="true"
shape="CV0aNiltaConsVVainfix <alengthV2alengthV0Aainfix <=c0alengthV0F">
<label
name="expl:parameter insertion_sort">
</label>
<proof
prover="cvc3-2.2"
prover="1"
timelimit="10"
edited=""
obsolete="false">
<result status="valid" time="0.00"/>
obsolete="false"
archived="false">
<result status="valid" time="0.01"/>
</proof>
<proof
prover="alt-ergo"
prover="0"
timelimit="10"
edited=""
obsolete="false">
obsolete="false"
archived="false">
<result status="valid" time="0.01"/>
</proof>
</goal>
<goal
name="WP_parameter insertion_sort.3"
locfile="programs/insertion_sort_list/../insertion_sort_list.mlw"
loclnum="19" loccnumb="10" loccnume="24"
expl="parameter insertion_sort"
sum="80b0842e233ef20ca04bf6ed7b47e326"
sum="01a3a1139967fc619194daefb574ad7e"
proved="true"
expanded="true"
shape="CV0aNiltaConsVVasortedV3IapermutV2V3AasortedV3FIainfix <alengthV2alengthV0Aainfix <=c0alengthV0F">
<label
name="expl:parameter insertion_sort">
</label>
<proof
prover="cvc3-2.2"
prover="1"
timelimit="10"
edited=""
obsolete="false">
<result status="valid" time="0.00"/>
obsolete="false"
archived="false">
<result status="valid" time="0.01"/>
</proof>
<proof
prover="alt-ergo"
prover="0"
timelimit="10"
edited=""
obsolete="false">
obsolete="false"
archived="false">
<result status="valid" time="0.00"/>
</proof>
</goal>
<goal
name="WP_parameter insertion_sort.4"
locfile="programs/insertion_sort_list/../insertion_sort_list.mlw"
loclnum="19" loccnumb="10" loccnume="24"
expl="parameter insertion_sort"
sum="70da74d76767b2269d36aef985b01798"
sum="0664d39ce85984eefbde659a0dd4e23a"
proved="true"
expanded="true"
shape="CV0aNiltaConsVVapermutV0V4AasortedV4IapermutaConsV1V3V4AasortedV4FIasortedV3IapermutV2V3AasortedV3FIainfix <alengthV2alengthV0Aainfix <=c0alengthV0F">
<label
name="expl:parameter insertion_sort">
</label>
<proof
prover="cvc3-2.2"
prover="1"
timelimit="10"
edited=""
obsolete="false">
<result status="valid" time="0.03"/>
obsolete="false"
archived="false">
<result status="valid" time="0.04"/>
</proof>
<proof
prover="alt-ergo"
prover="0"
timelimit="10"
edited=""
obsolete="false">
<result status="valid" time="0.03"/>
obsolete="false"
archived="false">
<result status="valid" time="0.08"/>
</proof>
</goal>
</transf>
......
......@@ -54,8 +54,17 @@ module InPlaceRev
list_seg p next1 pM null /\ next2 = set next1 q v /\
not (mem q pM) -> list_seg p next2 pM null
lemma list_seg_functional:
forall next:map loc loc, l1 l2:list loc, p: loc.
list_seg p next l1 null /\ list_seg p next l2 null -> l1 = l2
lemma list_seg_sublistl:
forall next:map loc loc, l1 l2:list loc, p q: loc.
list_seg p next (l1++Cons q l2) null ->
list_seg q next (Cons q l2) null
lemma list_seg_no_repet:
forall next:map loc loc, p: loc, pM:list loc.
forall next:map loc loc, pM:list loc, p: loc.
list_seg p next pM null -> no_repet pM
use import module ref.Ref
......
(* This file is generated by Why3's Coq driver *)
(* Beware! Only edit allowed sections below *)
Require Import ZArith.
Require Import Rbase.
Require int.Int.
Definition unit := unit.
Parameter qtmark : Type.
Parameter at1: forall (a:Type), a -> qtmark -> a.
Implicit Arguments at1.
Parameter old: forall (a:Type), a -> a.
Implicit Arguments old.
Definition implb(x:bool) (y:bool): bool := match (x,
y) with
| (true, false) => false
| (_, _) => true
end.
Inductive list (a:Type) :=
| Nil : list a
| Cons : a -> (list a) -> list a.
Set Contextual Implicit.
Implicit Arguments Nil.
Unset Contextual Implicit.
Implicit Arguments Cons.
Parameter head: forall (a:Type), (list a) -> a.
Implicit Arguments head.
Axiom head_cons : forall (a:Type), forall (x:a) (l:(list a)), ((head (Cons x
l)) = x).
Parameter tail: forall (a:Type), (list a) -> (list a).
Implicit Arguments tail.
Axiom tail_cons : forall (a:Type), forall (x:a) (l:(list a)), ((tail (Cons x
l)) = l).
Set Implicit Arguments.
Fixpoint mem (a:Type)(x:a) (l:(list a)) {struct l}: Prop :=
match l with
| Nil => False
| (Cons y r) => (x = y) \/ (mem x r)
end.
Unset Implicit Arguments.
Definition disjoint (a:Type)(l1:(list a)) (l2:(list a)): Prop :=
forall (x:a), ~ ((mem x l1) /\ (mem x l2)).
Implicit Arguments disjoint.
Set Implicit Arguments.
Fixpoint no_repet (a:Type)(l:(list a)) {struct l}: Prop :=
match l with
| Nil => True
| (Cons x r) => (~ (mem x r)) /\ (no_repet r)
end.
Unset Implicit Arguments.
Set Implicit Arguments.
Fixpoint infix_plpl (a:Type)(l1:(list a)) (l2:(list a)) {struct l1}: (list
a) :=
match l1 with
| Nil => l2
| (Cons x1 r1) => (Cons x1 (infix_plpl r1 l2))
end.
Unset Implicit Arguments.
Axiom Append_assoc : forall (a:Type), forall (l1:(list a)) (l2:(list a))
(l3:(list a)), ((infix_plpl l1 (infix_plpl l2
l3)) = (infix_plpl (infix_plpl l1 l2) l3)).
Axiom Append_l_nil : forall (a:Type), forall (l:(list a)), ((infix_plpl l
(Nil:(list a))) = l).
Set Implicit Arguments.
Fixpoint length (a:Type)(l:(list a)) {struct l}: Z :=
match l with
| Nil => 0%Z
| (Cons _ r) => (1%Z + (length r))%Z
end.
Unset Implicit Arguments.
Axiom Length_nonnegative : forall (a:Type), forall (l:(list a)),
(0%Z <= (length l))%Z.
Axiom Length_nil : forall (a:Type), forall (l:(list a)),
((length l) = 0%Z) <-> (l = (Nil:(list a))).
Axiom Append_length : forall (a:Type), forall (l1:(list a)) (l2:(list a)),
((length (infix_plpl l1 l2)) = ((length l1) + (length l2))%Z).
Axiom mem_append : forall (a:Type), forall (x:a) (l1:(list a)) (l2:(list a)),
(mem x (infix_plpl l1 l2)) <-> ((mem x l1) \/ (mem x l2)).
Axiom mem_decomp : forall (a:Type), forall (x:a) (l:(list a)), (mem x l) ->
exists l1:(list a), exists l2:(list a), (l = (infix_plpl l1 (Cons x l2))).
Set Implicit Arguments.
Fixpoint reverse (a:Type)(l:(list a)) {struct l}: (list a) :=
match l with
| Nil => (Nil:(list a))
| (Cons x r) => (infix_plpl (reverse r) (Cons x (Nil:(list a))))
end.
Unset Implicit Arguments.
Axiom reverse_append : forall (a:Type), forall (l1:(list a)) (l2:(list a))
(x:a), ((infix_plpl (reverse (Cons x l1)) l2) = (infix_plpl (reverse l1)
(Cons x l2))).
Axiom reverse_reverse : forall (a:Type), forall (l:(list a)),
((reverse (reverse l)) = l).
Axiom Reverse_length : forall (a:Type), forall (l:(list a)),
((length (reverse l)) = (length l)).
Parameter map : forall (a:Type) (b:Type), Type.
Parameter get: forall (a:Type) (b:Type), (map a b) -> a -> b.
Implicit Arguments get.
Parameter set: forall (a:Type) (b:Type), (map a b) -> a -> b -> (map a b).
Implicit Arguments set.
Axiom Select_eq : forall (a:Type) (b:Type), forall (m:(map a b)),
forall (a1:a) (a2:a), forall (b1:b), (a1 = a2) -> ((get (set m a1 b1)
a2) = b1).
Axiom Select_neq : forall (a:Type) (b:Type), forall (m:(map a b)),
forall (a1:a) (a2:a), forall (b1:b), (~ (a1 = a2)) -> ((get (set m a1 b1)
a2) = (get m a2)).
Parameter const: forall (b:Type) (a:Type), b -> (map a b).
Set Contextual Implicit.
Implicit Arguments const.
Unset Contextual Implicit.
Axiom Const : forall (b:Type) (a:Type), forall (b1:b) (a1:a), ((get (const(
b1):(map a b)) a1) = b1).
Parameter loc : Type.
Parameter null: loc.
Inductive list_seg : loc -> (map loc loc) -> (list loc) -> loc -> Prop :=
| list_seg_nil : forall (p:loc) (next:(map loc loc)), (list_seg p next
(Nil:(list loc)) p)
| list_seg_cons : forall (p:loc) (q:loc) (next:(map loc loc)) (l:(list
loc)), ((~ (p = null)) /\ (list_seg (get next p) next l q)) ->
(list_seg p next (Cons p l) q).
Axiom list_seg_frame : forall (next1:(map loc loc)) (next2:(map loc loc))
(p:loc) (q:loc) (v:loc) (pM:(list loc)), ((list_seg p next1 pM null) /\
((next2 = (set next1 q v)) /\ ~ (mem q pM))) -> (list_seg p next2 pM null).
(* YOU MAY EDIT THE CONTEXT BELOW *)
(* DO NOT EDIT BELOW *)
Theorem list_seg_functional : forall (next:(map loc loc)) (l1:(list loc))
(l2:(list loc)) (p:loc), ((list_seg p next l1 null) /\ (list_seg p next l2
null)) -> (l1 = l2).
(* YOU MAY EDIT THE PROOF BELOW *)
induction l1.
intros l2 p (h1,h2).
inversion h1; subst; clear h1.
inversion h2; subst; clear h2; intuition.
intros l2 p (h1,h2).
inversion h1; subst; clear h1.
inversion h2; subst; clear h2; intuition.
apply f_equal.
apply IHl1 with (p:=get next a); auto.
Qed.
(* DO NOT EDIT BELOW *)
......@@ -163,15 +163,46 @@ Axiom list_seg_frame : forall (next1:(map loc loc)) (next2:(map loc loc))
(p:loc) (q:loc) (v:loc) (pM:(list loc)), ((list_seg p next1 pM null) /\
((next2 = (set next1 q v)) /\ ~ (mem q pM))) -> (list_seg p next2 pM null).
Axiom list_seg_functional : forall (next:(map loc loc)) (l1:(list loc))
(l2:(list loc)) (p:loc), ((list_seg p next l1 null) /\ (list_seg p next l2
null)) -> (l1 = l2).
Axiom list_seg_sublistl : forall (next:(map loc loc)) (l1:(list loc))
(l2:(list loc)) (p:loc) (q:loc), (list_seg p next (infix_plpl l1 (Cons q
l2)) null) -> (list_seg q next (Cons q l2) null).
(* YOU MAY EDIT THE CONTEXT BELOW *)
(* DO NOT EDIT BELOW *)
Theorem list_seg_no_repet : forall (next:(map loc loc)) (p:loc) (pM:(list
loc)), (list_seg p next pM null) -> (no_repet pM).
Theorem list_seg_no_repet : forall (next:(map loc loc)) (pM:(list loc))
(p:loc), (list_seg p next pM null) -> (no_repet pM).
(* YOU MAY EDIT THE PROOF BELOW *)
intros.
(* is there an easy induction ?? *)
induction pM.
now simpl.
intros p h.
assert (a=p) by (inversion h; auto).
subst a.
split.
intro h1.
generalize (mem_decomp _ p pM h1).
intros (l1&l2&h2).
subst pM.
change (Cons p (infix_plpl l1 (Cons p l2))) with
(infix_plpl (Cons p l1) (Cons p l2)) in h.
generalize (list_seg_sublistl _ _ _ _ _ h).
intro h2.
generalize (list_seg_functional _ _ _ _ (conj h h2)).
intro h3.
generalize (f_equal (@length _) h3).
rewrite Append_length.
intros h4.
generalize (Length_nonnegative _ l1).
change (length (Cons p l1)) with (1+length l1)%Z in h4.
omega.
inversion h; subst; clear h.
apply IHpM with (p := get next p).
tauto.
Qed.
(* DO NOT EDIT BELOW *)
......
(* This file is generated by Why3's Coq driver *)
(* Beware! Only edit allowed sections below *)
Require Import ZArith.
Require Import Rbase.
Require int.Int.
Definition unit := unit.
Parameter qtmark : Type.
Parameter at1: forall (a:Type), a -> qtmark -> a.
Implicit Arguments at1.
Parameter old: forall (a:Type), a -> a.
Implicit Arguments old.
Definition implb(x:bool) (y:bool): bool := match (x,
y) with
| (true, false) => false
| (_, _) => true
end.
Inductive list (a:Type) :=
| Nil : list a
| Cons : a -> (list a) -> list a.
Set Contextual Implicit.
Implicit Arguments Nil.
Unset Contextual Implicit.
Implicit Arguments Cons.
Parameter head: forall (a:Type), (list a) -> a.
Implicit Arguments head.
Axiom head_cons : forall (a:Type), forall (x:a) (l:(list a)), ((head (Cons x
l)) = x).
Parameter tail: forall (a:Type), (list a) -> (list a).
Implicit Arguments tail.
Axiom tail_cons : forall (a:Type), forall (x:a) (l:(list a)), ((tail (Cons x
l)) = l).
Set Implicit Arguments.
Fixpoint mem (a:Type)(x:a) (l:(list a)) {struct l}: Prop :=
match l with
| Nil => False
| (Cons y r) => (x = y) \/ (mem x r)
end.
Unset Implicit Arguments.
Definition disjoint (a:Type)(l1:(list a)) (l2:(list a)): Prop :=
forall (x:a), ~ ((mem x l1) /\ (mem x l2)).
Implicit Arguments disjoint.
Set Implicit Arguments.
Fixpoint no_repet (a:Type)(l:(list a)) {struct l}: Prop :=
match l with
| Nil => True
| (Cons x r) => (~ (mem x r)) /\ (no_repet r)
end.
Unset Implicit Arguments.
Set Implicit Arguments.
Fixpoint infix_plpl (a:Type)(l1:(list a)) (l2:(list a)) {struct l1}: (list
a) :=