Commit c45528d4 authored by Jean-Christophe Filliâtre's avatar Jean-Christophe Filliâtre
Browse files

updated McCarthy's 91 example

parent ad638ed8
......@@ -13,7 +13,7 @@ module McCarthy91
f91 (f91 (n + 11))
else
n - 10
{ (n <= 100 /\ result = 91) \/ (n >= 101 /\ result = n - 10) }
{ result = if n <= 100 then 91 else n - 10 }
(* non-recursive implementation using a while loop *)
......@@ -21,7 +21,7 @@ module McCarthy91
use import module ref.Ref
use import int.Lex2
function f (x: int) : int = if x >= 101 then x-10 else 91
function f (x: int) : int = if x <= 100 then 91 else x-10
(* iter k x = f^k(x) *)
clone import int.Iter with type t = int, function f = f
......
<?xml version="1.0" encoding="UTF-8"?>
<!DOCTYPE why3session SYSTEM "why3session.dtd">
<why3session
name="programs/mccarthy/why3session.xml">
name="examples/programs/mccarthy/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"
id="2"
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"
id="3"
name="Z3"
version="2.19"/>
<prover
id="z3-3"
name="Z3"
version="3.2"/>
<file
name="../mccarthy.mlw"
verified="true"
expanded="true">
<theory
name="WP McCarthy91"
locfile="examples/programs/mccarthy/../mccarthy.mlw"
loclnum="4" loccnumb="7" loccnume="17"
verified="true"
expanded="true">
<goal
name="WP_parameter f91"
locfile="examples/programs/mccarthy/../mccarthy.mlw"
loclnum="10" loccnumb="10" loccnume="13"
expl="parameter f91"
sum="d2083d77525b9bb6f170c0e56335aada"
sum="67334438bff141dc6679a9a7fe9f47af"
proved="true"
expanded="false"
shape="iainfix <=V0c100ainfix =V2ainfix -V0c10Aainfix >=V0c101Oainfix =V2c91Aainfix <=V0c100Iainfix =V2ainfix -V1c10Aainfix >=V1c101Oainfix =V2c91Aainfix <=V1c100FAainfix <ainfix -c101V1ainfix -c101V0Aainfix <=c0ainfix -c101V0Iainfix =V1ainfix -ainfix +V0c11c10Aainfix >=ainfix +V0c11c101Oainfix =V1c91Aainfix <=ainfix +V0c11c100FAainfix <ainfix -c101ainfix +V0c11ainfix -c101V0Aainfix <=c0ainfix -c101V0ainfix =ainfix -V0c10ainfix -V0c10Aainfix >=V0c101Oainfix =ainfix -V0c10c91Aainfix <=V0c100F">
expanded="true"
shape="iainfix <=V0c100Liainfix <=ainfix +V0c11c100c91ainfix -ainfix +V0c11c10ainfix =iainfix <=V1c100c91ainfix -V1c10iainfix <=V0c100c91ainfix -V0c10Aainfix <ainfix -c101V1ainfix -c101V0Aainfix <=c0ainfix -c101V0Aainfix <ainfix -c101ainfix +V0c11ainfix -c101V0Aainfix <=c0ainfix -c101V0ainfix =ainfix -V0c10iainfix <=V0c100c91ainfix -V0c10F">
<label
name="expl:parameter f91">
</label>
<proof
prover="z3-2"
prover="3"
timelimit="2"
edited=""
obsolete="false">
<result status="valid" time="0.01"/>
obsolete="false"
archived="false">
<result status="valid" time="0.02"/>
</proof>
<proof
prover="cvc3-2.2"
prover="1"
timelimit="2"
edited=""
obsolete="false">
<result status="valid" time="0.00"/>
obsolete="false"
archived="false">
<result status="valid" time="0.02"/>
</proof>
<proof
prover="alt-ergo"
prover="0"
timelimit="2"
edited=""
obsolete="false">
<result status="valid" time="0.00"/>
obsolete="false"
archived="false">
<result status="valid" time="0.01"/>
</proof>
<proof
prover="simplify"
prover="2"
timelimit="2"
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 f91_nonrec"
locfile="examples/programs/mccarthy/../mccarthy.mlw"
loclnum="29" loccnumb="6" loccnume="16"
expl="parameter f91_nonrec"
sum="d63ac79f229fb22fb16fecce5521625d"
sum="3ad9ffda099012ef9a7ff69067cf39c1"
proved="true"
expanded="true"
shape="iainfix >V2c0iainfix >V1c100alexaTuple2ainfix +ainfix -c101V3ainfix *c10V4V4aTuple2ainfix +ainfix -c101V1ainfix *c10V2V2Aainfix =aiterV4V3afV0Aainfix >=V4c0Iainfix =V4ainfix -V2c1FIainfix =V3ainfix -V1c10FalexaTuple2ainfix +ainfix -c101V5ainfix *c10V6V6aTuple2ainfix +ainfix -c101V1ainfix *c10V2V2Aainfix =aiterV6V5afV0Aainfix >=V6c0Iainfix =V6ainfix +V2c1FIainfix =V5ainfix +V1c11Fainfix =V1afV0Iainfix =aiterV2V1afV0Aainfix >=V2c0FFAainfix =aiterc1V0afV0Aainfix >=c1c0F">
<label
name="expl:parameter f91_nonrec">
</label>
<transf
name="split_goal"
proved="true"
expanded="true">
<goal
name="WP_parameter f91_nonrec.1"
locfile="examples/programs/mccarthy/../mccarthy.mlw"
loclnum="29" loccnumb="6" loccnume="16"
expl="loop invariant init"
sum="7549d891ce7fe68249aee62ff1435b62"
sum="a4bc68a55252d1ed4d0b599eade8f592"
proved="true"
expanded="false"
expanded="true"
shape="ainfix =aiterc1V0afV0Aainfix >=c1c0F">
<label
name="expl:parameter f91_nonrec">
</label>
<proof
prover="z3-2"
prover="3"
timelimit="10"
edited=""
obsolete="false">
<result status="valid" time="0.00"/>
obsolete="false"
archived="false">
<result status="valid" time="0.01"/>
</proof>
<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">
<result status="valid" time="0.00"/>
obsolete="false"
archived="false">
<result status="valid" time="0.01"/>
</proof>
</goal>
<goal
name="WP_parameter f91_nonrec.2"
locfile="examples/programs/mccarthy/../mccarthy.mlw"
loclnum="29" loccnumb="6" loccnume="16"
expl="loop invariant preservation"
sum="a6926811f3cc84c7480b6b5c2320e35b"
sum="a099daab5b8fd22091dd354b30779929"
proved="true"
expanded="false"
expanded="true"
shape="ainfix =aiterV4V3afV0Aainfix >=V4c0Iainfix =V4ainfix -V2c1FIainfix =V3ainfix -V1c10FIainfix >V1c100Iainfix >V2c0Iainfix =aiterV2V1afV0Aainfix >=V2c0FFF">
<label
name="expl:parameter f91_nonrec">
</label>
<proof
prover="z3-2"
prover="3"
timelimit="10"
edited=""
obsolete="false">
<result status="valid" time="0.01"/>
obsolete="false"
archived="false">
<result status="valid" time="0.03"/>
</proof>
<proof
prover="cvc3-2.2"
prover="1"
timelimit="10"
edited=""
obsolete="false">
<result status="valid" time="0.01"/>
obsolete="false"
archived="false">
<result status="valid" time="0.02"/>
</proof>
<proof
prover="alt-ergo"
prover="0"
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 f91_nonrec.3"
locfile="examples/programs/mccarthy/../mccarthy.mlw"
loclnum="29" loccnumb="6" loccnume="16"
expl="loop variant decreases"
sum="2377b96b87b151bf0ff08639de66f9df"
sum="a5aec968960f73918ee216ec71dce767"
proved="true"
expanded="false"
expanded="true"
shape="alexaTuple2ainfix +ainfix -c101V3ainfix *c10V4V4aTuple2ainfix +ainfix -c101V1ainfix *c10V2V2Iainfix =aiterV4V3afV0Aainfix >=V4c0Iainfix =V4ainfix -V2c1FIainfix =V3ainfix -V1c10FIainfix >V1c100Iainfix >V2c0Iainfix =aiterV2V1afV0Aainfix >=V2c0FFF">
<label
name="expl:parameter f91_nonrec">
</label>
<proof
prover="z3-2"
prover="3"
timelimit="10"
edited=""
obsolete="false">
<result status="valid" time="0.02"/>
obsolete="false"
archived="false">
<result status="valid" time="0.03"/>
</proof>
<proof
prover="cvc3-2.2"
prover="1"
timelimit="10"
edited=""
obsolete="false">
<result status="valid" time="0.01"/>
obsolete="false"
archived="false">
<result status="valid" time="0.02"/>
</proof>
<proof
prover="alt-ergo"
prover="0"
timelimit="10"
edited=""
obsolete="false">
<result status="valid" time="0.00"/>
obsolete="false"
archived="false">
<result status="valid" time="0.02"/>
</proof>
</goal>
<goal
name="WP_parameter f91_nonrec.4"
locfile="examples/programs/mccarthy/../mccarthy.mlw"
loclnum="29" loccnumb="6" loccnume="16"
expl="loop invariant preservation"
sum="d16fd1bab97cb9d606198ac6d49db33b"
sum="f6917457ff621a597016f560e88a9233"
proved="true"
expanded="false"
expanded="true"
shape="ainfix =aiterV4V3afV0Aainfix >=V4c0Iainfix =V4ainfix +V2c1FIainfix =V3ainfix +V1c11FIainfix >V1c100NIainfix >V2c0Iainfix =aiterV2V1afV0Aainfix >=V2c0FFF">
<label
name="expl:parameter f91_nonrec">
</label>
<proof
prover="z3-2"
prover="3"
timelimit="10"
edited=""
obsolete="false">
<result status="valid" time="0.02"/>
obsolete="false"
archived="false">
<result status="valid" time="0.03"/>
</proof>
<proof
prover="cvc3-2.2"
prover="1"
timelimit="10"
edited=""
obsolete="false">
<result status="valid" time="0.02"/>
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.16"/>
obsolete="false"
archived="false">
<result status="valid" time="0.56"/>
</proof>
</goal>
<goal
name="WP_parameter f91_nonrec.5"
locfile="examples/programs/mccarthy/../mccarthy.mlw"
loclnum="29" loccnumb="6" loccnume="16"
expl="loop variant decreases"
sum="359940f497a48984e01e1cae18b88dc0"
sum="6a76d486a0ecd1f87a7a557dde586784"
proved="true"
expanded="false"
expanded="true"
shape="alexaTuple2ainfix +ainfix -c101V3ainfix *c10V4V4aTuple2ainfix +ainfix -c101V1ainfix *c10V2V2Iainfix =aiterV4V3afV0Aainfix >=V4c0Iainfix =V4ainfix +V2c1FIainfix =V3ainfix +V1c11FIainfix >V1c100NIainfix >V2c0Iainfix =aiterV2V1afV0Aainfix >=V2c0FFF">
<label
name="expl:parameter f91_nonrec">
</label>
<proof
prover="z3-2"
prover="3"
timelimit="10"
edited=""
obsolete="false">
<result status="valid" time="0.01"/>
obsolete="false"
archived="false">
<result status="valid" time="0.02"/>
</proof>
<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.02"/>
</proof>
<proof
prover="alt-ergo"
prover="0"
timelimit="10"
edited=""
obsolete="false">
<result status="valid" time="0.01"/>
obsolete="false"
archived="false">
<result status="valid" time="0.02"/>
</proof>
</goal>
<goal
name="WP_parameter f91_nonrec.6"
locfile="examples/programs/mccarthy/../mccarthy.mlw"
loclnum="29" loccnumb="6" loccnume="16"
expl="normal postcondition"
sum="dfbecf43c71054001704a6a83199312b"
sum="2293be5163de7c6b53ca78ce1011b125"
proved="true"
expanded="false"
expanded="true"
shape="ainfix =V1afV0Iainfix >V2c0NIainfix =aiterV2V1afV0Aainfix >=V2c0FFF">
<label
name="expl:parameter f91_nonrec">
</label>
<proof
prover="z3-2"
prover="3"
timelimit="10"
edited=""
obsolete="false">
<result status="valid" time="0.01"/>
obsolete="false"
archived="false">
<result status="valid" time="0.03"/>
</proof>
<proof
prover="cvc3-2.2"
prover="1"
timelimit="10"
edited=""
obsolete="false">
obsolete="false"
archived="false">
<result status="valid" time="0.02"/>
</proof>
<proof
prover="alt-ergo"
prover="0"
timelimit="10"
edited=""
obsolete="false">
obsolete="false"
archived="false">
<result status="valid" time="0.00"/>
</proof>
</goal>
......
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