Mentions légales du service

Skip to content
Snippets Groups Projects
Commit b800fea5 authored by François Bobot's avatar François Bobot
Browse files

Update tagset for FSet renaming

parent be95ca14
Branches
Tags
1 merge request!82Imperative TagSet with iterators
Show whitespace changes
Inline Side-by-side
examples/stdlib/tagset/why3session.xml
+ 102
− 102
View file @ b800fea5
<?xml version="1.0" encoding="UTF-8"?>
<!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN"
"http://why3.lri.fr/why3session.dtd">
<why3session shape_version="5">
<why3session shape_version="6">
<prover id="0" name="Alt-Ergo" version="2.2.0" timelimit="1" steplimit="0" memlimit="1000"/>
<prover id="1" name="CVC4" version="1.6" timelimit="1" steplimit="0" memlimit="1000"/>
<prover id="2" name="Z3" version="4.4.1" timelimit="1" steplimit="0" memlimit="1000"/>
......@@ -22,333 +22,333 @@
</theory>
<theory name="TagSet" proved="true">
<goal name="VC iteration_state" expl="VC for iteration_state" proved="true">
<proof prover="1"><result status="valid" time="0.61"/></proof>
<proof prover="1"><result status="valid" time="0.07"/></proof>
</goal>
<goal name="VC t" expl="VC for t" proved="true">
<proof prover="1"><result status="valid" time="0.23"/></proof>
<proof prover="1"><result status="valid" time="0.03"/></proof>
</goal>
<goal name="VC create" expl="VC for create" proved="true">
<proof prover="1"><result status="valid" time="0.66"/></proof>
<proof prover="1"><result status="valid" time="0.09"/></proof>
</goal>
<goal name="VC mem" expl="VC for mem" proved="true">
<proof prover="1"><result status="valid" time="0.68"/></proof>
<proof prover="1"><result status="valid" time="0.11"/></proof>
</goal>
<goal name="VC max_tags" expl="VC for max_tags" proved="true">
<proof prover="1"><result status="valid" time="0.60"/></proof>
<proof prover="1"><result status="valid" time="0.09"/></proof>
</goal>
<goal name="VC resize" expl="VC for resize" proved="true">
<transf name="split_vc" proved="true" >
<goal name="VC resize.0" expl="integer overflow" proved="true">
<proof prover="1"><result status="valid" time="0.38"/></proof>
<proof prover="1"><result status="valid" time="0.06"/></proof>
</goal>
<goal name="VC resize.1" expl="division by zero" proved="true">
<proof prover="1"><result status="valid" time="0.28"/></proof>
<proof prover="1"><result status="valid" time="0.04"/></proof>
</goal>
<goal name="VC resize.2" expl="integer overflow" proved="true">
<proof prover="1"><result status="valid" time="0.50"/></proof>
<proof prover="1"><result status="valid" time="0.07"/></proof>
</goal>
<goal name="VC resize.3" expl="integer overflow" proved="true">
<proof prover="1"><result status="valid" time="0.50"/></proof>
<proof prover="1"><result status="valid" time="0.07"/></proof>
</goal>
<goal name="VC resize.4" expl="array creation size" proved="true">
<proof prover="1"><result status="valid" time="0.40"/></proof>
<proof prover="1"><result status="valid" time="0.05"/></proof>
</goal>
<goal name="VC resize.5" expl="precondition" proved="true">
<proof prover="1"><result status="valid" time="0.39"/></proof>
<proof prover="1"><result status="valid" time="0.06"/></proof>
</goal>
<goal name="VC resize.6" expl="precondition" proved="true">
<proof prover="1"><result status="valid" time="0.28"/></proof>
<proof prover="1"><result status="valid" time="0.03"/></proof>
</goal>
<goal name="VC resize.7" expl="precondition" proved="true">
<proof prover="1"><result status="valid" time="0.35"/></proof>
<proof prover="1"><result status="valid" time="0.05"/></proof>
</goal>
<goal name="VC resize.8" expl="type invariant" proved="true">
<proof prover="1"><result status="valid" time="0.47"/></proof>
<proof prover="1"><result status="valid" time="0.08"/></proof>
</goal>
<goal name="VC resize.9" expl="type invariant" proved="true">
<proof prover="1"><result status="valid" time="0.64"/></proof>
<proof prover="1"><result status="valid" time="0.10"/></proof>
</goal>
<goal name="VC resize.10" expl="type invariant" proved="true">
<proof prover="1"><result status="valid" time="0.60"/></proof>
<proof prover="1"><result status="valid" time="0.10"/></proof>
</goal>
<goal name="VC resize.11" expl="type invariant" proved="true">
<proof prover="1"><result status="valid" time="0.62"/></proof>
<proof prover="1"><result status="valid" time="0.09"/></proof>
</goal>
<goal name="VC resize.12" expl="type invariant" proved="true">
<proof prover="1"><result status="valid" time="0.64"/></proof>
<proof prover="1"><result status="valid" time="0.11"/></proof>
</goal>
<goal name="VC resize.13" expl="type invariant" proved="true">
<proof prover="1"><result status="valid" time="0.35"/></proof>
<proof prover="1"><result status="valid" time="0.05"/></proof>
</goal>
<goal name="VC resize.14" expl="postcondition" proved="true">
<proof prover="1"><result status="valid" time="0.35"/></proof>
<proof prover="1"><result status="valid" time="0.06"/></proof>
</goal>
<goal name="VC resize.15" expl="postcondition" proved="true">
<proof prover="1"><result status="valid" time="0.30"/></proof>
<proof prover="1"><result status="valid" time="0.06"/></proof>
</goal>
</transf>
</goal>
<goal name="VC add" expl="VC for add" proved="true">
<transf name="split_vc" proved="true" >
<goal name="VC add.0" expl="precondition" proved="true">
<proof prover="1"><result status="valid" time="0.25"/></proof>
<proof prover="1"><result status="valid" time="0.03"/></proof>
</goal>
<goal name="VC add.1" expl="index in array bounds" proved="true">
<proof prover="1"><result status="valid" time="0.26"/></proof>
<proof prover="1"><result status="valid" time="0.04"/></proof>
</goal>
<goal name="VC add.2" expl="precondition" proved="true">
<proof prover="1"><result status="valid" time="0.26"/></proof>
<proof prover="1"><result status="valid" time="0.03"/></proof>
</goal>
<goal name="VC add.3" expl="precondition" proved="true">
<proof prover="1"><result status="valid" time="0.31"/></proof>
<proof prover="1"><result status="valid" time="0.03"/></proof>
</goal>
<goal name="VC add.4" expl="precondition" proved="true">
<proof prover="1"><result status="valid" time="0.30"/></proof>
<proof prover="1"><result status="valid" time="0.04"/></proof>
</goal>
<goal name="VC add.5" expl="precondition" proved="true">
<proof prover="1"><result status="valid" time="0.35"/></proof>
<proof prover="1"><result status="valid" time="0.04"/></proof>
</goal>
<goal name="VC add.6" expl="precondition" proved="true">
<proof prover="1"><result status="valid" time="0.27"/></proof>
<proof prover="1"><result status="valid" time="0.04"/></proof>
</goal>
<goal name="VC add.7" expl="type invariant" proved="true">
<proof prover="1"><result status="valid" time="0.24"/></proof>
<proof prover="1"><result status="valid" time="0.04"/></proof>
</goal>
<goal name="VC add.8" expl="postcondition" proved="true">
<proof prover="1"><result status="valid" time="0.23"/></proof>
<proof prover="1"><result status="valid" time="0.04"/></proof>
</goal>
<goal name="VC add.9" expl="type invariant" proved="true">
<proof prover="1"><result status="valid" time="0.45"/></proof>
<proof prover="1"><result status="valid" time="0.08"/></proof>
</goal>
<goal name="VC add.10" expl="type invariant" proved="true">
<proof prover="1"><result status="valid" time="0.62"/></proof>
<proof prover="1"><result status="valid" time="0.10"/></proof>
</goal>
<goal name="VC add.11" expl="type invariant" proved="true">
<proof prover="1"><result status="valid" time="0.63"/></proof>
<proof prover="1"><result status="valid" time="0.10"/></proof>
</goal>
<goal name="VC add.12" expl="type invariant" proved="true">
<proof prover="1"><result status="valid" time="0.78"/></proof>
<proof prover="1"><result status="valid" time="0.11"/></proof>
</goal>
<goal name="VC add.13" expl="type invariant" proved="true">
<proof prover="1"><result status="valid" time="0.71"/></proof>
<proof prover="1"><result status="valid" time="0.15"/></proof>
</goal>
<goal name="VC add.14" expl="type invariant" proved="true">
<proof prover="1"><result status="valid" time="0.32"/></proof>
<proof prover="1"><result status="valid" time="0.06"/></proof>
</goal>
<goal name="VC add.15" expl="postcondition" proved="true">
<proof prover="1"><result status="valid" time="0.32"/></proof>
<proof prover="1"><result status="valid" time="0.05"/></proof>
</goal>
</transf>
</goal>
<goal name="VC remove" expl="VC for remove" proved="true">
<transf name="split_vc" proved="true" >
<goal name="VC remove.0" expl="index in array bounds" proved="true">
<proof prover="1"><result status="valid" time="0.28"/></proof>
<proof prover="1"><result status="valid" time="0.03"/></proof>
</goal>
<goal name="VC remove.1" expl="precondition" proved="true">
<proof prover="1"><result status="valid" time="0.26"/></proof>
<proof prover="1"><result status="valid" time="0.04"/></proof>
</goal>
<goal name="VC remove.2" expl="precondition" proved="true">
<proof prover="1"><result status="valid" time="0.37"/></proof>
<proof prover="1"><result status="valid" time="0.05"/></proof>
</goal>
<goal name="VC remove.3" expl="precondition" proved="true">
<proof prover="1"><result status="valid" time="0.32"/></proof>
<proof prover="1"><result status="valid" time="0.04"/></proof>
</goal>
<goal name="VC remove.4" expl="precondition" proved="true">
<proof prover="1"><result status="valid" time="0.29"/></proof>
<proof prover="1"><result status="valid" time="0.04"/></proof>
</goal>
<goal name="VC remove.5" expl="precondition" proved="true">
<proof prover="1"><result status="valid" time="0.27"/></proof>
<proof prover="1"><result status="valid" time="0.04"/></proof>
</goal>
<goal name="VC remove.6" expl="type invariant" proved="true">
<proof prover="1"><result status="valid" time="0.22"/></proof>
<proof prover="1"><result status="valid" time="0.03"/></proof>
</goal>
<goal name="VC remove.7" expl="postcondition" proved="true">
<proof prover="1"><result status="valid" time="0.24"/></proof>
<proof prover="1"><result status="valid" time="0.04"/></proof>
</goal>
<goal name="VC remove.8" expl="type invariant" proved="true">
<proof prover="1"><result status="valid" time="0.44"/></proof>
<proof prover="1"><result status="valid" time="0.07"/></proof>
</goal>
<goal name="VC remove.9" expl="type invariant" proved="true">
<proof prover="1"><result status="valid" time="0.62"/></proof>
<proof prover="1"><result status="valid" time="0.08"/></proof>
</goal>
<goal name="VC remove.10" expl="type invariant" proved="true">
<proof prover="1"><result status="valid" time="0.60"/></proof>
<proof prover="1"><result status="valid" time="0.10"/></proof>
</goal>
<goal name="VC remove.11" expl="type invariant" proved="true">
<proof prover="1"><result status="valid" time="0.71"/></proof>
<proof prover="1"><result status="valid" time="0.10"/></proof>
</goal>
<goal name="VC remove.12" expl="type invariant" proved="true">
<proof prover="1"><result status="valid" time="0.68"/></proof>
<proof prover="1"><result status="valid" time="0.13"/></proof>
</goal>
<goal name="VC remove.13" expl="type invariant" proved="true">
<proof prover="1"><result status="valid" time="0.31"/></proof>
<proof prover="1"><result status="valid" time="0.05"/></proof>
</goal>
<goal name="VC remove.14" expl="postcondition" proved="true">
<proof prover="1"><result status="valid" time="0.81"/></proof>
<proof prover="1"><result status="valid" time="0.08"/></proof>
</goal>
<goal name="VC remove.15" expl="precondition" proved="true">
<proof prover="1"><result status="valid" time="0.28"/></proof>
<proof prover="1"><result status="valid" time="0.05"/></proof>
</goal>
<goal name="VC remove.16" expl="precondition" proved="true">
<proof prover="1"><result status="valid" time="0.27"/></proof>
<proof prover="1"><result status="valid" time="0.04"/></proof>
</goal>
<goal name="VC remove.17" expl="precondition" proved="true">
<proof prover="1"><result status="valid" time="0.27"/></proof>
<proof prover="1"><result status="valid" time="0.04"/></proof>
</goal>
<goal name="VC remove.18" expl="precondition" proved="true">
<proof prover="1"><result status="valid" time="0.26"/></proof>
<proof prover="1"><result status="valid" time="0.04"/></proof>
</goal>
<goal name="VC remove.19" expl="precondition" proved="true">
<proof prover="1"><result status="valid" time="0.31"/></proof>
<proof prover="1"><result status="valid" time="0.04"/></proof>
</goal>
<goal name="VC remove.20" expl="type invariant" proved="true">
<proof prover="1"><result status="valid" time="0.24"/></proof>
<proof prover="1"><result status="valid" time="0.04"/></proof>
</goal>
<goal name="VC remove.21" expl="postcondition" proved="true">
<proof prover="1"><result status="valid" time="0.22"/></proof>
<proof prover="1"><result status="valid" time="0.04"/></proof>
</goal>
<goal name="VC remove.22" expl="postcondition" proved="true">
<proof prover="0"><result status="valid" time="0.38" steps="185"/></proof>
<proof prover="0"><result status="valid" time="0.05" steps="161"/></proof>
</goal>
</transf>
</goal>
<goal name="VC iterator" expl="VC for iterator" proved="true">
<proof prover="1"><result status="valid" time="0.66"/></proof>
<proof prover="1"><result status="valid" time="0.11"/></proof>
</goal>
<goal name="Iterator.VC create" expl="VC for create" proved="true">
<transf name="split_vc" proved="true" >
<goal name="VC create.0" expl="loop invariant init" proved="true">
<proof prover="1"><result status="valid" time="0.38"/></proof>
<proof prover="1"><result status="valid" time="0.05"/></proof>
</goal>
<goal name="VC create.1" expl="loop invariant init" proved="true">
<proof prover="1"><result status="valid" time="0.39"/></proof>
<proof prover="1"><result status="valid" time="0.04"/></proof>
</goal>
<goal name="VC create.2" expl="index in array bounds" proved="true">
<proof prover="1"><result status="valid" time="0.24"/></proof>
<proof prover="1"><result status="valid" time="0.04"/></proof>
</goal>
<goal name="VC create.3" expl="integer overflow" proved="true">
<proof prover="1"><result status="valid" time="0.39"/></proof>
<proof prover="1"><result status="valid" time="0.06"/></proof>
</goal>
<goal name="VC create.4" expl="loop variant decrease" proved="true">
<proof prover="1"><result status="valid" time="0.32"/></proof>
<proof prover="1"><result status="valid" time="0.05"/></proof>
</goal>
<goal name="VC create.5" expl="loop invariant preservation" proved="true">
<proof prover="1"><result status="valid" time="0.35"/></proof>
<proof prover="1"><result status="valid" time="0.06"/></proof>
</goal>
<goal name="VC create.6" expl="loop invariant preservation" proved="true">
<proof prover="1"><result status="valid" time="0.47"/></proof>
<proof prover="1"><result status="valid" time="0.08"/></proof>
</goal>
<goal name="VC create.7" expl="precondition" proved="true">
<proof prover="1"><result status="valid" time="0.48"/></proof>
<proof prover="1"><result status="valid" time="0.07"/></proof>
</goal>
<goal name="VC create.8" expl="precondition" proved="true">
<proof prover="1"><result status="valid" time="0.34"/></proof>
<proof prover="1"><result status="valid" time="0.04"/></proof>
</goal>
<goal name="VC create.9" expl="precondition" proved="true">
<proof prover="1"><result status="valid" time="0.48"/></proof>
<proof prover="1"><result status="valid" time="0.08"/></proof>
</goal>
<goal name="VC create.10" expl="precondition" proved="true">
<proof prover="1"><result status="valid" time="0.46"/></proof>
<proof prover="1"><result status="valid" time="0.08"/></proof>
</goal>
<goal name="VC create.11" expl="precondition" proved="true">
<proof prover="1"><result status="valid" time="0.77"/></proof>
<proof prover="1"><result status="valid" time="0.13"/></proof>
</goal>
<goal name="VC create.12" expl="precondition" proved="true">
<transf name="split_vc" proved="true" >
<goal name="VC create.12.0" expl="precondition" proved="true">
<proof prover="1"><result status="valid" time="0.27"/></proof>
<proof prover="1"><result status="valid" time="0.04"/></proof>
</goal>
<goal name="VC create.12.1" expl="precondition" proved="true">
<transf name="split_vc" proved="true" >
<goal name="VC create.12.1.0" expl="precondition" proved="true">
<proof prover="1"><result status="valid" time="0.42"/></proof>
<proof prover="1"><result status="valid" time="0.07"/></proof>
</goal>
<goal name="VC create.12.1.1" expl="precondition" proved="true">
<proof prover="1"><result status="valid" time="0.40"/></proof>
<proof prover="1"><result status="valid" time="0.06"/></proof>
</goal>
</transf>
</goal>
<goal name="VC create.12.2" expl="precondition" proved="true">
<proof prover="1"><result status="valid" time="0.60"/></proof>
<proof prover="1"><result status="valid" time="0.12"/></proof>
</goal>
</transf>
</goal>
<goal name="VC create.13" expl="postcondition" proved="true">
<proof prover="1"><result status="valid" time="0.23"/></proof>
<proof prover="1"><result status="valid" time="0.04"/></proof>
</goal>
<goal name="VC create.14" expl="postcondition" proved="true">
<proof prover="1"><result status="valid" time="0.24"/></proof>
<proof prover="1"><result status="valid" time="0.03"/></proof>
</goal>
<goal name="VC create.15" expl="postcondition" proved="true">
<proof prover="1"><result status="valid" time="0.22"/></proof>
<proof prover="1"><result status="valid" time="0.03"/></proof>
</goal>
</transf>
</goal>
<goal name="Iterator.VC is_empty" expl="VC for is_empty" proved="true">
<proof prover="2"><result status="valid" time="0.82"/></proof>
<proof prover="2"><result status="valid" time="0.17"/></proof>
</goal>
<goal name="Iterator.VC next" expl="VC for next" proved="true">
<transf name="split_vc" proved="true" >
<goal name="VC next.0" expl="assertion" proved="true">
<proof prover="0"><result status="valid" time="0.14" steps="78"/></proof>
<proof prover="0"><result status="valid" time="0.02" steps="86"/></proof>
</goal>
<goal name="VC next.1" expl="index in array bounds" proved="true">
<proof prover="1"><result status="valid" time="0.41"/></proof>
<proof prover="1"><result status="valid" time="0.06"/></proof>
</goal>
<goal name="VC next.2" expl="integer overflow" proved="true">
<proof prover="1"><result status="valid" time="0.44"/></proof>
<proof prover="1"><result status="valid" time="0.06"/></proof>
</goal>
<goal name="VC next.3" expl="loop invariant init" proved="true">
<proof prover="1"><result status="valid" time="0.32"/></proof>
<proof prover="1"><result status="valid" time="0.05"/></proof>
</goal>
<goal name="VC next.4" expl="loop invariant init" proved="true">
<proof prover="1"><result status="valid" time="0.39"/></proof>
<proof prover="1"><result status="valid" time="0.06"/></proof>
</goal>
<goal name="VC next.5" expl="index in array bounds" proved="true">
<proof prover="1"><result status="valid" time="0.43"/></proof>
<proof prover="1"><result status="valid" time="0.08"/></proof>
</goal>
<goal name="VC next.6" expl="integer overflow" proved="true">
<proof prover="1"><result status="valid" time="0.43"/></proof>
<proof prover="1"><result status="valid" time="0.06"/></proof>
</goal>
<goal name="VC next.7" expl="loop variant decrease" proved="true">
<proof prover="1"><result status="valid" time="0.36"/></proof>
<proof prover="1"><result status="valid" time="0.05"/></proof>
</goal>
<goal name="VC next.8" expl="loop invariant preservation" proved="true">
<proof prover="1"><result status="valid" time="0.34"/></proof>
<proof prover="1"><result status="valid" time="0.05"/></proof>
</goal>
<goal name="VC next.9" expl="loop invariant preservation" proved="true">
<proof prover="1"><result status="valid" time="0.50"/></proof>
<proof prover="1"><result status="valid" time="0.08"/></proof>
</goal>
<goal name="VC next.10" expl="assertion" proved="true">
<proof prover="1"><result status="valid" time="0.49"/></proof>
<proof prover="1"><result status="valid" time="0.08"/></proof>
</goal>
<goal name="VC next.11" expl="type invariant" proved="true">
<proof prover="1"><result status="valid" time="0.72"/></proof>
<proof prover="1"><result status="valid" time="0.12"/></proof>
</goal>
<goal name="VC next.12" expl="type invariant" proved="true">
<proof prover="1"><result status="valid" time="0.51"/></proof>
<proof prover="1"><result status="valid" time="0.07"/></proof>
</goal>
<goal name="VC next.13" expl="type invariant" proved="true">
<proof prover="1"><result status="valid" time="0.55"/></proof>
<proof prover="1"><result status="valid" time="0.08"/></proof>
</goal>
<goal name="VC next.14" expl="type invariant" proved="true">
<proof prover="1"><result status="valid" time="0.56"/></proof>
<proof prover="1"><result status="valid" time="0.09"/></proof>
</goal>
<goal name="VC next.15" expl="type invariant" proved="true">
<proof prover="1"><result status="valid" time="1.58"/></proof>
<proof prover="1"><result status="valid" time="0.58"/></proof>
</goal>
<goal name="VC next.16" expl="type invariant" proved="true">
<proof prover="1"><result status="valid" time="0.78"/></proof>
<proof prover="1"><result status="valid" time="0.13"/></proof>
</goal>
<goal name="VC next.17" expl="postcondition" proved="true">
<proof prover="1"><result status="valid" time="0.68"/></proof>
<proof prover="1"><result status="valid" time="0.12"/></proof>
</goal>
<goal name="VC next.18" expl="postcondition" proved="true">
<proof prover="1"><result status="valid" time="0.29"/></proof>
<proof prover="1"><result status="valid" time="0.04"/></proof>
</goal>
<goal name="VC next.19" expl="postcondition" proved="true">
<proof prover="1"><result status="valid" time="0.27"/></proof>
<proof prover="1"><result status="valid" time="0.04"/></proof>
</goal>
</transf>
</goal>
......
stdlib/mach/tagset.mlw
+ 9
− 9
View file @ b800fea5
......@@ -35,7 +35,7 @@ module TagSetIntf
type iteration_state = mutable { }
type t = abstract {
mutable elts: S.set key;
mutable elts: S.fset key;
mutable iterated: iteration_state;
}
invariant { not (S.mem S.dummy elts) }
......@@ -66,9 +66,9 @@ module TagSetIntf
type iterator = abstract {
iterating: iteration_state;
mutable seen: S.set key;
mutable todo: S.set key;
all: S.set key;
mutable seen: S.fset key;
mutable todo: S.fset key;
all: S.fset key;
}
invariant { S.(union seen todo == all) }
invariant { S.(inter seen todo == S.empty) }
......@@ -118,7 +118,7 @@ module TagSet
clone import S as S with axiom tag_correct
type iteration_state = mutable {
ghost mutable elts': S.set key;
ghost mutable elts': S.fset key;
mutable value: array key;
}
invariant { not (S.mem S.dummy elts') }
......@@ -132,7 +132,7 @@ module TagSet
}
type t = {
ghost mutable elts: S.set key;
ghost mutable elts: S.fset key;
mutable iterated: iteration_state;
}
invariant { elts = iterated.elts' }
......@@ -204,9 +204,9 @@ module TagSet
type iterator = {
iterating: iteration_state;
ghost mutable seen: S.set key;
ghost mutable todo: S.set key;
ghost all: S.set key;
ghost mutable seen: S.fset key;
ghost mutable todo: S.fset key;
ghost all: S.fset key;
mutable offset: int63;
}
invariant { S.(==) all (S.union seen todo) }
......
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment