Skip to content

GitLab

why3
why3
Commit d6c29088 authored by MARCHE Claude's avatar MARCHE Claude
Browse files
Options

regression tests script, and a few more examples

parent 2890726c
Hide whitespace changes
Inline Side-by-side
Showing with 562 additions and 21 deletions
.gitignore
View file @ d6c29088
......@@ -147,7 +147,6 @@ why.conf
# /examples/
/examples/my_cosine/
/examples/genealogy/
/examples/programs/isqrt/
/examples/programs/course/
/examples/programs/wcet_hull/
/examples/programs/my_cosine/
......@@ -172,7 +171,6 @@ why.conf
/examples/programs/dijkstra/
/examples/programs/distance/
/examples/programs/flag/
/examples/programs/gcd_bezout/
/examples/programs/sf/
/examples/programs/vstte10_queens/
......
examples/hello_proof/why3session.xml
View file @ d6c29088
......@@ -4,41 +4,41 @@
<file name="../hello_proof.why" verified="false" expanded="true">
<theory name="HelloProof" verified="false" expanded="true">
<goal name="G1" sum="f81584706e28397114f2508adf6dd2ff" proved="true" expanded="true">
<proof prover="simplify" edited="" obsolete="false">
<proof prover="simplify" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.01"/>
</proof>
</goal>
<goal name="G2" sum="0bb17dc8e6f26a1a6aaf5ecf8ed5a5a8" proved="false" expanded="true">
<proof prover="alt-ergo" edited="" obsolete="false">
<proof prover="alt-ergo" timelimit="10" edited="" obsolete="false">
<result status="unknown" time="0.02"/>
</proof>
<proof prover="simplify" edited="" obsolete="false">
<proof prover="simplify" timelimit="10" edited="" obsolete="false">
<result status="unknown" time="0.01"/>
</proof>
<transf name="split_goal" proved="false" expanded="true">
<goal name="G2.1" sum="54b5fc27ec93fbe413651f6064794e54" proved="false" expanded="true">
<proof prover="coq" edited="" obsolete="false">
<proof prover="coq" timelimit="10" edited="" obsolete="false">
<result status="unknown" time="0.46"/>
</proof>
<proof prover="alt-ergo" edited="" obsolete="false">
<proof prover="alt-ergo" timelimit="10" edited="" obsolete="false">
<result status="unknown" time="0.02"/>
</proof>
<proof prover="simplify" edited="" obsolete="false">
<proof prover="simplify" timelimit="10" edited="" obsolete="false">
<result status="unknown" time="0.01"/>
</proof>
</goal>
<goal name="G2.2" sum="6cdd03a110385f45423b1683748dce81" proved="true" expanded="true">
<proof prover="simplify" edited="" obsolete="false">
<proof prover="simplify" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.01"/>
</proof>
</goal>
</transf>
</goal>
<goal name="G3" sum="b3b51b7bb0acfa332bfb937bfa017230" proved="true" expanded="true">
<proof prover="alt-ergo" edited="" obsolete="false">
<proof prover="alt-ergo" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.01"/>
</proof>
<proof prover="simplify" edited="" obsolete="false">
<proof prover="simplify" timelimit="10" edited="" obsolete="false">
<result status="unknown" time="0.01"/>
</proof>
</goal>
......
examples/programs/gcd/why3session.xml 0 → 100644
View file @ d6c29088
<?xml version="1.0" encoding="UTF-8"?>
<!DOCTYPE why3session SYSTEM "why3session.dtd">
<why3session name="programs/gcd/why3session.xml">
<file name="../gcd.mlw" verified="false" expanded="true">
<theory name="M" verified="false" expanded="true">
<goal name="WP_parameter gcd" expl="correctness of parameter gcd" sum="665cff5a35980903b7a8eb517c404e17" proved="false" expanded="true">
<proof prover="cvc3" timelimit="2" edited="" obsolete="false">
<result status="timeout" time="2.08"/>
</proof>
<proof prover="simplify" timelimit="2" edited="" obsolete="false">
<result status="timeout" time="2.09"/>
</proof>
<proof prover="alt-ergo" timelimit="2" edited="" obsolete="false">
<result status="unknown" time="0.34"/>
</proof>
<proof prover="z3" timelimit="2" edited="" obsolete="false">
<result status="timeout" time="2.09"/>
</proof>
<transf name="split_goal" proved="false" expanded="true">
<goal name="WP_parameter gcd.1" expl="normal postcondition" sum="d6c14b7052f661d1db3c5517270a214e" proved="true" expanded="true">
<proof prover="cvc3" timelimit="2" edited="" obsolete="false">
<result status="valid" time="0.02"/>
</proof>
<proof prover="alt-ergo" timelimit="2" edited="" obsolete="false">
<result status="valid" time="0.01"/>
</proof>
<proof prover="simplify" timelimit="2" edited="" obsolete="false">
<result status="valid" time="0.02"/>
</proof>
<proof prover="z3" timelimit="2" edited="" obsolete="false">
<result status="valid" time="0.03"/>
</proof>
</goal>
<goal name="WP_parameter gcd.2" expl="precondition" sum="ac183d41241c6eaf028e3626e0097b97" proved="true" expanded="true">
<proof prover="cvc3" timelimit="2" edited="" obsolete="false">
<result status="valid" time="0.02"/>
</proof>
<proof prover="alt-ergo" timelimit="2" edited="" obsolete="false">
<result status="valid" time="0.01"/>
</proof>
<proof prover="simplify" timelimit="2" edited="" obsolete="false">
<result status="valid" time="0.02"/>
</proof>
<proof prover="z3" timelimit="2" edited="" obsolete="false">
<result status="valid" time="0.03"/>
</proof>
</goal>
<goal name="WP_parameter gcd.3" expl="normal postcondition" sum="7e7d74481a07874402868ca8e73fb044" proved="false" expanded="true">
<proof prover="cvc3" timelimit="2" edited="" obsolete="false">
<result status="unknown" time="1.16"/>
</proof>
<proof prover="alt-ergo" timelimit="2" edited="" obsolete="false">
<result status="unknown" time="0.42"/>
</proof>
<proof prover="simplify" timelimit="2" edited="" obsolete="false">
<result status="timeout" time="2.08"/>
</proof>
<proof prover="z3" timelimit="2" edited="" obsolete="false">
<result status="timeout" time="2.08"/>
</proof>
</goal>
</transf>
</goal>
</theory>
</file>
</why3session>
examples/programs/gcd_bezout/why3session.xml 0 → 100644
View file @ d6c29088
<?xml version="1.0" encoding="UTF-8"?>
<!DOCTYPE why3session SYSTEM "why3session.dtd">
<why3session name="programs/gcd_bezout/why3session.xml">
<file name="../gcd_bezout.mlw" verified="false" expanded="true">
<theory name="M" verified="false" expanded="true">
<goal name="WP_parameter gcd" expl="correctness of parameter gcd" sum="44c73ab6d7cb8f3f8241f534deb156f1" proved="false" expanded="true">
<proof prover="alt-ergo" timelimit="2" edited="" obsolete="false">
<result status="timeout" time="2.09"/>
</proof>
<proof prover="cvc3" timelimit="2" edited="" obsolete="false">
<result status="timeout" time="2.09"/>
</proof>
<proof prover="simplify" timelimit="2" edited="" obsolete="false">
<result status="timeout" time="2.09"/>
</proof>
<proof prover="z3" timelimit="2" edited="" obsolete="false">
<result status="highfailure" time="0.30"/>
</proof>
<transf name="split_goal" proved="false" expanded="true">
<goal name="WP_parameter gcd.1" expl="loop invariant init" sum="8566a02a986fda736b7f696339e845f1" proved="true" expanded="false">
<proof prover="simplify" timelimit="2" edited="" obsolete="false">
<result status="valid" time="0.01"/>
</proof>
<proof prover="cvc3" timelimit="2" edited="" obsolete="false">
<result status="valid" time="0.02"/>
</proof>
<proof prover="alt-ergo" timelimit="2" edited="" obsolete="false">
<result status="valid" time="0.02"/>
</proof>
<proof prover="z3" timelimit="2" edited="" obsolete="false">
<result status="valid" time="0.02"/>
</proof>
</goal>
<goal name="WP_parameter gcd.2" expl="loop invariant preservation" sum="6aa9c41319e3ce9cdb5c07f21e43fc1a" proved="false" expanded="true">
<proof prover="simplify" timelimit="2" edited="" obsolete="false">
<result status="timeout" time="2.08"/>
</proof>
<proof prover="cvc3" timelimit="2" edited="" obsolete="false">
<result status="timeout" time="2.06"/>
</proof>
<proof prover="alt-ergo" timelimit="2" edited="" obsolete="false">
<result status="timeout" time="2.11"/>
</proof>
<proof prover="z3" timelimit="2" edited="" obsolete="false">
<result status="timeout" time="2.09"/>
</proof>
</goal>
<goal name="WP_parameter gcd.3" expl="loop variant decreases" sum="cca2a902409976d7fe1249041e32fc6e" proved="true" expanded="false">
<proof prover="simplify" timelimit="2" edited="" obsolete="false">
<result status="valid" time="0.02"/>
</proof>
<proof prover="cvc3" timelimit="2" edited="" obsolete="false">
<result status="valid" time="0.09"/>
</proof>
<proof prover="alt-ergo" timelimit="2" edited="" obsolete="false">
<result status="timeout" time="2.02"/>
</proof>
<proof prover="z3" timelimit="2" edited="" obsolete="false">
<result status="valid" time="0.04"/>
</proof>
</goal>
<goal name="WP_parameter gcd.4" expl="normal postcondition" sum="70282398b1f17ace6b7f8ea5e5755ba1" proved="true" expanded="false">
<proof prover="simplify" timelimit="2" edited="" obsolete="false">
<result status="valid" time="0.02"/>
</proof>
<proof prover="cvc3" timelimit="2" edited="" obsolete="false">
<result status="unknown" time="0.72"/>
</proof>
<proof prover="alt-ergo" timelimit="2" edited="" obsolete="false">
<result status="valid" time="1.14"/>
</proof>
<proof prover="z3" timelimit="2" edited="" obsolete="false">
<result status="timeout" time="2.09"/>
</proof>
</goal>
</transf>
</goal>
</theory>
</file>
</why3session>
examples/programs/isqrt/isqrt.mlw_M_WP_isqrt_1.v 0 → 100644
View file @ d6c29088
(* Beware! Only edit allowed sections below *)
(* This file is generated by Why3's Coq driver *)
Require Import ZArith.
Require Import Rbase.
Parameter ghost : forall (a:Type), Type.
Definition unit := unit.
Parameter ignore: forall (a:Type), a -> unit.
Implicit Arguments ignore.
Parameter label_ : Type.
Parameter at1: forall (a:Type), a -> label_ -> a.
Implicit Arguments at1.
Parameter old: forall (a:Type), a -> a.
Implicit Arguments old.
Parameter ref : forall (a:Type), Type.
Definition sqr(x:Z): Z := (x * x)%Z.
Theorem WP_isqrt : forall (x:Z), (0%Z <= x)%Z -> forall (result:Z),
(result = 0%Z) -> forall (result1:Z), (result1 = 1%Z) ->
(((0%Z <= result)%Z /\ (((sqr result) <= x)%Z /\
(result1 = (sqr (result + 1%Z)%Z)))) -> forall (sum:Z), forall (count:Z),
((0%Z <= count)%Z /\ (((sqr count) <= x)%Z /\
(sum = (sqr (count + 1%Z)%Z)))) -> forall (result2:Z), (result2 = sum) ->
((result2 <= x)%Z -> forall (result3:Z), (result3 = count) ->
forall (count1:Z), (count1 = (result3 + 1%Z)%Z) -> forall (result4:Z),
(result4 = sum) -> forall (result5:Z), (result5 = count1) ->
forall (sum1:Z), (sum1 = ((result4 + (2%Z * result5)%Z)%Z + 1%Z)%Z) ->
(((0%Z <= count1)%Z /\ (((sqr count1) <= x)%Z /\
(sum1 = (sqr (count1 + 1%Z)%Z)))) -> (0%Z <= (x - count)%Z)%Z))).
(* YOU MAY EDIT THE PROOF BELOW *)
intros.
Qed.
(* DO NOT EDIT BELOW *)
examples/programs/isqrt/isqrt.mlw_M_WP_main_1.v 0 → 100644
View file @ d6c29088
(* Beware! Only edit allowed sections below *)
(* This file is generated by Why3's Coq driver *)
Require Import ZArith.
Require Import Rbase.
Parameter ghost : forall (a:Type), Type.
Definition unit := unit.
Parameter ignore: forall (a:Type), a -> unit.
Implicit Arguments ignore.
Parameter label_ : Type.
Parameter at1: forall (a:Type), a -> label_ -> a.
Implicit Arguments at1.
Parameter old: forall (a:Type), a -> a.
Implicit Arguments old.
Parameter ref : forall (a:Type), Type.
Definition sqr(x:Z): Z := (x * x)%Z.
Theorem WP_main : (0%Z <= 17%Z)%Z /\ forall (result:Z), ((0%Z <= result)%Z /\
(((sqr result) <= 17%Z)%Z /\ (17%Z < (sqr (result + 1%Z)%Z))%Z)) ->
(result = 4%Z).
(* YOU MAY EDIT THE PROOF BELOW *)
intros.
Qed.
(* DO NOT EDIT BELOW *)
examples/programs/isqrt/isqrt.mlw_M_WP_main_2.v 0 → 100644
View file @ d6c29088
(* Beware! Only edit allowed sections below *)
(* This file is generated by Why3's Coq driver *)
Require Import ZArith.
Require Import Rbase.
Parameter ghost : forall (a:Type), Type.
Definition unit := unit.
Parameter ignore: forall (a:Type), a -> unit.
Implicit Arguments ignore.
Parameter label_ : Type.
Parameter at1: forall (a:Type), a -> label_ -> a.
Implicit Arguments at1.
Parameter old: forall (a:Type), a -> a.
Implicit Arguments old.
Parameter ref : forall (a:Type), Type.
Definition sqr(x:Z): Z := (x * x)%Z.
Theorem WP_main : (0%Z <= 17%Z)%Z -> forall (result:Z), ((0%Z <= result)%Z /\
(((sqr result) <= 17%Z)%Z /\ (17%Z < (sqr (result + 1%Z)%Z))%Z)) ->
(result = 4%Z).
(* YOU MAY EDIT THE PROOF BELOW *)
intros.
assert (h:(result < 4 \/ result = 4 \/ result > 4)%Z) by omega.
destruct h as [h1|[h2|h3]]; auto.
Qed.
(* DO NOT EDIT BELOW *)
examples/programs/isqrt/why3session.xml 0 → 100644
View file @ d6c29088
<?xml version="1.0" encoding="UTF-8"?>
<!DOCTYPE why3session SYSTEM "why3session.dtd">
<why3session name="programs/isqrt/why3session.xml">
<file name="../isqrt.mlw" verified="true" expanded="true">
<theory name="M" verified="true" expanded="true">
<goal name="WP_parameter isqrt" expl="correctness of parameter isqrt" sum="510de4257915daa3e680ba4e3c8515f1" proved="true" expanded="true">
<proof prover="cvc3" timelimit="2" edited="" obsolete="false">
<result status="valid" time="0.04"/>
</proof>
<proof prover="simplify" timelimit="2" edited="" obsolete="false">
<result status="unknown" time="0.02"/>
</proof>
<proof prover="alt-ergo" timelimit="2" edited="" obsolete="false">
<result status="valid" time="0.12"/>
</proof>
<proof prover="z3" timelimit="2" edited="" obsolete="false">
<result status="valid" time="0.03"/>
</proof>
</goal>
<goal name="WP_parameter main" expl="correctness of parameter main" sum="fad1c189aa702c8c6c682810d5ecf636" proved="true" expanded="true">
<proof prover="cvc3" timelimit="2" edited="" obsolete="false">
<result status="unknown" time="0.11"/>
</proof>
<proof prover="simplify" timelimit="2" edited="" obsolete="false">
<result status="unknown" time="0.02"/>
</proof>
<proof prover="alt-ergo" timelimit="2" edited="" obsolete="false">
<result status="unknown" time="0.02"/>
</proof>
<proof prover="z3" timelimit="2" edited="" obsolete="false">
<result status="valid" time="0.02"/>
</proof>
</goal>
</theory>
</file>
</why3session>
examples/programs/mac_carthy/why3session.xml 0 → 100644
View file @ d6c29088
<?xml version="1.0" encoding="UTF-8"?>
<!DOCTYPE why3session SYSTEM "why3session.dtd">
<why3session name="programs/mac_carthy/why3session.xml">
<file name="../mac_carthy.mlw" verified="true" expanded="true">
<theory name="M" verified="true" expanded="true">
<goal name="WP_parameter f91" expl="correctness of parameter f91" sum="d76ec4e4b18463778c1d69a5f339cd5b" proved="true" expanded="true">
<proof prover="cvc3" timelimit="2" edited="" obsolete="false">
<result status="valid" time="0.02"/>
</proof>
<proof prover="alt-ergo" timelimit="2" edited="" obsolete="false">
<result status="valid" time="0.01"/>
</proof>
<proof prover="simplify" timelimit="2" edited="" obsolete="false">
<result status="valid" time="0.01"/>
</proof>
<proof prover="z3" timelimit="2" edited="" obsolete="false">
<result status="valid" time="0.02"/>
</proof>
</goal>
<goal name="WP_parameter f91_nonrec" expl="correctness of parameter f91_nonrec" sum="0a7c396695b0240cd521dde6e0557c36" proved="true" expanded="true">
<proof prover="cvc3" timelimit="2" edited="" obsolete="false">
<result status="valid" time="0.08"/>
</proof>
<proof prover="alt-ergo" timelimit="2" edited="" obsolete="false">
<result status="valid" time="1.46"/>
</proof>
<proof prover="simplify" timelimit="2" edited="" obsolete="false">
<result status="valid" time="0.02"/>
</proof>
<proof prover="z3" timelimit="2" edited="" obsolete="false">
<result status="valid" time="0.03"/>
</proof>
</goal>
</theory>
</file>
</why3session>
examples/programs/power/power.mlw_Power_Power_mult_2.v 0 → 100644
View file @ d6c29088
(* Beware! Only edit allowed sections below *)
(* This file is generated by Why3's Coq driver *)
Require Import ZArith.
Require Import Rbase.
Parameter ghost : forall (a:Type), Type.
Definition unit := unit.
Parameter ignore: forall (a:Type), a -> unit.
Implicit Arguments ignore.
Parameter label_ : Type.
Parameter at1: forall (a:Type), a -> label_ -> a.
Implicit Arguments at1.
Parameter old: forall (a:Type), a -> a.
Implicit Arguments old.
Parameter power: Z -> Z -> Z.
Axiom Power_0 : forall (x:Z), ((power x 0%Z) = 1%Z).
Axiom Power_s : forall (x:Z) (n:Z), (0%Z < n)%Z -> ((power x
n) = (x * (power x (n - 1%Z)%Z))%Z).
Axiom Power_1 : forall (x:Z), ((power x 1%Z) = x).
Axiom Power_sum : forall (x:Z) (n:Z) (m:Z), (0%Z <= n)%Z -> ((0%Z <= m)%Z ->
((power x (n + m)%Z) = ((power x n) * (power x m))%Z)).
Theorem Power_mult : forall (x:Z) (n:Z) (m:Z), (0%Z <= n)%Z ->
((0%Z <= m)%Z -> ((power x (n * m)%Z) = (power (power x n) m))).
(* YOU MAY EDIT THE PROOF BELOW *)
admit.
Qed.
(* DO NOT EDIT BELOW *)
examples/programs/power/power.mlw_Power_Power_sum_2.v 0 → 100644
View file @ d6c29088
(* Beware! Only edit allowed sections below *)
(* This file is generated by Why3's Coq driver *)
Require Import ZArith.
Require Import Rbase.
Parameter ghost : forall (a:Type), Type.
Definition unit := unit.
Parameter ignore: forall (a:Type), a -> unit.
Implicit Arguments ignore.
Parameter label_ : Type.
Parameter at1: forall (a:Type), a -> label_ -> a.
Implicit Arguments at1.
Parameter old: forall (a:Type), a -> a.
Implicit Arguments old.
Parameter power: Z -> Z -> Z.
Axiom Power_0 : forall (x:Z), ((power x 0%Z) = 1%Z).
Axiom Power_s : forall (x:Z) (n:Z), (0%Z < n)%Z -> ((power x
n) = (x * (power x (n - 1%Z)%Z))%Z).
Axiom Power_1 : forall (x:Z), ((power x 1%Z) = x).
Theorem Power_sum : forall (x:Z) (n:Z) (m:Z), (0%Z <= n)%Z ->
((0%Z <= m)%Z -> ((power x (n + m)%Z) = ((power x n) * (power x m))%Z)).
(* YOU MAY EDIT THE PROOF BELOW *)
intros x n m Hn Hm.
generalize Hm.
pattern m.
apply Z_lt_induction; auto.
intros n0 Hind Hn0.
assert (h:(n0 = 0 \/ n0 > 0)%Z) by omega.
destruct h.
subst n0; rewrite Power_0; ring_simplify (n+0)%Z; ring.
rewrite Power_s; auto with zarith.
replace (n+n0-1)%Z with (n+(n0-1))%Z by omega.
rewrite Hind; auto with zarith.
rewrite (Power_s x n0).
ring.
omega.
Qed.
(* DO NOT EDIT BELOW *)
examples/programs/power/why3session.xml 0 → 100644
View file @ d6c29088
<?xml version="1.0" encoding="UTF-8"?>
<!DOCTYPE why3session SYSTEM "why3session.dtd">
<why3session name="programs/power/why3session.xml">
<file name="../power.mlw" verified="false" expanded="true">
<theory name="Power" verified="false" expanded="true">
<goal name="Power_1" sum="1db7c130e0faaa3525077846831aadf3" proved="true" expanded="false">
<proof prover="cvc3" timelimit="2" edited="" obsolete="false">
<result status="valid" time="0.01"/>
</proof>
<proof prover="simplify" timelimit="2" edited="" obsolete="false">
<result status="unknown" time="0.01"/>
</proof>
<proof prover="alt-ergo" timelimit="2" edited="" obsolete="false">
<result status="valid" time="0.01"/>
</proof>
<proof prover="z3" timelimit="2" edited="" obsolete="false">
<result status="valid" time="0.02"/>
</proof>
</goal>
<goal name="Power_sum" sum="0222179599018e583f47a3d214f2e604" proved="false" expanded="true">
<proof prover="cvc3" timelimit="2" edited="" obsolete="false">
<result status="timeout" time="2.08"/>
</proof>
<proof prover="simplify" timelimit="2" edited="" obsolete="false">
<result status="unknown" time="0.01"/>
</proof>
<proof prover="alt-ergo" timelimit="2" edited="" obsolete="false">
<result status="timeout" time="2.09"/>
</proof>
<proof prover="z3" timelimit="2" edited="" obsolete="false">
<result status="timeout" time="2.07"/>
</proof>
</goal>
<goal name="Power_mult" sum="9d09d633adb75294ad19c24d7ad24bf4" proved="false" expanded="true">
<proof prover="cvc3" timelimit="2" edited="" obsolete="false">
<result status="unknown" time="1.50"/>
</proof>
<proof prover="simplify" timelimit="2" edited="" obsolete="false">
<result status="unknown" time="0.01"/>
</proof>
<proof prover="alt-ergo" timelimit="2" edited="" obsolete="false">
<result status="unknown" time="0.15"/>
</proof>
<proof prover="z3" timelimit="2" edited="" obsolete="false">
<result status="timeout" time="2.08"/>
</proof>
</goal>
</theory>
<theory name="M" verified="false" expanded="true">
<goal name="WP_parameter fast_exp" expl="correctness of parameter fast_exp" sum="ff0a5f4d7ce2252d7f09664075c560a8" proved="true" expanded="false">
<proof prover="cvc3" timelimit="2" edited="" obsolete="false">
<result status="timeout" time="2.08"/>
</proof>
<proof prover="simplify" timelimit="2" edited="" obsolete="false">
<result status="timeout" time="2.08"/>
</proof>
<proof prover="alt-ergo" timelimit="2" edited="" obsolete="false">
<result status="valid" time="0.10"/>
</proof>
<proof prover="z3" timelimit="2" edited="" obsolete="false">
<result status="timeout" time="2.08"/>
</proof>
</goal>