Attention une mise à jour du serveur va être effectuée le lundi 17 mai entre 13h et 13h30. Cette mise à jour va générer une interruption du service de quelques minutes.

simpler variants in bitvector examples

parent f4becc27
......@@ -51,7 +51,7 @@ module Test_proofinuse
let two = 2:t in
while uge !i two do
variant{ !i with ult }
variant{ t'int !i }
i := lsr_bv !i two
done
......
......@@ -2,6 +2,7 @@
<!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="2.0.0" timelimit="1" steplimit="0" memlimit="1000"/>
<prover id="3" name="Alt-Ergo" version="1.30" timelimit="1" steplimit="0" memlimit="1000"/>
<prover id="4" name="CVC4" version="1.5" timelimit="1" steplimit="0" memlimit="1000"/>
<file name="../bitvector_examples.mlw" proved="true">
......@@ -13,7 +14,11 @@
<proof prover="4"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="VC testVariant" expl="VC for testVariant" proved="true">
<proof prover="4"><result status="valid" time="0.04"/></proof>
<transf name="split_vc" proved="true" >
<goal name="VC testVariant.0" expl="loop variant decrease" proved="true">
<proof prover="0"><result status="valid" time="0.40" steps="582"/></proof>
</goal>
</transf>
</goal>
<goal name="ttt" proved="true">
<proof prover="4"><result status="valid" time="0.05"/></proof>
......
......@@ -142,7 +142,7 @@ module Bitwalker
let i = ref BV32.zeros in
let lstart = BV32.sub_check (BV32.of_int 64) len in
while BV32.ult !i len do variant{ !i with BV32.ugt }
while BV32.ult !i len do variant{ BV32.t'int len - BV32.t'int !i }
invariant {0 <= BV32.t'int !i <= BV32.t'int len}
invariant {forall j:int. BV32.t'int len - BV32.t'int !i <= j < BV32.t'int len ->
BV64.nth !retval j
......@@ -255,7 +255,7 @@ module Bitwalker
let i = ref BV32.zeros in
label Init in
while BV32.ult !i len do variant { !i with BV32.ugt }
while BV32.ult !i len do variant { BV32.t'int len - BV32.t'int !i }
invariant {0 <= BV32.t'int !i <= BV32.t'int len}
invariant {forall j:int. 0 <= j < BV32.t'int start ->
nth8_stream (addr at Init) j
......
......@@ -75,7 +75,7 @@ module Utils_Spec
numof_shift p q a (b-1) k
let rec lemma countSpec_Aux (bv : t) : unit
variant {bv with ult}
variant {t'int bv}
ensures {t'int (count bv) = NumOf.numof (nth bv) 0 32}
=
if pure { bv <> zeros } then
......
......@@ -2,6 +2,7 @@
<!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="2.0.0" timelimit="1" steplimit="0" memlimit="1000"/>
<prover id="3" name="Alt-Ergo" version="1.30" timelimit="1" steplimit="0" memlimit="1000"/>
<prover id="5" name="CVC4" version="1.4" alternative="noBV" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="8" name="Z3" version="4.5.0" timelimit="1" steplimit="0" memlimit="1000"/>
......@@ -51,8 +52,11 @@
<transf name="split_goal_right" proved="true" >
<goal name="VC countSpec_Aux.0" expl="variant decrease" proved="true">
<transf name="split_goal_right" proved="true" >
<goal name="VC countSpec_Aux.0.0" expl="variant decrease" proved="true">
<proof prover="9"><result status="valid" time="0.01"/></proof>
<goal name="VC countSpec_Aux.0.0" expl="VC for countSpec_Aux" proved="true">
<proof prover="9"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="VC countSpec_Aux.0.1" expl="VC for countSpec_Aux" proved="true">
<proof prover="0"><result status="valid" time="0.39" steps="315"/></proof>
</goal>
</transf>
</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