Commit 2242838b authored by Andrei Paskevich's avatar Andrei Paskevich
Browse files

Peano: move division and minmax into separate modules

parent c687def9
This diff is collapsed.
......@@ -2,33 +2,33 @@
<!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="1.30" timelimit="1" steplimit="0" memlimit="1000"/>
<prover id="1" name="CVC4" version="1.4" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="1" name="CVC4" version="1.5" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="2" name="Alt-Ergo" version="2.0.0" timelimit="1" steplimit="0" memlimit="1000"/>
<file name="../monoid.mlw" proved="true">
<theory name="MonoidSumDef" proved="true">
<goal name="VC agg" expl="VC for agg" proved="true">
<proof prover="0"><result status="valid" time="0.01" steps="13"/></proof>
<proof prover="2"><result status="valid" time="0.01" steps="14"/></proof>
</goal>
<goal name="agg_sing_core" proved="true">
<proof prover="0"><result status="valid" time="0.00" steps="22"/></proof>
<proof prover="2"><result status="valid" time="0.00" steps="22"/></proof>
</goal>
<goal name="VC agg_cat" expl="VC for agg_cat" proved="true">
<proof prover="0"><result status="valid" time="0.07" steps="435"/></proof>
<proof prover="2"><result status="valid" time="0.07" steps="375"/></proof>
</goal>
<goal name="MS.M.assoc" proved="true">
<proof prover="0"><result status="valid" time="0.00" steps="2"/></proof>
<proof prover="2"><result status="valid" time="0.00" steps="2"/></proof>
</goal>
<goal name="MS.M.neutral" proved="true">
<proof prover="0"><result status="valid" time="0.00" steps="3"/></proof>
<proof prover="2"><result status="valid" time="0.00" steps="3"/></proof>
</goal>
<goal name="MS.agg_empty" proved="true">
<proof prover="0"><result status="valid" time="0.00" steps="3"/></proof>
<proof prover="2"><result status="valid" time="0.00" steps="3"/></proof>
</goal>
<goal name="MS.agg_sing" proved="true">
<proof prover="1"><result status="valid" time="0.03"/></proof>
</goal>
<goal name="MS.agg_cat" proved="true">
<proof prover="0"><result status="valid" time="0.00" steps="2"/></proof>
<proof prover="2"><result status="valid" time="0.00" steps="2"/></proof>
</goal>
</theory>
</file>
......
......@@ -2,31 +2,31 @@
<!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="1.30" timelimit="1" steplimit="0" memlimit="1000"/>
<prover id="1" name="Alt-Ergo" version="2.0.0" timelimit="1" steplimit="0" memlimit="1000"/>
<file name="../preorder.mlw" proved="true">
<theory name="Full" proved="true">
<goal name="Eq.Refl" proved="true">
<proof prover="0"><result status="valid" time="0.00" steps="3"/></proof>
<proof prover="1"><result status="valid" time="0.00" steps="3"/></proof>
</goal>
<goal name="Eq.Trans" proved="true">
<proof prover="0"><result status="valid" time="0.01" steps="34"/></proof>
<proof prover="1"><result status="valid" time="0.01" steps="48"/></proof>
</goal>
<goal name="Eq.Symm" proved="true">
<proof prover="0"><result status="valid" time="0.00" steps="9"/></proof>
<proof prover="1"><result status="valid" time="0.00" steps="5"/></proof>
</goal>
<goal name="Lt.Trans" proved="true">
<proof prover="0"><result status="valid" time="0.01" steps="34"/></proof>
<proof prover="1"><result status="valid" time="0.01" steps="49"/></proof>
</goal>
<goal name="Lt.Asymm" proved="true">
<proof prover="0"><result status="valid" time="0.00" steps="5"/></proof>
<proof prover="1"><result status="valid" time="0.00" steps="5"/></proof>
</goal>
</theory>
<theory name="TotalFull" proved="true">
<goal name="Lt.Total" proved="true">
<proof prover="0"><result status="valid" time="0.00" steps="3"/></proof>
<proof prover="1"><result status="valid" time="0.00" steps="11"/></proof>
</goal>
<goal name="lt_def2" proved="true">
<proof prover="0"><result status="valid" time="0.00" steps="7"/></proof>
<proof prover="1"><result status="valid" time="0.00" steps="13"/></proof>
</goal>
</theory>
</file>
......
This diff is collapsed.
......@@ -2,159 +2,159 @@
<!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="1.30" timelimit="1" steplimit="0" memlimit="1000"/>
<prover id="1" name="Alt-Ergo" version="2.0.0" timelimit="1" steplimit="0" memlimit="1000"/>
<file name="../ral.mlw" proved="true">
<theory name="RAL" proved="true">
<goal name="VC balancing" expl="VC for balancing" proved="true">
<proof prover="0"><result status="valid" time="0.01" steps="3"/></proof>
<proof prover="1"><result status="valid" time="0.01" steps="3"/></proof>
</goal>
<goal name="M.assoc" proved="true">
<proof prover="0"><result status="valid" time="0.01" steps="4"/></proof>
<proof prover="1"><result status="valid" time="0.01" steps="4"/></proof>
</goal>
<goal name="M.neutral" proved="true">
<proof prover="0"><result status="valid" time="0.01" steps="4"/></proof>
<proof prover="1"><result status="valid" time="0.01" steps="4"/></proof>
</goal>
<goal name="M.M.assoc" proved="true">
<proof prover="0"><result status="valid" time="0.01" steps="4"/></proof>
<proof prover="1"><result status="valid" time="0.01" steps="4"/></proof>
</goal>
<goal name="M.M.neutral" proved="true">
<proof prover="0"><result status="valid" time="0.01" steps="4"/></proof>
<proof prover="1"><result status="valid" time="0.01" steps="4"/></proof>
</goal>
<goal name="M.VC zero" expl="VC for zero" proved="true">
<proof prover="0"><result status="valid" time="0.01" steps="4"/></proof>
<proof prover="1"><result status="valid" time="0.01" steps="4"/></proof>
</goal>
<goal name="M.VC op" expl="VC for op" proved="true">
<proof prover="0"><result status="valid" time="0.01" steps="4"/></proof>
<proof prover="1"><result status="valid" time="0.01" steps="4"/></proof>
</goal>
<goal name="D.VC measure" expl="VC for measure" proved="true">
<proof prover="0"><result status="valid" time="0.01" steps="4"/></proof>
<proof prover="1"><result status="valid" time="0.01" steps="4"/></proof>
</goal>
<goal name="VC agg_measure_is_length" expl="VC for agg_measure_is_length" proved="true">
<proof prover="0"><result status="valid" time="0.01" steps="50"/></proof>
<proof prover="1"><result status="valid" time="0.01" steps="50"/></proof>
</goal>
<goal name="VC selected_part" expl="VC for selected_part" proved="true">
<proof prover="0"><result status="valid" time="0.26" steps="762"/></proof>
<proof prover="1"><result status="valid" time="0.12" steps="729"/></proof>
</goal>
<goal name="Sel.M.assoc" proved="true">
<proof prover="0"><result status="valid" time="0.01" steps="4"/></proof>
<proof prover="1"><result status="valid" time="0.01" steps="4"/></proof>
</goal>
<goal name="Sel.M.neutral" proved="true">
<proof prover="0"><result status="valid" time="0.01" steps="4"/></proof>
<proof prover="1"><result status="valid" time="0.01" steps="4"/></proof>
</goal>
<goal name="Sel.M.VC zero" expl="VC for zero" proved="true">
<proof prover="0"><result status="valid" time="0.01" steps="4"/></proof>
<proof prover="1"><result status="valid" time="0.01" steps="4"/></proof>
</goal>
<goal name="Sel.M.VC op" expl="VC for op" proved="true">
<proof prover="0"><result status="valid" time="0.01" steps="4"/></proof>
<proof prover="1"><result status="valid" time="0.01" steps="4"/></proof>
</goal>
<goal name="Sel.M.agg_empty" proved="true">
<proof prover="0"><result status="valid" time="0.02" steps="6"/></proof>
<proof prover="1"><result status="valid" time="0.02" steps="6"/></proof>
</goal>
<goal name="Sel.M.agg_sing" proved="true">
<proof prover="0"><result status="valid" time="0.01" steps="19"/></proof>
<proof prover="1"><result status="valid" time="0.01" steps="19"/></proof>
</goal>
<goal name="Sel.M.agg_cat" proved="true">
<proof prover="0"><result status="valid" time="0.01" steps="5"/></proof>
<proof prover="1"><result status="valid" time="0.01" steps="5"/></proof>
</goal>
<goal name="Sel.D.VC measure" expl="VC for measure" proved="true">
<proof prover="0"><result status="valid" time="0.01" steps="4"/></proof>
<proof prover="1"><result status="valid" time="0.01" steps="4"/></proof>
</goal>
<goal name="Sel.VC balancing" expl="VC for balancing" proved="true">
<proof prover="0"><result status="valid" time="0.01" steps="4"/></proof>
<proof prover="1"><result status="valid" time="0.01" steps="4"/></proof>
</goal>
<goal name="Sel.selection_empty" proved="true">
<proof prover="0"><result status="valid" time="0.02" steps="35"/></proof>
<proof prover="1"><result status="valid" time="0.02" steps="35"/></proof>
</goal>
<goal name="Sel.VC selected_part" expl="VC for selected_part" proved="true">
<proof prover="0"><result status="valid" time="0.28" steps="655"/></proof>
<proof prover="1"><result status="valid" time="0.10" steps="397"/></proof>
</goal>
<goal name="VC empty" expl="VC for empty" proved="true">
<proof prover="0"><result status="valid" time="0.02" steps="6"/></proof>
<proof prover="1"><result status="valid" time="0.02" steps="6"/></proof>
</goal>
<goal name="VC singleton" expl="VC for singleton" proved="true">
<proof prover="0"><result status="valid" time="0.02" steps="6"/></proof>
<proof prover="1"><result status="valid" time="0.02" steps="6"/></proof>
</goal>
<goal name="VC is_empty" expl="VC for is_empty" proved="true">
<proof prover="0"><result status="valid" time="0.01" steps="4"/></proof>
<proof prover="1"><result status="valid" time="0.01" steps="4"/></proof>
</goal>
<goal name="VC decompose_front" expl="VC for decompose_front" proved="true">
<proof prover="0"><result status="valid" time="0.03" steps="59"/></proof>
<proof prover="1"><result status="valid" time="0.03" steps="59"/></proof>
</goal>
<goal name="VC decompose_back" expl="VC for decompose_back" proved="true">
<proof prover="0"><result status="valid" time="0.04" steps="59"/></proof>
<proof prover="1"><result status="valid" time="0.04" steps="59"/></proof>
</goal>
<goal name="VC front" expl="VC for front" proved="true">
<proof prover="0"><result status="valid" time="0.01" steps="4"/></proof>
<proof prover="1"><result status="valid" time="0.01" steps="4"/></proof>
</goal>
<goal name="VC back" expl="VC for back" proved="true">
<proof prover="0"><result status="valid" time="0.02" steps="4"/></proof>
<proof prover="1"><result status="valid" time="0.02" steps="4"/></proof>
</goal>
<goal name="VC cons" expl="VC for cons" proved="true">
<proof prover="0"><result status="valid" time="0.02" steps="7"/></proof>
<proof prover="1"><result status="valid" time="0.02" steps="7"/></proof>
</goal>
<goal name="VC snoc" expl="VC for snoc" proved="true">
<proof prover="0"><result status="valid" time="0.02" steps="7"/></proof>
<proof prover="1"><result status="valid" time="0.02" steps="7"/></proof>
</goal>
<goal name="VC concat" expl="VC for concat" proved="true">
<proof prover="0"><result status="valid" time="0.03" steps="4"/></proof>
<proof prover="1"><result status="valid" time="0.03" steps="4"/></proof>
</goal>
<goal name="VC length" expl="VC for length" proved="true">
<proof prover="0"><result status="valid" time="0.01" steps="5"/></proof>
<proof prover="1"><result status="valid" time="0.01" steps="5"/></proof>
</goal>
<goal name="VC set" expl="VC for set" proved="true">
<proof prover="0"><result status="valid" time="0.20" steps="488"/></proof>
<proof prover="1"><result status="valid" time="0.20" steps="492"/></proof>
</goal>
<goal name="VC get" expl="VC for get" proved="true">
<proof prover="0"><result status="valid" time="0.07" steps="106"/></proof>
<proof prover="1"><result status="valid" time="0.07" steps="106"/></proof>
</goal>
<goal name="VC insert" expl="VC for insert" proved="true">
<proof prover="0"><result status="valid" time="0.47" steps="498"/></proof>
<proof prover="1"><result status="valid" time="0.28" steps="533"/></proof>
</goal>
<goal name="VC remove" expl="VC for remove" proved="true">
<proof prover="0"><result status="valid" time="0.38" steps="360"/></proof>
<proof prover="1"><result status="valid" time="0.21" steps="392"/></proof>
</goal>
<goal name="VC cut" expl="VC for cut" proved="true">
<proof prover="0"><result status="valid" time="0.09" steps="177"/></proof>
<proof prover="1"><result status="valid" time="0.09" steps="181"/></proof>
</goal>
<goal name="VC split" expl="VC for split" proved="true">
<proof prover="0"><result status="valid" time="0.15" steps="353"/></proof>
<proof prover="1"><result status="valid" time="0.15" steps="355"/></proof>
</goal>
<goal name="VC harness" expl="VC for harness" proved="true">
<transf name="split_goal_right" proved="true" >
<goal name="VC harness.0" expl="precondition" proved="true">
<proof prover="0"><result status="valid" time="0.03" steps="6"/></proof>
<proof prover="1"><result status="valid" time="0.03" steps="6"/></proof>
</goal>
<goal name="VC harness.1" expl="precondition" proved="true">
<proof prover="0"><result status="valid" time="0.03" steps="9"/></proof>
<proof prover="1"><result status="valid" time="0.03" steps="9"/></proof>
</goal>
<goal name="VC harness.2" expl="precondition" proved="true">
<proof prover="0"><result status="valid" time="0.01" steps="12"/></proof>
<proof prover="1"><result status="valid" time="0.01" steps="12"/></proof>
</goal>
<goal name="VC harness.3" expl="precondition" proved="true">
<proof prover="0"><result status="valid" time="0.03" steps="15"/></proof>
<proof prover="1"><result status="valid" time="0.03" steps="15"/></proof>
</goal>
<goal name="VC harness.4" expl="check" proved="true">
<proof prover="0"><result status="valid" time="0.06" steps="143"/></proof>
<proof prover="1"><result status="valid" time="0.06" steps="142"/></proof>
</goal>
<goal name="VC harness.5" expl="check" proved="true">
<proof prover="0"><result status="valid" time="0.07" steps="143"/></proof>
<proof prover="1"><result status="valid" time="0.07" steps="142"/></proof>
</goal>
<goal name="VC harness.6" expl="precondition" proved="true">
<proof prover="0"><result status="valid" time="0.03" steps="18"/></proof>
<proof prover="1"><result status="valid" time="0.03" steps="18"/></proof>
</goal>
<goal name="VC harness.7" expl="precondition" proved="true">
<proof prover="0"><result status="valid" time="0.02" steps="20"/></proof>
<proof prover="1"><result status="valid" time="0.02" steps="20"/></proof>
</goal>
<goal name="VC harness.8" expl="check" proved="true">
<proof prover="0"><result status="valid" time="0.58" steps="361"/></proof>
<proof prover="1"><result status="valid" time="0.58" steps="536"/></proof>
</goal>
<goal name="VC harness.9" expl="check" proved="true">
<proof prover="0" timelimit="5"><result status="valid" time="1.81" steps="534"/></proof>
<proof prover="1" timelimit="5"><result status="valid" time="1.02" steps="501"/></proof>
</goal>
</transf>
</goal>
<goal name="VC harness2" expl="VC for harness2" proved="true">
<proof prover="0"><result status="valid" time="0.11" steps="216"/></proof>
<proof prover="1"><result status="valid" time="0.11" steps="223"/></proof>
</goal>
</theory>
</file>
......
This diff is collapsed.
......@@ -242,7 +242,6 @@ module McCarthy91Mach
n := !n - 10;
e := pred !e
end else begin
assert { spec !n = spec (spec (!n + 11)) };
n := !n + 11;
e := succ !e
end
......
......@@ -48,19 +48,16 @@
<goal name="VC f91_nonrec.3" expl="loop invariant preservation" proved="true">
<proof prover="3"><result status="valid" time="0.03" steps="217"/></proof>
</goal>
<goal name="VC f91_nonrec.4" expl="assertion" proved="true">
<proof prover="3"><result status="valid" time="0.01" steps="20"/></proof>
<goal name="VC f91_nonrec.4" expl="integer overflow" proved="true">
<proof prover="3"><result status="valid" time="0.01" steps="16"/></proof>
</goal>
<goal name="VC f91_nonrec.5" expl="integer overflow" proved="true">
<proof prover="3"><result status="valid" time="0.01" steps="17"/></proof>
</goal>
<goal name="VC f91_nonrec.6" expl="loop variant decrease" proved="true">
<proof prover="3"><result status="valid" time="0.00" steps="18"/></proof>
<goal name="VC f91_nonrec.5" expl="loop variant decrease" proved="true">
<proof prover="3"><result status="valid" time="0.00" steps="17"/></proof>
</goal>
<goal name="VC f91_nonrec.7" expl="loop invariant preservation" proved="true">
<proof prover="3"><result status="valid" time="0.04" steps="304"/></proof>
<goal name="VC f91_nonrec.6" expl="loop invariant preservation" proved="true">
<proof prover="3"><result status="valid" time="3.56" steps="4952"/></proof>
</goal>
<goal name="VC f91_nonrec.8" expl="postcondition" proved="true">
<goal name="VC f91_nonrec.7" expl="postcondition" proved="true">
<proof prover="3"><result status="valid" time="0.00" steps="30"/></proof>
</goal>
</transf>
......
......@@ -98,7 +98,7 @@
<proof prover="4"><result status="valid" time="0.36" steps="1404"/></proof>
</goal>
<goal name="VC count_bt_queens" expl="VC for count_bt_queens" proved="true">
<proof prover="4"><result status="valid" time="4.08" steps="3486"/></proof>
<proof prover="4"><result status="valid" time="4.08" steps="3527"/></proof>
</goal>
<goal name="VC count_queens" expl="VC for count_queens" proved="true">
<proof prover="4"><result status="valid" time="0.01" steps="15"/></proof>
......
......@@ -70,19 +70,33 @@ module Peano
e.g. addition of two values of different signs
*)
end
module ComputerDivision
use int.Int
use int.ComputerDivision
use Peano
val div (x y: t) : t
requires { y.v <> 0 }
ensures { result.v = div x.v y.v }
val mod (x y: t) : t
requires { y.v <> 0 }
ensures { result.v = mod x.v y.v }
end
module MinMax
use int.Int
use int.MinMax
use Peano
val max (x y: t) : t
ensures { result.v = max x.v y.v }
val min (x y: t) : t
ensures { result.v = min x.v y.v }
......
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