Skip to content

GitLab

why3
why3
Commit 23718fa4 authored by Jean-Christophe Filliâtre's avatar Jean-Christophe Filliâtre
Browse files
Options

no more polymorphic equality in same_fringe

parent 7dc1d6dc
Hide whitespace changes
Inline Side-by-side
Showing with 58 additions and 56 deletions
examples/same_fringe.mlw
View file @ 23718fa4
......@@ -16,6 +16,8 @@ module SameFringe
type elt
val eq (x y: elt) : bool ensures { result <-> x=y }
type tree =
| Empty
| Node tree elt tree
......@@ -51,7 +53,7 @@ module SameFringe
| Done, Done ->
True
| Next x1 r1 e1, Next x2 r2 e2 ->
x1 = x2 && eq_enum (enum r1 e1) (enum r2 e2)
eq x1 x2 && eq_enum (enum r1 e1) (enum r2 e2)
| _ ->
False
end
......
examples/same_fringe/why3session.xml
View file @ 23718fa4
......@@ -26,9 +26,9 @@
<goal
name="WP_parameter enum"
locfile="../same_fringe.mlw"
loclnum="41" loccnumb="10" loccnume="14"
loclnum="43" loccnumb="10" loccnume="14"
expl="VC for enum"
sum="dece388278e53203fb21ab593b9766e2"
sum="454b49cc1ed963641e62e462bed21d30"
proved="true"
expanded="false"
shape="Cainfix =aenum_elementsV1ainfix ++aelementsV0aenum_elementsV1aEmptyainfix =aenum_elementsV5ainfix ++aelementsV0aenum_elementsV1Iainfix =aenum_elementsV5ainfix ++aelementsV2aenum_elementsaNextV3V4V1FACfaEmptyainfix =V7V2Oainfix =V6V2aNodeVwVV0aNodeVVVV0F">
......@@ -41,9 +41,9 @@
<goal
name="WP_parameter enum.1"
locfile="../same_fringe.mlw"
loclnum="41" loccnumb="10" loccnume="14"
loclnum="43" loccnumb="10" loccnume="14"
expl="1. postcondition"
sum="c39b4982043e7c317d71f63a1b994fd2"
sum="a1d6ed7b3d2ae45549f68dc77fe313cc"
proved="true"
expanded="false"
shape="postconditionCainfix =aenum_elementsV1ainfix ++aelementsV0aenum_elementsV1aEmptytaNodeVVVV0F">
......@@ -61,9 +61,9 @@
<goal
name="WP_parameter enum.2"
locfile="../same_fringe.mlw"
loclnum="41" loccnumb="10" loccnume="14"
loclnum="43" loccnumb="10" loccnume="14"
expl="2. variant decrease"
sum="48d2b3e5159f8443d419780710e6732a"
sum="9aaf056f6a364e340e0fef7ed78814cf"
proved="true"
expanded="false"
shape="variant decreaseCtaEmptyCfaEmptyainfix =V6V2Oainfix =V5V2aNodeVwVV0aNodeVVVV0F">
......@@ -81,9 +81,9 @@
<goal
name="WP_parameter enum.3"
locfile="../same_fringe.mlw"
loclnum="41" loccnumb="10" loccnume="14"
loclnum="43" loccnumb="10" loccnume="14"
expl="3. postcondition"
sum="e706015577dfcadc0f0841247655ce3d"
sum="d45868eb0dcaca8394ccee0186b4be95"
proved="true"
expanded="false"
shape="postconditionCtaEmptyainfix =aenum_elementsV5ainfix ++aelementsV0aenum_elementsV1Iainfix =aenum_elementsV5ainfix ++aelementsV2aenum_elementsaNextV3V4V1FaNodeVVVV0F">
......@@ -103,12 +103,12 @@
<goal
name="WP_parameter eq_enum"
locfile="../same_fringe.mlw"
loclnum="48" loccnumb="10" loccnume="17"
loclnum="50" loccnumb="10" loccnume="17"
expl="VC for eq_enum"
sum="833cb837dd9a705f9ac5833206ce541c"
sum="a89bd5d533bdacae7ff8a9461a4f1c9b"
proved="true"
expanded="false"
shape="CCiNainfix =aenum_elementsV0aenum_elementsV1ainfix =aenum_elementsV0aenum_elementsV1qainfix =V10aTrueIainfix =aenum_elementsV9aenum_elementsV8qainfix =V10aTrueFAainfix &lt;alengthaenum_elementsV9alengthaenum_elementsV0Aainfix &lt;=c0alengthaenum_elementsV0Iainfix =aenum_elementsV9ainfix ++aelementsV6aenum_elementsV7FIainfix =aenum_elementsV8ainfix ++aelementsV3aenum_elementsV4Fainfix =V5V2aNextVVVNainfix =aenum_elementsV0aenum_elementsV1wV0aNextVVVCainfix =aenum_elementsV0aenum_elementsV1aDoneNainfix =aenum_elementsV0aenum_elementsV1wV0aDoneV1F">
shape="CCiNainfix =aenum_elementsV0aenum_elementsV1ainfix =aenum_elementsV0aenum_elementsV1qainfix =V11aTrueIainfix =aenum_elementsV10aenum_elementsV9qainfix =V11aTrueFAainfix &lt;alengthaenum_elementsV10alengthaenum_elementsV0Aainfix &lt;=c0alengthaenum_elementsV0Iainfix =aenum_elementsV10ainfix ++aelementsV6aenum_elementsV7FIainfix =aenum_elementsV9ainfix ++aelementsV3aenum_elementsV4Fainfix =V8aTrueIainfix =V5V2qainfix =V8aTrueFaNextVVVNainfix =aenum_elementsV0aenum_elementsV1wV0aNextVVVCainfix =aenum_elementsV0aenum_elementsV1aDoneNainfix =aenum_elementsV0aenum_elementsV1wV0aDoneV1F">
<label
name="expl:VC for eq_enum"/>
<transf
......@@ -118,12 +118,12 @@
<goal
name="WP_parameter eq_enum.1"
locfile="../same_fringe.mlw"
loclnum="48" loccnumb="10" loccnume="17"
loclnum="50" loccnumb="10" loccnume="17"
expl="1. variant decrease"
sum="d0fa555508bd038432e667d8919268ed"
sum="5d5048f9a5aa2f2257cdf8a706776f29"
proved="true"
expanded="false"
shape="variant decreaseCCainfix &lt;alengthaenum_elementsV9alengthaenum_elementsV0Aainfix &lt;=c0alengthaenum_elementsV0Iainfix =aenum_elementsV9ainfix ++aelementsV6aenum_elementsV7FIainfix =aenum_elementsV8ainfix ++aelementsV3aenum_elementsV4FIainfix =V5V2aNextVVVtwV0aNextVVVtaDoneV1F">
shape="variant decreaseCCainfix &lt;alengthaenum_elementsV10alengthaenum_elementsV0Aainfix &lt;=c0alengthaenum_elementsV0Iainfix =aenum_elementsV10ainfix ++aelementsV6aenum_elementsV7FIainfix =aenum_elementsV9ainfix ++aelementsV3aenum_elementsV4FIainfix =V8aTrueIainfix =V5V2qainfix =V8aTrueFaNextVVVtwV0aNextVVVtaDoneV1F">
<label
name="expl:VC for eq_enum"/>
<proof
......@@ -146,12 +146,12 @@
<goal
name="WP_parameter eq_enum.2"
locfile="../same_fringe.mlw"
loclnum="48" loccnumb="10" loccnume="17"
loclnum="50" loccnumb="10" loccnume="17"
expl="2. postcondition"
sum="21714d4506aaef35ee0077ee790d8710"
sum="2bb6d015afe3cd416058cba880382aaf"
proved="true"
expanded="false"
shape="postconditionCCainfix =aenum_elementsV0aenum_elementsV1qainfix =V10aTrueIainfix =aenum_elementsV9aenum_elementsV8qainfix =V10aTrueFIainfix =aenum_elementsV9ainfix ++aelementsV6aenum_elementsV7FIainfix =aenum_elementsV8ainfix ++aelementsV3aenum_elementsV4FIainfix =V5V2aNextVVVtwV0aNextVVVtaDoneV1F">
shape="postconditionCCainfix =aenum_elementsV0aenum_elementsV1qainfix =V11aTrueIainfix =aenum_elementsV10aenum_elementsV9qainfix =V11aTrueFIainfix =aenum_elementsV10ainfix ++aelementsV6aenum_elementsV7FIainfix =aenum_elementsV9ainfix ++aelementsV3aenum_elementsV4FIainfix =V8aTrueIainfix =V5V2qainfix =V8aTrueFaNextVVVtwV0aNextVVVtaDoneV1F">
<label
name="expl:VC for eq_enum"/>
<proof
......@@ -166,12 +166,12 @@
<goal
name="WP_parameter eq_enum.3"
locfile="../same_fringe.mlw"
loclnum="48" loccnumb="10" loccnume="17"
loclnum="50" loccnumb="10" loccnume="17"
expl="3. postcondition"
sum="4b7cfc269f2124373901b7f87778edf1"
sum="cd274d75a5c6d7b45bd964009b05a6e0"
proved="true"
expanded="false"
shape="postconditionCCNainfix =aenum_elementsV0aenum_elementsV1INainfix =V5V2aNextVVVtwV0aNextVVVtaDoneV1F">
shape="postconditionCCNainfix =aenum_elementsV0aenum_elementsV1INainfix =V8aTrueIainfix =V5V2qainfix =V8aTrueFaNextVVVtwV0aNextVVVtaDoneV1F">
<label
name="expl:VC for eq_enum"/>
<proof
......@@ -186,9 +186,9 @@
<goal
name="WP_parameter eq_enum.4"
locfile="../same_fringe.mlw"
loclnum="48" loccnumb="10" loccnume="17"
loclnum="50" loccnumb="10" loccnume="17"
expl="4. postcondition"
sum="a71d1aa9338a4982790c15e744e0f431"
sum="d37d8a595da2ee2eac3357c4c53b2e73"
proved="true"
expanded="false"
shape="postconditionCCtaNextVVVNainfix =aenum_elementsV0aenum_elementsV1wV0aNextVVVtaDoneV1F">
......@@ -206,9 +206,9 @@
<goal
name="WP_parameter eq_enum.5"
locfile="../same_fringe.mlw"
loclnum="48" loccnumb="10" loccnume="17"
loclnum="50" loccnumb="10" loccnume="17"
expl="5. postcondition"
sum="389c887b301cfcbde02c3318e9519bad"
sum="d92a6f52f032120d6f10b23c1991db64"
proved="true"
expanded="false"
shape="postconditionCtaNextVVVCainfix =aenum_elementsV0aenum_elementsV1aDonetwV0aDoneV1F">
......@@ -226,9 +226,9 @@
<goal
name="WP_parameter eq_enum.6"
locfile="../same_fringe.mlw"
loclnum="48" loccnumb="10" loccnume="17"
loclnum="50" loccnumb="10" loccnume="17"
expl="6. postcondition"
sum="4c8d063a2f0cca5c654b2bd16cfa7f82"
sum="f44f29b9a1a023b8ea1f00719880c8a7"
proved="true"
expanded="false"
shape="postconditionCtaNextVVVCtaDoneNainfix =aenum_elementsV0aenum_elementsV1wV0aDoneV1F">
......@@ -248,9 +248,9 @@
<goal
name="WP_parameter same_fringe"
locfile="../same_fringe.mlw"
loclnum="59" loccnumb="6" loccnume="17"
loclnum="61" loccnumb="6" loccnume="17"
expl="VC for same_fringe"
sum="aa745433bbb4d79b0e1b66ccd053c7d3"
sum="e541dc833c30bb5a6e42aee77ffa9436"
proved="true"
expanded="false"
shape="ainfix =aelementsV0aelementsV1qainfix =V4aTrueIainfix =aenum_elementsV3aenum_elementsV2qainfix =V4aTrueFIainfix =aenum_elementsV3ainfix ++aelementsV0aenum_elementsaDoneFIainfix =aenum_elementsV2ainfix ++aelementsV1aenum_elementsaDoneFF">
......@@ -268,9 +268,9 @@
<goal
name="WP_parameter test1"
locfile="../same_fringe.mlw"
loclnum="63" loccnumb="6" loccnume="11"
loclnum="65" loccnumb="6" loccnume="11"
expl="VC for test1"
sum="0a9beb3d0997b6ca600b0febccc3b469"
sum="1426836a18ae0a33440eb84360028535"
proved="true"
expanded="false"
shape="t">
......@@ -288,9 +288,9 @@
<goal
name="WP_parameter test2"
locfile="../same_fringe.mlw"
loclnum="64" loccnumb="6" loccnume="11"
loclnum="66" loccnumb="6" loccnume="11"
expl="VC for test2"
sum="0a9beb3d0997b6ca600b0febccc3b469"
sum="1426836a18ae0a33440eb84360028535"
proved="true"
expanded="false"
shape="t">
......@@ -308,9 +308,9 @@
<goal
name="WP_parameter test3"
locfile="../same_fringe.mlw"
loclnum="65" loccnumb="6" loccnume="11"
loclnum="67" loccnumb="6" loccnume="11"
expl="VC for test3"
sum="0a9beb3d0997b6ca600b0febccc3b469"
sum="1426836a18ae0a33440eb84360028535"
proved="true"
expanded="false"
shape="t">
......@@ -328,9 +328,9 @@
<goal
name="WP_parameter leaf"
locfile="../same_fringe.mlw"
loclnum="70" loccnumb="6" loccnume="10"
loclnum="72" loccnumb="6" loccnume="10"
expl="VC for leaf"
sum="9020315c47e71b0301c59e758be57eb8"
sum="01ad6b6fcb7a77d600990a7a5eee4f20"
proved="true"
expanded="false"
shape="t">
......@@ -348,9 +348,9 @@
<goal
name="WP_parameter test4"
locfile="../same_fringe.mlw"
loclnum="72" loccnumb="6" loccnume="11"
loclnum="74" loccnumb="6" loccnume="11"
expl="VC for test4"
sum="9020315c47e71b0301c59e758be57eb8"
sum="01ad6b6fcb7a77d600990a7a5eee4f20"
proved="true"
expanded="false"
shape="t">
......@@ -368,9 +368,9 @@
<goal
name="WP_parameter test5"
locfile="../same_fringe.mlw"
loclnum="73" loccnumb="6" loccnume="11"
loclnum="75" loccnumb="6" loccnume="11"
expl="VC for test5"
sum="9020315c47e71b0301c59e758be57eb8"
sum="01ad6b6fcb7a77d600990a7a5eee4f20"
proved="true"
expanded="false"
shape="t">
......@@ -388,9 +388,9 @@
<goal
name="WP_parameter bench"
locfile="../same_fringe.mlw"
loclnum="77" loccnumb="6" loccnume="11"
loclnum="79" loccnumb="6" loccnume="11"
expl="VC for bench"
sum="9020315c47e71b0301c59e758be57eb8"
sum="01ad6b6fcb7a77d600990a7a5eee4f20"
proved="true"
expanded="false"
shape="t">
......@@ -409,15 +409,15 @@
<theory
name="Test"
locfile="../same_fringe.mlw"
loclnum="82" loccnumb="7" loccnume="11"
loclnum="84" loccnumb="7" loccnume="11"
verified="true"
expanded="true">
<goal
name="WP_parameter test1"
locfile="../same_fringe.mlw"
loclnum="87" loccnumb="6" loccnume="11"
loclnum="89" loccnumb="6" loccnume="11"
expl="VC for test1"
sum="d37ebc1cd434eba73675a2913c7a3548"
sum="ed83cf8f94dc7e606e1f92f92fed8d4b"
proved="true"
expanded="false"
shape="t">
......@@ -435,9 +435,9 @@
<goal
name="WP_parameter test2"
locfile="../same_fringe.mlw"
loclnum="88" loccnumb="6" loccnume="11"
loclnum="90" loccnumb="6" loccnume="11"
expl="VC for test2"
sum="d37ebc1cd434eba73675a2913c7a3548"
sum="ed83cf8f94dc7e606e1f92f92fed8d4b"
proved="true"
expanded="false"
shape="t">
......@@ -455,9 +455,9 @@
<goal
name="WP_parameter test3"
locfile="../same_fringe.mlw"
loclnum="89" loccnumb="6" loccnume="11"
loclnum="91" loccnumb="6" loccnume="11"
expl="VC for test3"
sum="d37ebc1cd434eba73675a2913c7a3548"
sum="ed83cf8f94dc7e606e1f92f92fed8d4b"
proved="true"
expanded="false"
shape="t">
......@@ -475,9 +475,9 @@
<goal
name="WP_parameter leaf"
locfile="../same_fringe.mlw"
loclnum="94" loccnumb="6" loccnume="10"
loclnum="96" loccnumb="6" loccnume="10"
expl="VC for leaf"
sum="cb3d58a8e5a4cd2167042439af66c371"
sum="dc55bd7369be012960b70e3e49ca6168"
proved="true"
expanded="false"
shape="t">
......@@ -495,9 +495,9 @@
<goal
name="WP_parameter test4"
locfile="../same_fringe.mlw"
loclnum="96" loccnumb="6" loccnume="11"
loclnum="98" loccnumb="6" loccnume="11"
expl="VC for test4"
sum="cb3d58a8e5a4cd2167042439af66c371"
sum="dc55bd7369be012960b70e3e49ca6168"
proved="true"
expanded="false"
shape="t">
......@@ -515,9 +515,9 @@
<goal
name="WP_parameter test5"
locfile="../same_fringe.mlw"
loclnum="97" loccnumb="6" loccnume="11"
loclnum="99" loccnumb="6" loccnume="11"
expl="VC for test5"
sum="cb3d58a8e5a4cd2167042439af66c371"
sum="dc55bd7369be012960b70e3e49ca6168"
proved="true"
expanded="false"
shape="t">
......
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