Skip to content

why3
why3
Commit c41a4218 authored by MARCHE Claude's avatar MARCHE Claude
Browse files
Options

More examples included in regression tests

parent ccad1159
Expand all Hide whitespace changes
Inline Side-by-side
Showing with 1771 additions and 82 deletions
examples/foveoos2011/array_max/why3session.xml
View file @ c41a4218
<?xml version="1.0" encoding="UTF-8"?>
<!DOCTYPE why3session SYSTEM "/home/marche/why3/share/why3session.dtd">
<!DOCTYPE why3session SYSTEM "/usr/local/share/why3/why3session.dtd">
<why3session
name="./foveoos2011/array_max/why3session.xml">
name="array_max/why3session.xml">
<prover
id="0"
name="Alt-Ergo"
......@@ -16,45 +16,48 @@
version="2.19"/>
<file
name="../array_max.mlw"
verified="false"
expanded="false">
verified="true"
expanded="true">
<theory
name="WP ArrayMax"
locfile="./foveoos2011/array_max/../array_max.mlw"
locfile="array_max/../array_max.mlw"
loclnum="14" loccnumb="7" loccnume="15"
verified="false"
verified="true"
expanded="true">
<goal
name="WP_parameter max"
locfile="./foveoos2011/array_max/../array_max.mlw"
locfile="array_max/../array_max.mlw"
loclnum="21" loccnumb="6" loccnume="9"
expl="parameter max"
sum="d352c899d3258c870d470a9bbd204e5a"
proved="false"
proved="true"
expanded="true"
shape="iainfix =V3V2Niainfix <=agetV1V3agetV1V2ainfix <ainfix -V2V4ainfix -V2V3Aainfix <=c0ainfix -V2V3Aainfix <=agetV1V5amaxagetV1V4agetV1V2Iainfix <V5V0Aainfix <V2V5Oainfix <V5V4Aainfix <=c0V5FAainfix <V2V0Aainfix <=V4V2Aainfix <=c0V4Iainfix =V4ainfix +V3c1Fainfix <ainfix -V6V3ainfix -V2V3Aainfix <=c0ainfix -V2V3Aainfix <=agetV1V7amaxagetV1V3agetV1V6Iainfix <V7V0Aainfix <V6V7Oainfix <V7V3Aainfix <=c0V7FAainfix <V6V0Aainfix <=V3V6Aainfix <=c0V3Iainfix =V6ainfix -V2c1FAainfix <V2V0Aainfix <=c0V2Aainfix <V3V0Aainfix <=c0V3ainfix <=agetV1V8agetV1V3Iainfix <V8V0Aainfix <=c0V8FAainfix <V3V0Aainfix <=c0V3Iainfix <=agetV1V9amaxagetV1V3agetV1V2Iainfix <V9V0Aainfix <V2V9Oainfix <V9V3Aainfix <=c0V9FAainfix <V2V0Aainfix <=V3V2Aainfix <=c0V3FFAainfix <=agetV1V10amaxagetV1c0agetV1ainfix -V0c1Iainfix <V10V0Aainfix <ainfix -V0c1V10Oainfix <V10c0Aainfix <=c0V10FAainfix <ainfix -V0c1V0Aainfix <=c0ainfix -V0c1Aainfix <=c0c0Iainfix <c0V0FF">
shape="iainfix =V3V2Niainfix &lt;=agetV1V3agetV1V2ainfix &lt;ainfix -V2V4ainfix -V2V3Aainfix &lt;=c0ainfix -V2V3Aainfix &lt;=agetV1V5amaxagetV1V4agetV1V2Iainfix &lt;V5V0Aainfix &lt;V2V5Oainfix &lt;V5V4Aainfix &lt;=c0V5FAainfix &lt;V2V0Aainfix &lt;=V4V2Aainfix &lt;=c0V4Iainfix =V4ainfix +V3c1Fainfix &lt;ainfix -V6V3ainfix -V2V3Aainfix &lt;=c0ainfix -V2V3Aainfix &lt;=agetV1V7amaxagetV1V3agetV1V6Iainfix &lt;V7V0Aainfix &lt;V6V7Oainfix &lt;V7V3Aainfix &lt;=c0V7FAainfix &lt;V6V0Aainfix &lt;=V3V6Aainfix &lt;=c0V3Iainfix =V6ainfix -V2c1FAainfix &lt;V2V0Aainfix &lt;=c0V2Aainfix &lt;V3V0Aainfix &lt;=c0V3ainfix &lt;=agetV1V8agetV1V3Iainfix &lt;V8V0Aainfix &lt;=c0V8FAainfix &lt;V3V0Aainfix &lt;=c0V3Iainfix &lt;=agetV1V9amaxagetV1V3agetV1V2Iainfix &lt;V9V0Aainfix &lt;V2V9Oainfix &lt;V9V3Aainfix &lt;=c0V9FAainfix &lt;V2V0Aainfix &lt;=V3V2Aainfix &lt;=c0V3FFAainfix &lt;=agetV1V10amaxagetV1c0agetV1ainfix -V0c1Iainfix &lt;V10V0Aainfix &lt;ainfix -V0c1V10Oainfix &lt;V10c0Aainfix &lt;=c0V10FAainfix &lt;ainfix -V0c1V0Aainfix &lt;=c0ainfix -V0c1Aainfix &lt;=c0c0Iainfix &lt;c0V0FF">
<label
name="expl:parameter max"/>
<proof
prover="2"
timelimit="5"
obsolete="true"
memlimit="0"
obsolete="false"
archived="false">
<result status="valid" time="0.05"/>
<result status="valid" time="0.02"/>
</proof>
<proof
prover="1"
timelimit="5"
obsolete="true"
memlimit="0"
obsolete="false"
archived="false">
<result status="valid" time="0.09"/>
<result status="valid" time="0.04"/>
</proof>
<proof
prover="0"
timelimit="5"
obsolete="true"
timelimit="7"
memlimit="0"
obsolete="false"
archived="false">
<result status="valid" time="3.46"/>
<result status="valid" time="2.32"/>
</proof>
</goal>
</theory>
......
examples/foveoos2011/duplets/why3session.xml
View file @ c41a4218
<?xml version="1.0" encoding="UTF-8"?>
<!DOCTYPE why3session SYSTEM "/home/marche/why3/share/why3session.dtd">
<!DOCTYPE why3session SYSTEM "/usr/local/share/why3/why3session.dtd">
<why3session
name="./foveoos2011/duplets/why3session.xml">
name="duplets/why3session.xml">
<prover
id="0"
name="Alt-Ergo"
......@@ -16,78 +16,83 @@
version="2.19"/>
<file
name="../duplets.mlw"
verified="false"
expanded="false">
verified="true"
expanded="true">
<theory
name="Option"
locfile="./foveoos2011/duplets/../duplets.mlw"
locfile="duplets/../duplets.mlw"
loclnum="15" loccnumb="7" loccnume="13"
verified="true"
expanded="true">
</theory>
<theory
name="WP Duplets"
locfile="./foveoos2011/duplets/../duplets.mlw"
locfile="duplets/../duplets.mlw"
loclnum="27" loccnumb="7" loccnume="14"
verified="false"
verified="true"
expanded="true">
<goal
name="WP_parameter duplet"
locfile="./foveoos2011/duplets/../duplets.mlw"
locfile="duplets/../duplets.mlw"
loclnum="43" loccnumb="6" loccnume="12"
expl="parameter duplet"
sum="be962a5577c9db0d565e6d563eba464e"
proved="false"
proved="true"
expanded="true"
shape="Lamk arrayV0V2ais_dupletV3V4V5NICV1aNonefaSomeVainfix =V6agetV2V4NIainfix <V5V0Aainfix <V4V5Aainfix <V4ainfix +ainfix -V0c2c1Aainfix <=c0V4FNALagetV2V7iCV1aNonefaSomeVainfix =V9V8ais_dupletV3V10V11NICV1aNonefaSomeVainfix =V12agetV2V10NIainfix <V11V0Aainfix <V10V11Aainfix <V10ainfix +V7c1Aainfix <=c0V10Fais_dupletV3V13V14NICV1aNonefaSomeVainfix =V15agetV2V13NIainfix <V14V0Aainfix <V13V14Aainfix <V13ainfix +V7c1Aainfix <=c0V13FIais_dupletV3V7V16NIainfix <V16ainfix +ainfix -V0c1c1Aainfix <V7V16FAiainfix =agetV2V17V8CV1aNonefaSomeVainfix =V20agetV2V18NAais_dupletV3V18V19Iainfix =aTuple2V18V19aTuple2V7V17Fais_dupletV3V7V21NIainfix <V21ainfix +V17c1Aainfix <V7V21FAainfix <V17V0Aainfix <=c0V17Iais_dupletV3V7V22NIainfix <V22V17Aainfix <V7V22FIainfix <=V17ainfix -V0c1Aainfix <=ainfix +V7c1V17FAais_dupletV3V7V23NIainfix <V23ainfix +V7c1Aainfix <V7V23FIainfix <=ainfix +V7c1ainfix -V0c1Aais_dupletV3V24V25NICV1aNonefaSomeVainfix =V26agetV2V24NIainfix <V25V0Aainfix <V24V25Aainfix <V24ainfix +V7c1Aainfix <=c0V24FIainfix >ainfix +V7c1ainfix -V0c1Aainfix <V7V0Aainfix <=c0V7Iais_dupletV3V27V28NICV1aNonefaSomeVainfix =V29agetV2V27NIainfix <V28V0Aainfix <V27V28Aainfix <V27V7Aainfix <=c0V27FIainfix <=V7ainfix -V0c2Aainfix <=c0V7FAais_dupletV3V30V31NICV1aNonefaSomeVainfix =V32agetV2V30NIainfix <V31V0Aainfix <V30V31Aainfix <V30c0Aainfix <=c0V30FIainfix <=c0ainfix -V0c2Aainfix >c0ainfix -V0c2NICV1aNonefaSomeVainfix =V35agetV2V33NAais_dupletV3V33V34EAainfix <=c2V0FFF">
shape="Lamk arrayV0V2ais_dupletV3V4V5NICV1aNonefaSomeVainfix =V6agetV2V4NIainfix &lt;V5V0Aainfix &lt;V4V5Aainfix &lt;V4ainfix +ainfix -V0c2c1Aainfix &lt;=c0V4FNALagetV2V7iCV1aNonefaSomeVainfix =V9V8ais_dupletV3V10V11NICV1aNonefaSomeVainfix =V12agetV2V10NIainfix &lt;V11V0Aainfix &lt;V10V11Aainfix &lt;V10ainfix +V7c1Aainfix &lt;=c0V10Fais_dupletV3V13V14NICV1aNonefaSomeVainfix =V15agetV2V13NIainfix &lt;V14V0Aainfix &lt;V13V14Aainfix &lt;V13ainfix +V7c1Aainfix &lt;=c0V13FIais_dupletV3V7V16NIainfix &lt;V16ainfix +ainfix -V0c1c1Aainfix &lt;V7V16FAiainfix =agetV2V17V8CV1aNonefaSomeVainfix =V20agetV2V18NAais_dupletV3V18V19Iainfix =aTuple2V18V19aTuple2V7V17Fais_dupletV3V7V21NIainfix &lt;V21ainfix +V17c1Aainfix &lt;V7V21FAainfix &lt;V17V0Aainfix &lt;=c0V17Iais_dupletV3V7V22NIainfix &lt;V22V17Aainfix &lt;V7V22FIainfix &lt;=V17ainfix -V0c1Aainfix &lt;=ainfix +V7c1V17FAais_dupletV3V7V23NIainfix &lt;V23ainfix +V7c1Aainfix &lt;V7V23FIainfix &lt;=ainfix +V7c1ainfix -V0c1Aais_dupletV3V24V25NICV1aNonefaSomeVainfix =V26agetV2V24NIainfix &lt;V25V0Aainfix &lt;V24V25Aainfix &lt;V24ainfix +V7c1Aainfix &lt;=c0V24FIainfix &gt;ainfix +V7c1ainfix -V0c1Aainfix &lt;V7V0Aainfix &lt;=c0V7Iais_dupletV3V27V28NICV1aNonefaSomeVainfix =V29agetV2V27NIainfix &lt;V28V0Aainfix &lt;V27V28Aainfix &lt;V27V7Aainfix &lt;=c0V27FIainfix &lt;=V7ainfix -V0c2Aainfix &lt;=c0V7FAais_dupletV3V30V31NICV1aNonefaSomeVainfix =V32agetV2V30NIainfix &lt;V31V0Aainfix &lt;V30V31Aainfix &lt;V30c0Aainfix &lt;=c0V30FIainfix &lt;=c0ainfix -V0c2Aainfix &gt;c0ainfix -V0c2NICV1aNonefaSomeVainfix =V35agetV2V33NAais_dupletV3V33V34EAainfix &lt;=c2V0FFF">
<label
name="expl:parameter duplet"/>
<proof
prover="2"
timelimit="5"
obsolete="true"
memlimit="0"
obsolete="false"
archived="false">
<result status="valid" time="0.14"/>
<result status="valid" time="0.06"/>
</proof>
<proof
prover="1"
timelimit="5"
obsolete="true"
memlimit="0"
obsolete="false"
archived="false">
<result status="valid" time="0.14"/>
<result status="valid" time="0.06"/>
</proof>
</goal>
<goal
name="WP_parameter duplets"
locfile="./foveoos2011/duplets/../duplets.mlw"
locfile="duplets/../duplets.mlw"
loclnum="75" loccnumb="6" loccnume="13"
expl="parameter duplets"
sum="65814ae1fd6df2639c018f0a16b5291a"
proved="false"
proved="true"
expanded="true"
shape="Lamk arrayV0V1LagetV1V4ainfix =agetV1V3agetV1V6NAais_dupletV2V6V7Aais_dupletV2V3V4Iainfix =V5agetV1V6NAais_dupletV2V6V7FAainfix =V5agetV1V8NAais_dupletV2V8V9EAainfix <=c2V0Aainfix <V4V0Aainfix <=c0V4Iais_dupletV2V3V4FAais_dupletV2V10V11EAainfix <=c2V0Iainfix =agetV1V12agetV1V14NAais_dupletV2V14V15Aais_dupletV2V12V13EAainfix <=c4V0FF">
shape="Lamk arrayV0V1LagetV1V4ainfix =agetV1V3agetV1V6NAais_dupletV2V6V7Aais_dupletV2V3V4Iainfix =V5agetV1V6NAais_dupletV2V6V7FAainfix =V5agetV1V8NAais_dupletV2V8V9EAainfix &lt;=c2V0Aainfix &lt;V4V0Aainfix &lt;=c0V4Iais_dupletV2V3V4FAais_dupletV2V10V11EAainfix &lt;=c2V0Iainfix =agetV1V12agetV1V14NAais_dupletV2V14V15Aais_dupletV2V12V13EAainfix &lt;=c4V0FF">
<label
name="expl:parameter duplets"/>
<proof
prover="2"
timelimit="5"
obsolete="true"
memlimit="0"
obsolete="false"
archived="false">
<result status="valid" time="0.05"/>
<result status="valid" time="0.02"/>
</proof>
<proof
prover="1"
timelimit="5"
obsolete="true"
memlimit="0"
obsolete="false"
archived="false">
<result status="valid" time="0.03"/>
<result status="valid" time="0.01"/>
</proof>
<proof
prover="0"
timelimit="5"
obsolete="true"
memlimit="0"
obsolete="false"
archived="false">
<result status="valid" time="0.06"/>
<result status="valid" time="0.02"/>
</proof>
</goal>
</theory>
......
examples/foveoos2011/tree_max/why3session.xml
View file @ c41a4218
<?xml version="1.0" encoding="UTF-8"?>
<!DOCTYPE why3session SYSTEM "/home/marche/why3/share/why3session.dtd">
<!DOCTYPE why3session SYSTEM "/usr/local/share/why3/why3session.dtd">
<why3session
name="./foveoos2011/tree_max/why3session.xml">
name="tree_max/why3session.xml">
<prover
id="0"
name="Alt-Ergo"
......@@ -9,95 +9,80 @@
<prover
id="1"
name="Coq"
version="8.3pl3"/>
<prover
id="2"
name="Z3"
version="2.19"/>
version="8.3pl4"/>
<file
name="../tree_max.mlw"
verified="false"
expanded="false">
verified="true"
expanded="true">
<theory
name="BinTree"
locfile="./foveoos2011/tree_max/../tree_max.mlw"
locfile="tree_max/../tree_max.mlw"
loclnum="26" loccnumb="7" loccnume="14"
verified="false"
verified="true"
expanded="true">
<goal
name="ge_trans"
locfile="./foveoos2011/tree_max/../tree_max.mlw"
locfile="tree_max/../tree_max.mlw"
loclnum="47" loccnumb="8" loccnume="16"
sum="a42fd40c97a8473c63c4df5f3809a29e"
proved="false"
proved="true"
expanded="true"
shape="age_treeV1V0Iage_treeV2V0Aainfix >=V1V2F">
shape="age_treeV1V0Iage_treeV2V0Aainfix &gt;=V1V2F">
<proof
prover="1"
timelimit="5"
memlimit="0"
edited="tree_max_BinTree_ge_trans_1.v"
obsolete="true"
obsolete="false"
archived="false">
<result status="valid" time="0.46"/>
<result status="valid" time="0.47"/>
</proof>
</goal>
</theory>
<theory
name="WP TreeMax"
locfile="./foveoos2011/tree_max/../tree_max.mlw"
locfile="tree_max/../tree_max.mlw"
loclnum="52" loccnumb="7" loccnume="14"
verified="false"
verified="true"
expanded="true">
<goal
name="WP_parameter max_aux"
locfile="./foveoos2011/tree_max/../tree_max.mlw"
locfile="tree_max/../tree_max.mlw"
loclnum="58" loccnumb="10" loccnume="17"
expl="parameter max_aux"
sum="fd19a0d15660fc84baa28f170db90b43"
proved="false"
proved="true"
expanded="true"
shape="CV0aNullainfix >=V1V1Aage_treeV1V0aTreeVVVamemV6V0Oainfix =V6V1Aainfix >=V6V1Aage_treeV6V0IamemV6V3Oainfix =V6V5Aainfix >=V6V5Aage_treeV6V3FIamemV5V4Oainfix =V5amaxV2V1Aainfix >=V5amaxV2V1Aage_treeV5V4FFF">
shape="CV0aNullainfix &gt;=V1V1Aage_treeV1V0aTreeVVVamemV6V0Oainfix =V6V1Aainfix &gt;=V6V1Aage_treeV6V0IamemV6V3Oainfix =V6V5Aainfix &gt;=V6V5Aage_treeV6V3FIamemV5V4Oainfix =V5amaxV2V1Aainfix &gt;=V5amaxV2V1Aage_treeV5V4FFF">
<label
name="expl:parameter max_aux"/>
<proof
prover="2"
timelimit="5"
obsolete="true"
archived="false">
<result status="valid" time="1.70"/>
</proof>
<proof
prover="0"
timelimit="5"
obsolete="true"
memlimit="0"
obsolete="false"
archived="false">
<result status="valid" time="0.06"/>
<result status="valid" time="0.04"/>
</proof>
</goal>
<goal
name="WP_parameter max"
locfile="./foveoos2011/tree_max/../tree_max.mlw"
locfile="tree_max/../tree_max.mlw"
loclnum="68" loccnumb="6" loccnume="9"
expl="parameter max"
sum="2b396ce2e0ce29212289ff83a143c14c"
proved="false"
proved="true"
expanded="true"
shape="CV0aNullfaTreeVVVamemV5V0Aage_treeV5V0IamemV5V2Oainfix =V5V4Aainfix >=V5V4Aage_treeV5V2FIamemV4V3Oainfix =V4V1Aainfix >=V4V1Aage_treeV4V3FIainfix =V0aNullNF">
shape="CV0aNullfaTreeVVVamemV5V0Aage_treeV5V0IamemV5V2Oainfix =V5V4Aainfix &gt;=V5V4Aage_treeV5V2FIamemV4V3Oainfix =V4V1Aainfix &gt;=V4V1Aage_treeV4V3FIainfix =V0aNullNF">
<label
name="expl:parameter max"/>
<proof
prover="2"
timelimit="5"
obsolete="true"
archived="false">
<result status="valid" time="0.05"/>
</proof>
<proof
prover="0"
timelimit="5"
obsolete="true"
memlimit="0"
obsolete="false"
archived="false">
<result status="valid" time="0.03"/>
<result status="valid" time="0.01"/>
</proof>
</goal>
</theory>
......
examples/programs/flag2.mlw 0 → 100644
View file @ c41a4218
(** {1 Dijkstra's "Dutch national flag"}
Variant which number of occurrences instead of permut predicate
*)
module Flag
use import int.Int
use import map.Map
use import module ref.Ref
type color = Blue | White | Red
predicate monochrome (a:map int color) (i:int) (j:int) (c:color) =
forall k:int. i <= k < j -> a[k]=c
function nb_occ (a:map int color) (i:int) (j:int) (c:color) : int
axiom nb_occ_null:
forall a:map int color, i j:int, c:color.
i >= j -> nb_occ a i j c = 0
axiom nb_occ_add:
forall a:map int color, i j:int, c:color.
i < j -> nb_occ a i j c = nb_occ a i (j-1) c +
(if get a (j-1) = c then 1 else 0)
lemma nb_occ_store:
forall a:map int color, i j k:int, c c':color.
i <= k < j ->
nb_occ (set a k c) i j c' =
nb_occ a i j c' + (if c=c' then 1 else 0) - (if get a k = c' then 1 else 0)
lemma nb_occ_store_outside:
forall a:map int color, i j k:int, c c':color.
not (i <= k < j) -> nb_occ (set a k c) i j c' = nb_occ a i j c'
let swap(a:ref (map int color)) (i:int) (j:int) : unit =
{ }
let ai = get !a i in
let aj = get !a j in
a := set !a i aj;
a := set !a j ai
{ get !a i = get (old !a) j /\
get !a j = get (old !a) i /\
(forall k:int. k <> i /\ k <> j -> get !a k = get (old !a) k) /\
(forall i j:int, c:color. nb_occ !a i j c = nb_occ (old !a) i j c)
}
let dutch_flag (a:ref (map int color)) (n:int) =
{ 0 <= n }
let b = ref 0 in
let i = ref 0 in
let r = ref n in
'Init:
while !i < !r do
invariant {
0 <= !b <= !i <= !r <= n /\
monochrome !a 0 !b Blue /\
monochrome !a !b !i White /\
monochrome !a !r n Red /\
forall c:color. nb_occ !a 0 n c = nb_occ (at !a 'Init) 0 n c }
variant { !r - !i }
match get !a !i with
| Blue -> swap a !b !i; b := !b + 1; i := !i + 1
| White -> i := !i + 1
| Red -> r := !r - 1; swap a !r !i
end
done
{ (exists b:int. exists r:int.
monochrome !a 0 b Blue /\
monochrome !a b r White /\
monochrome !a r n Red)
/\ forall c:color. nb_occ !a 0 n c = nb_occ (old !a) 0 n c }
end
(***
Local Variables:
compile-command: "unset LANG; make -C ../.. examples/programs/flag2.gui"
End:
*)
examples/programs/flag2/why3session.xml 0 → 100644
View file @ c41a4218
This diff is collapsed.
examples/regtests.sh
View file @ c41a4218
......@@ -73,6 +73,7 @@ echo "=== Programs in their own subdir ==="
run_dir programs/vacid_0_binary_heaps "-I programs/vacid_0_binary_heaps"
run_dir hoare_logic "-I hoare_logic"
run_dir bitvectors "-I bitvectors"
run_dir foveoos2011 "-I foveoos2011"
echo ""
echo "Summary: $success/$total"
......
share/why3session.dtd
View file @ c41a4218
......@@ -34,7 +34,8 @@
<!ELEMENT proof (result|undone)>
<!ATTLIST proof prover CDATA #REQUIRED>
<!ATTLIST proof timelimit CDATA #REQUIRED>
<!ATTLIST proof timelimit CDATA #IMPLIED>
<!ATTLIST proof memlimit CDATA #IMPLIED>
<!ATTLIST proof edited CDATA #IMPLIED>
<!ATTLIST proof obsolete CDATA #IMPLIED>
<!ATTLIST proof archived CDATA #IMPLIED>
......
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