Commit 4f7af118 authored by François Bobot's avatar François Bobot

[Tagset] give bounds for max_tags

parent b800fea5
...@@ -34,7 +34,9 @@ ...@@ -34,7 +34,9 @@
<proof prover="1"><result status="valid" time="0.11"/></proof> <proof prover="1"><result status="valid" time="0.11"/></proof>
</goal> </goal>
<goal name="VC max_tags" expl="VC for max_tags" proved="true"> <goal name="VC max_tags" expl="VC for max_tags" proved="true">
<proof prover="0" obsolete="true"><result status="timeout" time="1.00"/></proof>
<proof prover="1"><result status="valid" time="0.09"/></proof> <proof prover="1"><result status="valid" time="0.09"/></proof>
<proof prover="2" obsolete="true"><result status="timeout" time="1.00"/></proof>
</goal> </goal>
<goal name="VC resize" expl="VC for resize" proved="true"> <goal name="VC resize" expl="VC for resize" proved="true">
<transf name="split_vc" proved="true" > <transf name="split_vc" proved="true" >
...@@ -209,7 +211,7 @@ ...@@ -209,7 +211,7 @@
<proof prover="1"><result status="valid" time="0.04"/></proof> <proof prover="1"><result status="valid" time="0.04"/></proof>
</goal> </goal>
<goal name="VC remove.22" expl="postcondition" proved="true"> <goal name="VC remove.22" expl="postcondition" proved="true">
<proof prover="0"><result status="valid" time="0.05" steps="161"/></proof> <proof prover="0"><result status="valid" time="0.05" steps="73"/></proof>
</goal> </goal>
</transf> </transf>
</goal> </goal>
...@@ -291,7 +293,7 @@ ...@@ -291,7 +293,7 @@
<goal name="Iterator.VC next" expl="VC for next" proved="true"> <goal name="Iterator.VC next" expl="VC for next" proved="true">
<transf name="split_vc" proved="true" > <transf name="split_vc" proved="true" >
<goal name="VC next.0" expl="assertion" proved="true"> <goal name="VC next.0" expl="assertion" proved="true">
<proof prover="0"><result status="valid" time="0.02" steps="86"/></proof> <proof prover="0"><result status="valid" time="0.02" steps="109"/></proof>
</goal> </goal>
<goal name="VC next.1" expl="index in array bounds" proved="true"> <goal name="VC next.1" expl="index in array bounds" proved="true">
<proof prover="1"><result status="valid" time="0.06"/></proof> <proof prover="1"><result status="valid" time="0.06"/></proof>
......
...@@ -53,6 +53,7 @@ module TagSetIntf ...@@ -53,6 +53,7 @@ module TagSetIntf
val function max_tags (h: t) : Int63.int63 val function max_tags (h: t) : Int63.int63
ensures { forall v. S.mem v h.elts -> tag v <= result } ensures { forall v. S.mem v h.elts -> tag v <= result }
ensures { -1 <= result < Int63.max_int63 }
val add (h: t) (k: key): unit val add (h: t) (k: key): unit
requires { k <> S.dummy } requires { k <> S.dummy }
...@@ -156,7 +157,8 @@ module TagSet ...@@ -156,7 +157,8 @@ module TagSet
tag k < Array.length h.iterated.value && Array.(S.tag h.iterated.value[tag k] <> S.tag S.dummy) tag k < Array.length h.iterated.value && Array.(S.tag h.iterated.value[tag k] <> S.tag S.dummy)
let function max_tags (h: t) : Int63.int63 let function max_tags (h: t) : Int63.int63
ensures { forall v. S.mem v h.elts -> tag v <= result } = ensures { forall v. S.mem v h.elts -> tag v <= result }
ensures { -1 <= result < Int63.max_int63 } =
Array.(length h.iterated.value) - 1 Array.(length h.iterated.value) - 1
let resize (h:t) (k:key) : unit let resize (h:t) (k:key) : unit
......
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