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

updated proof on moloch

parent 66369094
...@@ -45,6 +45,6 @@ end ...@@ -45,6 +45,6 @@ end
(* (*
Local Variables: Local Variables:
compile-command: "why3ide fill.mlw" compile-command: "unset LANG; make -C ../.. examples/programs/fill.gui"
End: End:
*) *)
...@@ -2,6 +2,7 @@ ...@@ -2,6 +2,7 @@
(* Beware! Only edit allowed sections below *) (* Beware! Only edit allowed sections below *)
Require Import ZArith. Require Import ZArith.
Require Import Rbase. Require Import Rbase.
Require int.Int.
Definition unit := unit. Definition unit := unit.
Parameter qtmark : Type. Parameter qtmark : Type.
......
<?xml version="1.0" encoding="UTF-8"?> <?xml version="1.0" encoding="UTF-8"?>
<!DOCTYPE why3session SYSTEM "why3session.dtd"> <!DOCTYPE why3session SYSTEM "why3session.dtd">
<why3session <why3session
name="fill/why3session.xml"> name="examples/programs/fill/why3session.xml">
<prover <prover
id="0" id="0"
name="Alt-Ergo" name="Alt-Ergo"
...@@ -9,21 +9,21 @@ ...@@ -9,21 +9,21 @@
<prover <prover
id="1" id="1"
name="Coq" name="Coq"
version="8.2pl2"/> version="8.3pl3"/>
<file <file
name="../fill.mlw" name="../fill.mlw"
verified="true" verified="true"
expanded="true"> expanded="true">
<theory <theory
name="WP Fill" name="WP Fill"
locfile="fill/../fill.mlw" locfile="examples/programs/fill/../fill.mlw"
loclnum="6" loccnumb="7" loccnume="11" loclnum="4" loccnumb="7" loccnume="11"
verified="true" verified="true"
expanded="true"> expanded="true">
<goal <goal
name="size_nonneg" name="size_nonneg"
locfile="fill/../fill.mlw" locfile="examples/programs/fill/../fill.mlw"
loclnum="24" loccnumb="8" loccnume="19" loclnum="23" loccnumb="8" loccnume="19"
sum="8382205e1f534dc681a160909cc41727" sum="8382205e1f534dc681a160909cc41727"
proved="true" proved="true"
expanded="true" expanded="true"
...@@ -31,16 +31,16 @@ ...@@ -31,16 +31,16 @@
<proof <proof
prover="1" prover="1"
timelimit="15" timelimit="15"
edited="fill_WP_Fill_size_nonneg_1.v" edited="fill_WP_Fill_size_nonneg_2.v"
obsolete="false" obsolete="false"
archived="false"> archived="false">
<result status="valid" time="0.45"/> <result status="valid" time="0.48"/>
</proof> </proof>
</goal> </goal>
<goal <goal
name="WP_parameter fill" name="WP_parameter fill"
locfile="fill/../fill.mlw" locfile="examples/programs/fill/../fill.mlw"
loclnum="26" loccnumb="10" loccnume="14" loclnum="25" loccnumb="10" loccnume="14"
expl="parameter fill" expl="parameter fill"
sum="2382af3dce215ccfb7a37bfd9f852d4a" sum="2382af3dce215ccfb7a37bfd9f852d4a"
proved="true" proved="true"
...@@ -54,7 +54,7 @@ ...@@ -54,7 +54,7 @@
timelimit="15" timelimit="15"
obsolete="false" obsolete="false"
archived="false"> archived="false">
<result status="valid" time="0.09"/> <result status="valid" time="0.07"/>
</proof> </proof>
</goal> </goal>
</theory> </theory>
......
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