Commit 37ec2123 authored by Andrei Paskevich's avatar Andrei Paskevich

update proof sessions

parent 6ee0ec51
......@@ -158,10 +158,8 @@ why3.conf
/examples/programs/algo64/
/examples/programs/algo65/
/examples/programs/binary_search_c/
/examples/programs/bresenham/
/examples/programs/dijkstra/
/examples/programs/distance/
/examples/programs/sf/
# modules
/modules/string/
......
<?xml version="1.0" encoding="UTF-8"?>
<!DOCTYPE why3session SYSTEM "why3session.dtd">
<why3session name="my_cosine/why3session.xml">
<why3session name="examples/my_cosine/why3session.xml">
<file name="../my_cosine.why" verified="true" expanded="true">
<theory name="CosineSingle" verified="true" expanded="true">
<goal name="MethodError" sum="04d7ba2ad67e6273c77266e812fe0b5d" proved="true" expanded="true">
<proof prover="coq" timelimit="2" edited="my_cosine_CosineSingle_MethodError_1.v" obsolete="false">
<result status="valid" time="4.29"/>
</proof>
<proof prover="alt-ergo" timelimit="10" edited="" obsolete="false">
<result status="timeout" time="10.04"/>
</proof>
<proof prover="simplify" timelimit="10" edited="" obsolete="false">
<result status="timeout" time="10.06"/>
</proof>
<proof prover="z3" timelimit="10" edited="" obsolete="false">
<result status="timeout" time="10.06"/>
<result status="valid" time="3.63"/>
</proof>
</goal>
<goal name="TotalErrorFullyExpanded" sum="86136c1aa7501342a2789f26b4088e3b" proved="true" expanded="true">
<proof prover="alt-ergo" timelimit="10" edited="" obsolete="false">
<result status="timeout" time="10.01"/>
</proof>
<proof prover="simplify" timelimit="10" edited="" obsolete="false">
<result status="timeout" time="10.09"/>
</proof>
<proof prover="gappa" timelimit="2" edited="" obsolete="false">
<result status="valid" time="0.02"/>
</proof>
<proof prover="z3" timelimit="10" edited="" obsolete="false">
<result status="timeout" time="10.06"/>
<result status="valid" time="0.01"/>
</proof>
</goal>
<goal name="TotalErrorExpanded" sum="1d2075874f81d542bc1500ae6147faec" proved="true" expanded="true">
<proof prover="alt-ergo" timelimit="2" edited="" obsolete="false">
<result status="valid" time="0.98"/>
</proof>
<proof prover="simplify" timelimit="10" edited="" obsolete="false">
<result status="timeout" time="10.11"/>
</proof>
<proof prover="z3" timelimit="2" edited="" obsolete="false">
<result status="valid" time="0.12"/>
<result status="valid" time="0.72"/>
</proof>
</goal>
<goal name="TotalError" sum="84d328c047b191246fda42eaa2ab5255" proved="true" expanded="true">
<proof prover="alt-ergo" timelimit="10" edited="" obsolete="false">
<result status="valid" time="2.73"/>
</proof>
<proof prover="simplify" timelimit="10" edited="" obsolete="false">
<result status="timeout" time="10.03"/>
</proof>
<proof prover="z3" timelimit="10" edited="" obsolete="false">
<result status="timeout" time="10.12"/>
<result status="valid" time="2.06"/>
</proof>
</goal>
</theory>
......
This diff is collapsed.
(* This file is generated by Why3's Coq driver *)
(* Beware! Only edit allowed sections below *)
Require Import ZArith.
Require Import Rbase.
Definition unit := unit.
Parameter mark : Type.
Parameter at1: forall (a:Type), a -> mark -> a.
Implicit Arguments at1.
Parameter old: forall (a:Type), a -> a.
Implicit Arguments old.
Inductive ref (a:Type) :=
| mk_ref : a -> ref a.
Implicit Arguments mk_ref.
Definition contents (a:Type)(u:(ref a)): a :=
match u with
| mk_ref contents1 => contents1
end.
Implicit Arguments contents.
Inductive even : Z -> Prop :=
| even_0 : (even 0%Z)
| even_odd : forall (x:Z), (even x) -> (even (x + 2%Z)%Z).
Theorem even_not_odd : forall (x:Z), (even x) -> ~ (even (x + 1%Z)%Z).
(* YOU MAY EDIT THE PROOF BELOW *)
assert (nonneg: forall x:Z, even x -> (x >= 0)%Z).
induction 1; auto with *.
induction 1.
red; intro.
inversion H.
assert (h: (x = -1)%Z) by omega.
absurd (-1 >= 0)%Z.
omega.
apply nonneg.
rewrite <- h; auto.
intuition.
inversion H0.
assert (h: (x = -3)%Z) by omega.
absurd (-3 >= 0)%Z.
omega.
apply nonneg.
rewrite <- h; auto.
assert (x0 = x+1)%Z by omega.
subst x0; auto.
Qed.
(* DO NOT EDIT BELOW *)
......@@ -20,7 +20,7 @@
</goal>
<goal name="even_not_odd" sum="53e6bf87df0a78f77396dc37febf9ad4" proved="true" expanded="true">
<proof prover="coq" timelimit="10" edited="sf_WP_HoareLogic_even_not_odd_1.v" obsolete="false">
<result status="valid" time="0.65"/>
<result status="valid" time="0.52"/>
</proof>
</goal>
<goal name="WP_parameter parity" expl="correctness of parameter parity" sum="f0ebcfc44576c91bca3ab0d6fc1ea8de" proved="true" expanded="true">
......@@ -46,9 +46,53 @@
</proof>
</goal>
<goal name="WP_parameter list_member" expl="correctness of parameter list_member" sum="b4187b983e65459b73a851378ae0705f" proved="true" expanded="true">
<proof prover="yices" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.04"/>
</proof>
<transf name="split_goal" proved="true" expanded="true">
<goal name="WP_parameter list_member.1" expl="loop invariant init" sum="31f4e55cabffdd4d63e20199d1a77867" proved="true" expanded="true">
<proof prover="alt-ergo" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.01"/>
</proof>
</goal>
<goal name="WP_parameter list_member.2" expl="precondition" sum="edfdcfe23487d8d0453cb4a42accae64" proved="true" expanded="true">
<proof prover="alt-ergo" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.01"/>
</proof>
</goal>
<goal name="WP_parameter list_member.3" expl="precondition" sum="58f178b2f8c525bf8edc57ed7808237d" proved="true" expanded="true">
<proof prover="alt-ergo" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.01"/>
</proof>
</goal>
<goal name="WP_parameter list_member.4" expl="loop invariant preservation" sum="927d4cc123030bc09cf89d7be84c6724" proved="true" expanded="true">
<proof prover="z3" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.67"/>
</proof>
</goal>
<goal name="WP_parameter list_member.5" expl="loop variant decreases" sum="6bbef49de1a1b1573727678eefae860e" proved="true" expanded="true">
<proof prover="alt-ergo" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.02"/>
</proof>
</goal>
<goal name="WP_parameter list_member.6" expl="precondition" sum="0e12c88f2567c5f0aea89a6304cd0642" proved="true" expanded="true">
<proof prover="alt-ergo" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.01"/>
</proof>
</goal>
<goal name="WP_parameter list_member.7" expl="loop invariant preservation" sum="7f5d2ee098045d0c9285ac28dfa83a7d" proved="true" expanded="true">
<proof prover="z3" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.67"/>
</proof>
</goal>
<goal name="WP_parameter list_member.8" expl="loop variant decreases" sum="c067362f1067ed1aaabae3ef66460a35" proved="true" expanded="true">
<proof prover="alt-ergo" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.03"/>
</proof>
</goal>
<goal name="WP_parameter list_member.9" expl="normal postcondition" sum="911c750ca19f35b9e7d64137fb7d7a4a" proved="true" expanded="true">
<proof prover="alt-ergo" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.01"/>
</proof>
</goal>
</transf>
</goal>
</theory>
</file>
......
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