Commit c4da6ea2 authored by MARCHE Claude's avatar MARCHE Claude

more logic examples

parent 8f2e9733
......@@ -147,7 +147,6 @@ why3.conf
/tests/test-and/
# /examples/
/examples/genealogy/
/examples/programs/course/
/examples/programs/wcet_hull/
/examples/programs/binary_search2/
......
This diff is collapsed.
<?xml version="1.0" encoding="UTF-8"?>
<!DOCTYPE why3session SYSTEM "why3session.dtd">
<why3session
name="examples/genealogy/why3session.xml">
<prover
id="alt-ergo"
name="Alt-Ergo"
version="0.93"/>
<prover
id="coq"
name="Coq"
version="8.3pl2"/>
<prover
id="cvc3"
name="CVC3"
version="2.2"/>
<prover
id="gappa"
name="Gappa"
version="0.15.0"/>
<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="yices"
name="Yices"
version="1.0.25"/>
<prover
id="z3"
name="Z3"
version="2.19"/>
<file
name="../genealogy.why"
verified="true"
expanded="true">
<theory
name="Genealogy"
verified="true"
expanded="true">
<goal
name="Child_is_son_or_daughter"
sum="0d9428be56bdef7e1d922bf2238f1165"
proved="true"
expanded="true"
shape="adaughterV0V1OasonV0V1qachildV0V1F">
<proof
prover="cvc3"
timelimit="5"
edited=""
obsolete="false">
<result status="valid" time="0.00"/>
</proof>
<proof
prover="alt-ergo"
timelimit="5"
edited=""
obsolete="false">
<result status="unknown" time="0.02"/>
</proof>
<proof
prover="z3"
timelimit="5"
edited=""
obsolete="false">
<result status="valid" time="0.00"/>
</proof>
<proof
prover="vampire"
timelimit="5"
edited=""
obsolete="false">
<result status="valid" time="0.00"/>
</proof>
<proof
prover="spass"
timelimit="5"
edited=""
obsolete="false">
<result status="valid" time="0.01"/>
</proof>
</goal>
<goal
name="Sibling_sym"
sum="70b829c50403667e5bc14a04cc1159bd"
proved="true"
expanded="true"
shape="asiblingV1V0IasiblingV0V1F">
<proof
prover="cvc3"
timelimit="5"
edited=""
obsolete="false">
<result status="valid" time="0.00"/>
</proof>
<proof
prover="alt-ergo"
timelimit="5"
edited=""
obsolete="false">
<result status="valid" time="0.01"/>
</proof>
<proof
prover="z3"
timelimit="5"
edited=""
obsolete="false">
<result status="valid" time="0.01"/>
</proof>
<proof
prover="vampire"
timelimit="5"
edited=""
obsolete="false">
<result status="valid" time="0.01"/>
</proof>
<proof
prover="spass"
timelimit="5"
edited=""
obsolete="false">
<result status="valid" time="0.01"/>
</proof>
</goal>
<goal
name="Sibling_is_brother_or_sister"
sum="0e8bcad7ab8ffb579a7b587bf3a5395a"
proved="true"
expanded="true"
shape="asisterV0V1OabrotherV0V1qasiblingV0V1F">
<proof
prover="cvc3"
timelimit="5"
edited=""
obsolete="false">
<result status="valid" time="0.00"/>
</proof>
<proof
prover="alt-ergo"
timelimit="5"
edited=""
obsolete="false">
<result status="unknown" time="0.01"/>
</proof>
<proof
prover="z3"
timelimit="5"
edited=""
obsolete="false">
<result status="valid" time="0.01"/>
</proof>
<proof
prover="vampire"
timelimit="5"
edited=""
obsolete="false">
<result status="valid" time="0.00"/>
</proof>
<proof
prover="spass"
timelimit="5"
edited=""
obsolete="false">
<result status="valid" time="0.01"/>
</proof>
</goal>
<goal
name="Grandparent_is_grandfather_or_grandmother"
sum="9b434898ae387b15f4efa4ef0360638c"
proved="true"
expanded="true"
shape="agrandmotherV0V1OagrandfatherV0V1qagrandparentV0V1F">
<proof
prover="cvc3"
timelimit="5"
edited=""
obsolete="false">
<result status="valid" time="0.00"/>
</proof>
<proof
prover="alt-ergo"
timelimit="5"
edited=""
obsolete="false">
<result status="valid" time="0.02"/>
</proof>
<proof
prover="z3"
timelimit="5"
edited=""
obsolete="false">
<result status="valid" time="0.01"/>
</proof>
<proof
prover="vampire"
timelimit="5"
edited=""
obsolete="false">
<result status="timeout" time="5.97"/>
</proof>
<proof
prover="spass"
timelimit="5"
edited=""
obsolete="false">
<result status="timeout" time="5.98"/>
</proof>
</goal>
<goal
name="Grandfather_male"
sum="4d3f039d1dd398d21204dd8c93de3a95"
proved="true"
expanded="true"
shape="ainfix =agenderV0aMaleIagrandfatherV0V1F">
<proof
prover="cvc3"
timelimit="5"
edited=""
obsolete="false">
<result status="valid" time="0.00"/>
</proof>
<proof
prover="alt-ergo"
timelimit="5"
edited=""
obsolete="false">
<result status="valid" time="0.01"/>
</proof>
<proof
prover="z3"
timelimit="5"
edited=""
obsolete="false">
<result status="valid" time="0.01"/>
</proof>
<proof
prover="vampire"
timelimit="5"
edited=""
obsolete="false">
<result status="valid" time="0.03"/>
</proof>
<proof
prover="spass"
timelimit="5"
edited=""
obsolete="false">
<result status="valid" time="0.02"/>
</proof>
</goal>
<goal
name="Grandmother_female"
sum="ead3173c219c2fcdd4529070c8b91a5d"
proved="true"
expanded="true"
shape="ainfix =agenderV0aFemaleIagrandmotherV0V1F">
<proof
prover="cvc3"
timelimit="5"
edited=""
obsolete="false">
<result status="valid" time="0.00"/>
</proof>
<proof
prover="alt-ergo"
timelimit="5"
edited=""
obsolete="false">
<result status="valid" time="0.01"/>
</proof>
<proof
prover="z3"
timelimit="5"
edited=""
obsolete="false">
<result status="valid" time="0.00"/>
</proof>
<proof
prover="vampire"
timelimit="5"
edited=""
obsolete="false">
<result status="valid" time="0.02"/>
</proof>
<proof
prover="spass"
timelimit="5"
edited=""
obsolete="false">
<result status="valid" time="0.02"/>
</proof>
</goal>
<goal
name="Only_two_grandfathers"
sum="22d7d550efa239a19b13533aa853c732"
proved="true"
expanded="true"
shape="ainfix =V0V2Oainfix =V1V2Oainfix =V0V1IagrandfatherV2V3IagrandfatherV1V3IagrandfatherV0V3F">
<proof
prover="cvc3"
timelimit="5"
edited=""
obsolete="false">
<result status="valid" time="0.00"/>
</proof>
<proof
prover="alt-ergo"
timelimit="5"
edited=""
obsolete="false">
<result status="valid" time="0.02"/>
</proof>
<proof
prover="z3"
timelimit="5"
edited=""
obsolete="false">
<result status="valid" time="0.01"/>
</proof>
<proof
prover="vampire"
timelimit="5"
edited=""
obsolete="false">
<result status="timeout" time="5.98"/>
</proof>
<proof
prover="spass"
timelimit="5"
edited=""
obsolete="false">
<result status="valid" time="0.01"/>
</proof>
</goal>
</theory>
</file>
</why3session>
<?xml version="1.0" encoding="UTF-8"?>
<!DOCTYPE why3session SYSTEM "why3session.dtd">
<why3session
name="examples/ns_clone/why3session.xml">
<prover
id="alt-ergo"
name="Alt-Ergo"
version="0.93"/>
<prover
id="coq"
name="Coq"
version="8.3pl2"/>
<prover
id="cvc3"
name="CVC3"
version="2.2"/>
<prover
id="gappa"
name="Gappa"
version="0.15.0"/>
<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="yices"
name="Yices"
version="1.0.25"/>
<prover
id="z3"
name="Z3"
version="2.19"/>
<file
name="../ns_clone.why"
verified="true"
expanded="true">
<theory
name="Sig"
verified="true"
expanded="true">
</theory>
<theory
name="Struct"
verified="true"
expanded="true">
<goal
name="AddMem"
sum="c8b1c322d4e0d8d659ca857c742357c8"
proved="true"
expanded="true"
shape="amemV0aaddV0V1F">
<proof
prover="simplify"
timelimit="5"
edited=""
obsolete="false">
<result status="valid" time="0.00"/>
</proof>
<proof
prover="cvc3"
timelimit="5"
edited=""
obsolete="false">
<result status="valid" time="0.00"/>
</proof>
<proof
prover="alt-ergo"
timelimit="5"
edited=""
obsolete="false">
<result status="valid" time="0.01"/>
</proof>
<proof
prover="gappa"
timelimit="5"
edited=""
obsolete="false">
<result status="valid" time="0.00"/>
</proof>
<proof
prover="z3"
timelimit="5"
edited=""
obsolete="false">
<result status="valid" time="0.01"/>
</proof>
<proof
prover="yices"
timelimit="5"
edited=""
obsolete="false">
<result status="valid" time="0.00"/>
</proof>
<proof
prover="vampire"
timelimit="5"
edited=""
obsolete="false">
<result status="valid" time="0.00"/>
</proof>
<proof
prover="spass"
timelimit="5"
edited=""
obsolete="false">
<result status="valid" time="0.01"/>
</proof>
</goal>
</theory>
<theory
name="Shared"
verified="true"
expanded="true">
</theory>
<theory
name="AbstractUser"
verified="true"
expanded="true">
</theory>
<theory
name="ConcreteUser"
verified="true"
expanded="true">
<goal
name="AddMem"
sum="06d9434ece994aa021951514fb5536ac"
proved="true"
expanded="true"
shape="amemV0aaddV0V1F">
<proof
prover="simplify"
timelimit="5"
edited=""
obsolete="false">
<result status="valid" time="0.00"/>
</proof>
<proof
prover="cvc3"
timelimit="5"
edited=""
obsolete="false">
<result status="valid" time="0.00"/>
</proof>
<proof
prover="alt-ergo"
timelimit="5"
edited=""
obsolete="false">
<result status="valid" time="0.01"/>
</proof>
<proof
prover="gappa"
timelimit="5"
edited=""
obsolete="false">
<result status="valid" time="0.00"/>
</proof>
<proof
prover="z3"
timelimit="5"
edited=""
obsolete="false">
<result status="valid" time="0.00"/>
</proof>
<proof
prover="yices"
timelimit="5"
edited=""
obsolete="false">
<result status="valid" time="0.00"/>
</proof>
<proof
prover="vampire"
timelimit="5"
edited=""
obsolete="false">
<result status="valid" time="0.00"/>
</proof>
<proof
prover="spass"
timelimit="5"
edited=""
obsolete="false">
<result status="valid" time="0.01"/>
</proof>
</goal>
</theory>
</file>
</why3session>
......@@ -29,9 +29,16 @@ theory SortedList
forall x y : t, l : list t.
x <= y -> sorted (Cons y l) -> sorted (Cons x (Cons y l))
lemma sorted_inf:
forall x y: t, l: list t. x <= y -> sorted (Cons y l) ->
sorted (Cons x l)
lemma sorted_mem:
forall x: t, l: list t. sorted (Cons x l) ->
forall y: t. mem y l -> x <= y
(* by induction on l *)
end
theory SortedIntList
......
(* This file is generated by Why3's Coq driver *)
(* Beware! Only edit allowed sections below *)
Require Import ZArith.
Require Import Rbase.
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.
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.
Parameter t : Type.
Parameter infix_lseq: t -> t -> Prop.
Axiom le_refl : forall (x:t), (infix_lseq x x).
Axiom le_asym : forall (x:t) (y:t), (infix_lseq x y) -> ((infix_lseq y x) ->
(x = y)).
Axiom le_trans : forall (x:t) (y:t) (z:t), (infix_lseq x y) -> ((infix_lseq y
z) -> (infix_lseq x z)).
Inductive sorted : (list t) -> Prop :=
| sorted_nil : (sorted (Nil:(list t)))
| sorted_one : forall (x:t), (sorted (Cons x (Nil:(list t))))
| sorted_two : forall (x:t) (y:t) (l:(list t)), (infix_lseq x y) ->
((sorted (Cons y l)) -> (sorted (Cons x (Cons y l)))).
Axiom sorted_inf : forall (x:t) (y:t) (l:(list t)), (infix_lseq x y) ->
((sorted (Cons y l)) -> (sorted (Cons x l))).
(* YOU MAY EDIT THE CONTEXT BELOW *)
(* DO NOT EDIT BELOW *)
Theorem sorted_mem : forall (x:t) (l:(list t)), (sorted (Cons x l)) ->
forall (y:t), (mem y l) -> (infix_lseq x y).
(* YOU MAY EDIT THE PROOF BELOW *)
induction l.
simpl; tauto.
simpl.
intro H.
inversion H.
intros y0 [Heq | Hmem].
subst; auto.
apply IHl; auto.
apply sorted_inf with (y:=a); auto.
Qed.
(* DO NOT EDIT BELOW *)
<?xml version="1.0" encoding="UTF-8"?>
<!DOCTYPE why3session SYSTEM "why3session.dtd">
<why3session
name="examples/sorted_list/why3session.xml">
<prover
id="alt-ergo"
name="Alt-Ergo"
version="0.93"/>
<prover
id="coq"
name="Coq"
version="8.3pl2"/>
<prover
id="cvc3"
name="CVC3"
version="2.2"/>
<prover
id="gappa"
name="Gappa"
version="0.15.0"/>
<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="yices"
name="Yices"
version="1.0.25"/>
<prover
id="z3"
name="Z3"
version="2.19"/>
<file
name="../sorted_list.why"
verified="true"
expanded="true">
<theory
name="Order"
verified="true"
expanded="true">
</theory>
<theory
name="List"
verified="true"
expanded="true">
</theory>
<theory
name="SortedList"
verified="true"
expanded="true">
<goal