Commit 1b49eb9d authored by Andrei Paskevich's avatar Andrei Paskevich

move proof sessions for the standard library files to examples/stdlib

parent e24dac47
......@@ -59,9 +59,6 @@ why3.conf
/bin/why3config.byte
/bin/why3config.opt
/bin/why3config
/bin/why3bench.byte
/bin/why3bench.opt
/bin/why3bench
/bin/why3doc.byte
/bin/why3doc.opt
/bin/why3doc
......
......@@ -64,7 +64,7 @@ run_dir () {
}
echo "=== Standard Library ==="
run_dir ../lib/why3
run_dir stdlib
echo ""
echo "=== Tests ==="
......
<?xml version="1.0" encoding="UTF-8"?>
<!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN"
"http://why3.lri.fr/why3session.dtd">
<why3session shape_version="4">
<prover id="0" name="Alt-Ergo" version="0.95.2" timelimit="6" memlimit="1000"/>
<file name="../../../theories/bintree.why" expanded="true">
<theory name="Tree" sum="208c972190eb44f8b7351a2a7178896b">
</theory>
<theory name="Size" sum="1b4362b7d1c7f5d591b7cebb29436eb3" expanded="true">
<goal name="size_nonneg" expanded="true">
<transf name="induction_ty_lex" expanded="true">
<goal name="size_nonneg.1" expl="1." expanded="true">
<proof prover="0"><result status="valid" time="0.01"/></proof>
</goal>
</transf>
</goal>
<goal name="size_empty" expanded="true">
<transf name="induction_ty_lex" expanded="true">
<goal name="size_empty.1" expl="1.">
<proof prover="0"><result status="valid" time="0.01"/></proof>
</goal>
</transf>
</goal>
</theory>
<theory name="Occ" sum="28b23ceca3e03201b4d6c1cb076df8df" expanded="true">
<goal name="occ_nonneg" expanded="true">
<transf name="induction_ty_lex" expanded="true">
<goal name="occ_nonneg.1" expl="1." expanded="true">
<proof prover="0"><result status="valid" time="0.01"/></proof>
</goal>
</transf>
</goal>
</theory>
<theory name="Inorder" sum="2d88f35ea90c25deb909cfdd20759a20">
</theory>
<theory name="Preorder" sum="8e4a9c3c1f301dc9f0123151fd0ef6df">
</theory>
<theory name="InorderLength" sum="705873080e4ccf1add2d294ce9d1af26" expanded="true">
<goal name="inorder_length" expanded="true">
<transf name="induction_ty_lex" expanded="true">
<goal name="inorder_length.1" expl="1." expanded="true">
<proof prover="0"><result status="valid" time="0.01"/></proof>
</goal>
</transf>
</goal>
</theory>
<theory name="Zipper" sum="5ac1b9482fd084daf1b2d94fa61274e1">
</theory>
</file>
</why3session>
<?xml version="1.0" encoding="UTF-8"?>
<!DOCTYPE why3session PUBLIC "-//Why3//proof session v2//EN" "http://why3.lri.fr/why3session.dtd">
<why3session shape_version="4">
<prover
id="0"
name="Alt-Ergo"
version="0.95.2"/>
<file
name="../bintree.why"
verified="true"
expanded="true">
<theory
name="Tree"
locfile="../bintree.why"
loclnum="4" loccnumb="7" loccnume="11"
verified="true"
expanded="false">
</theory>
<theory
name="Size"
locfile="../bintree.why"
loclnum="10" loccnumb="7" loccnume="11"
verified="true"
expanded="true">
<label
name="number of nodes"/>
<goal
name="size_nonneg"
locfile="../bintree.why"
loclnum="20" loccnumb="8" loccnume="19"
sum="cb8c289d9686ccc4e3509e0890619661"
proved="true"
expanded="true"
shape="ainfix &lt;=c0asizeV0F">
<transf
name="induction_ty_lex"
proved="true"
expanded="true">
<goal
name="size_nonneg.1"
locfile="../bintree.why"
loclnum="20" loccnumb="8" loccnume="19"
expl="1."
sum="12d53d1b4d232aed7f7f83d7cb5e3f42"
proved="true"
expanded="true"
shape="Cainfix &lt;=c0asizeV0aEmptyainfix &lt;=c0asizeV0Iainfix &lt;=c0asizeV1Iainfix &lt;=c0asizeV3aNodeVVVV0F">
<proof
prover="0"
timelimit="6"
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.01"/>
</proof>
</goal>
</transf>
</goal>
<goal
name="size_empty"
locfile="../bintree.why"
loclnum="22" loccnumb="8" loccnume="18"
sum="b31540d42a20b62d3b95f5df6a1117e7"
proved="true"
expanded="true"
shape="ainfix =V0aEmptyqainfix =c0asizeV0F">
<transf
name="induction_ty_lex"
proved="true"
expanded="true">
<goal
name="size_empty.1"
locfile="../bintree.why"
loclnum="22" loccnumb="8" loccnume="18"
expl="1."
sum="c50dc79fc1bbfb85ca3062b724b8de5e"
proved="true"
expanded="false"
shape="Cainfix =V0aEmptyqainfix =c0asizeV0aEmptyainfix =V0aEmptyqainfix =c0asizeV0Iainfix =V1aEmptyqainfix =c0asizeV1Iainfix =V3aEmptyqainfix =c0asizeV3aNodeVVVV0F">
<proof
prover="0"
timelimit="6"
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.01"/>
</proof>
</goal>
</transf>
</goal>
</theory>
<theory
name="Occ"
locfile="../bintree.why"
loclnum="26" loccnumb="7" loccnume="10"
verified="true"
expanded="true">
<label
name="occurrences in a binary tree"/>
<goal
name="occ_nonneg"
locfile="../bintree.why"
loclnum="36" loccnumb="8" loccnume="18"
sum="717594c52723f5c7e9666ab1ab6810b6"
proved="true"
expanded="true"
shape="ainfix &lt;=c0aoccV0V1F">
<transf
name="induction_ty_lex"
proved="true"
expanded="true">
<goal
name="occ_nonneg.1"
locfile="../bintree.why"
loclnum="36" loccnumb="8" loccnume="18"
expl="1."
sum="63d90ff251110ddb7e30c27b8bb421b1"
proved="true"
expanded="true"
shape="Cainfix &lt;=c0aoccV0V1aEmptyainfix &lt;=c0aoccV0V1Iainfix &lt;=c0aoccV0V2Iainfix &lt;=c0aoccV0V4aNodeVVVV1F">
<proof
prover="0"
timelimit="6"
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.01"/>
</proof>
</goal>
</transf>
</goal>
</theory>
<theory
name="Inorder"
locfile="../bintree.why"
loclnum="44" loccnumb="7" loccnume="14"
verified="true"
expanded="false">
<label
name="inorder traversal"/>
</theory>
<theory
name="Preorder"
locfile="../bintree.why"
loclnum="56" loccnumb="7" loccnume="15"
verified="true"
expanded="false">
<label
name="preorder traversal"/>
</theory>
<theory
name="InorderLength"
locfile="../bintree.why"
loclnum="68" loccnumb="7" loccnume="20"
verified="true"
expanded="true">
<goal
name="inorder_length"
locfile="../bintree.why"
loclnum="74" loccnumb="8" loccnume="22"
sum="e81c509b7e9a14f0ce5eba170b717974"
proved="true"
expanded="true"
shape="ainfix =alengthainorderV0asizeV0F">
<transf
name="induction_ty_lex"
proved="true"
expanded="true">
<goal
name="inorder_length.1"
locfile="../bintree.why"
loclnum="74" loccnumb="8" loccnume="22"
expl="1."
sum="76c4ea67fd68f44ff3811c278c699051"
proved="true"
expanded="true"
shape="Cainfix =alengthainorderV0asizeV0aEmptyainfix =alengthainorderV0asizeV0Iainfix =alengthainorderV1asizeV1Iainfix =alengthainorderV3asizeV3aNodeVVVV0F">
<proof
prover="0"
timelimit="6"
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.01"/>
</proof>
</goal>
</transf>
</goal>
</theory>
<theory
name="Zipper"
locfile="../bintree.why"
loclnum="78" loccnumb="7" loccnume="13"
verified="true"
expanded="false">
<label
name="Huet&apos;s zipper"/>
</theory>
</file>
</why3session>
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