From 24fc5f1618969fee61a96c7641fafc3bba1336ee Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?L=C3=A9on=20Gondelman?= Date: Tue, 1 Apr 2014 10:03:03 +0200 Subject: [PATCH] new example for balance --- examples/balance.mlw | 64 ++++++++ examples/balance/why3session.xml | 241 +++++++++++++++++++++++++++---- 2 files changed, 274 insertions(+), 31 deletions(-) diff --git a/examples/balance.mlw b/examples/balance.mlw index 69724a939..a5c4f7078 100644 --- a/examples/balance.mlw +++ b/examples/balance.mlw @@ -50,3 +50,67 @@ module Balance if balls[6] < balls[7] then 6 else 7 end + + + +module Balance12 + + use import int.Int + use import array.Array + + (* All values in balls[lo..hi[ are equal to [w], apart from balls[lb] + which is of a different weight (lighter or heavier) . *) + predicate spec (balls: array int) (lo hi j: int) (w: int) (b: bool) = + 0 <= lo <= j < hi <= length balls && + (forall i: int. lo <= i < hi -> i <> j -> balls[i] = w) && + (if b then balls[j] < w else balls[j] > w) + + (* j : the index of the different ball, + b : the status (lighter or heavier) of the different ball + False True meaning heavier and True meaining lighter *) + let solve12 (balls: array int) (ghost w j: int) (ghost b: bool) : (int, bool) + requires { spec balls 0 12 j w b } + ensures { result = (j, b) } + = + if balls[0] + balls[1] + balls[2] + balls[3] = + balls[4] + balls[5] + balls[6] + balls[7] + then + if balls[0] + balls[8] = balls[9] + balls[10] + then + if balls[0] < balls[11] + then (11, False) + else (11, True) + else if balls[0] + balls[8] < balls[9] + balls[10] + then + if balls[9] = balls[10] then (8, True) + else if balls[9] < balls[10] then (10, False) else (9, False) + else + if balls[9] = balls[10] then (8, False) + else if balls[9] < balls[10] then (9, True) else (10, True) + else if balls[0] + balls[1] + balls[2] + balls[3] < + balls[4] + balls[5] + balls[6] + balls[7] + then + if balls[0] + balls[1] + balls[4] = balls[2] + balls[5] + balls[8] + then + if balls[6] = balls[7] then (3, True) + else if balls[6] < balls[7] then (7, False) else (6, False) + else if balls[0] + balls[1] + balls[4] < balls[2] + balls[5] + balls[8] + then + if balls[0] = balls[1] then (5, False) + else if balls[0] < balls[1] then (0, True) else (1, True) + else + if balls[4] = balls[8] then (2, True) else (4, False) + else + if balls[0] + balls[1] + balls[4] = balls[2] + balls[5] + balls[8] + then + if balls[6] = balls[7] then (3, False) + else if balls[6] < balls[7] then (6, True) else (7, True) + else if balls[0] + balls[1] + balls[4] < balls[2] + balls[5] + balls[8] + then + if balls[2] = balls[5] then (4, True ) + else if balls[2] < balls[5] then (5, False) else (2, False) + else + if balls[0] = balls[1] then (5, True) else + if balls[0] < balls[1] then (1, False) else (0, False) + +end \ No newline at end of file diff --git a/examples/balance/why3session.xml b/examples/balance/why3session.xml index 16e871394..b26cfa93f 100644 --- a/examples/balance/why3session.xml +++ b/examples/balance/why3session.xml @@ -5,6 +5,14 @@ id="0" name="Alt-Ergo" version="0.95.1"/> + + @@ -30,17 +38,25 @@ prover="0" timelimit="10" memlimit="1000" - obsolete="false" + obsolete="true" archived="false"> + + + @@ -55,7 +71,7 @@ locfile="../balance.mlw" loclnum="39" loccnumb="6" loccnume="12" expl="1. index in array bounds" - sum="b2d40a695281102206c57ffef269a7bb" + sum="6a926496ec2fc5fae3feee17218eafab" proved="true" expanded="false" shape="index in array boundsainfix <c5V0Aainfix <=c0c5IaspecV4c0c8V2V3Aainfix <=c0V0Lamk arrayV0V1F"> @@ -65,17 +81,25 @@ prover="0" timelimit="10" memlimit="1000" - obsolete="false" + obsolete="true" archived="false"> + + + @@ -85,6 +109,14 @@ prover="0" timelimit="10" memlimit="1000" + obsolete="true" + archived="false"> + + + @@ -95,7 +127,7 @@ locfile="../balance.mlw" loclnum="39" loccnumb="6" loccnume="12" expl="3. index in array bounds" - sum="f6912272fe1d882bc93fc208c49f7818" + sum="479606dd06d14fc5f000f81557cd09e9" proved="true" expanded="false" shape="index in array boundsainfix <c3V0Aainfix <=c0c3Iainfix <c4V0Aainfix <=c0c4Iainfix <c5V0Aainfix <=c0c5IaspecV4c0c8V2V3Aainfix <=c0V0Lamk arrayV0V1F"> @@ -105,6 +137,14 @@ prover="0" timelimit="10" memlimit="1000" + obsolete="true" + archived="false"> + + + @@ -115,7 +155,7 @@ locfile="../balance.mlw" loclnum="39" loccnumb="6" loccnume="12" expl="4. index in array bounds" - sum="312128fcc4d69b83a16700ff15607aff" + sum="9b1074d5dcdc780843225fac52f28c88" proved="true" expanded="false" shape="index in array boundsainfix <c2V0Aainfix <=c0c2Iainfix <c3V0Aainfix <=c0c3Iainfix <c4V0Aainfix <=c0c4Iainfix <c5V0Aainfix <=c0c5IaspecV4c0c8V2V3Aainfix <=c0V0Lamk arrayV0V1F"> @@ -125,6 +165,14 @@ prover="0" timelimit="10" memlimit="1000" + obsolete="true" + archived="false"> + + + @@ -135,7 +183,7 @@ locfile="../balance.mlw" loclnum="39" loccnumb="6" loccnume="12" expl="5. index in array bounds" - sum="c39db593354d8d388a14517730b5a4ae" + sum="ae8999d91cac2dc2f9f0c03bd79676b3" proved="true" expanded="false" shape="index in array boundsainfix <c1V0Aainfix <=c0c1Iainfix <c2V0Aainfix <=c0c2Iainfix <c3V0Aainfix <=c0c3Iainfix <c4V0Aainfix <=c0c4Iainfix <c5V0Aainfix <=c0c5IaspecV4c0c8V2V3Aainfix <=c0V0Lamk arrayV0V1F"> @@ -145,17 +193,25 @@ prover="0" timelimit="10" memlimit="1000" - obsolete="false" + obsolete="true" archived="false"> + + + @@ -165,6 +221,14 @@ prover="0" timelimit="10" memlimit="1000" + obsolete="true" + archived="false"> + + + @@ -175,7 +239,7 @@ locfile="../balance.mlw" loclnum="39" loccnumb="6" loccnume="12" expl="7. precondition" - sum="013f897984932d02e06a771270dc3d1f" + sum="34f24aec5759081fee36b1644c8429a2" proved="true" expanded="false" shape="preconditionaspecV4c0ainfix +c0c3V2V3Iainfix <ainfix +ainfix +agetV1c0agetV1c1agetV1c2ainfix +ainfix +agetV1c3agetV1c4agetV1c5Iainfix <c0V0Aainfix <=c0c0Iainfix <c1V0Aainfix <=c0c1Iainfix <c2V0Aainfix <=c0c2Iainfix <c3V0Aainfix <=c0c3Iainfix <c4V0Aainfix <=c0c4Iainfix <c5V0Aainfix <=c0c5IaspecV4c0c8V2V3Aainfix <=c0V0Lamk arrayV0V1F"> @@ -185,17 +249,25 @@ prover="0" timelimit="10" memlimit="1000" - obsolete="false" + obsolete="true" archived="false"> + + + @@ -205,17 +277,25 @@ prover="0" timelimit="10" memlimit="1000" - obsolete="false" + obsolete="true" archived="false"> + + + @@ -225,17 +305,25 @@ prover="0" timelimit="10" memlimit="1000" - obsolete="false" + obsolete="true" archived="false"> + + + @@ -245,17 +333,25 @@ prover="0" timelimit="10" memlimit="1000" - obsolete="false" + obsolete="true" archived="false"> + + + @@ -265,17 +361,25 @@ prover="0" timelimit="10" memlimit="1000" - obsolete="false" + obsolete="true" archived="false"> + + + @@ -285,6 +389,14 @@ prover="0" timelimit="10" memlimit="1000" + obsolete="true" + archived="false"> + + + @@ -295,7 +407,7 @@ locfile="../balance.mlw" loclnum="39" loccnumb="6" loccnume="12" expl="13. index in array bounds" - sum="690c698a413c66bc1693b12cb66955c7" + sum="b47140fc58b644b4ac9d5b7679aee6f6" proved="true" expanded="false" shape="index in array boundsainfix <c0V0Aainfix <=c0c0Iainfix <c1V0Aainfix <=c0c1Iainfix <c2V0Aainfix <=c0c2Iainfix <c3V0Aainfix <=c0c3Iainfix <c4V0Aainfix <=c0c4Iainfix <c5V0Aainfix <=c0c5INainfix <ainfix +ainfix +agetV1c0agetV1c1agetV1c2ainfix +ainfix +agetV1c3agetV1c4agetV1c5Iainfix <c0V0Aainfix <=c0c0Iainfix <c1V0Aainfix <=c0c1Iainfix <c2V0Aainfix <=c0c2Iainfix <c3V0Aainfix <=c0c3Iainfix <c4V0Aainfix <=c0c4Iainfix <c5V0Aainfix <=c0c5IaspecV4c0c8V2V3Aainfix <=c0V0Lamk arrayV0V1F"> @@ -305,6 +417,14 @@ prover="0" timelimit="10" memlimit="1000" + obsolete="true" + archived="false"> + + + @@ -315,7 +435,7 @@ locfile="../balance.mlw" loclnum="39" loccnumb="6" loccnume="12" expl="14. precondition" - sum="2620171d7414e045b8365fbe66eb3348" + sum="b3b8375d53b28e76a2d3682683a3c898" proved="true" expanded="false" shape="preconditionaspecV4c3ainfix +c3c3V2V3Iainfix >ainfix +ainfix +agetV1c0agetV1c1agetV1c2ainfix +ainfix +agetV1c3agetV1c4agetV1c5Iainfix <c0V0Aainfix <=c0c0Iainfix <c1V0Aainfix <=c0c1Iainfix <c2V0Aainfix <=c0c2Iainfix <c3V0Aainfix <=c0c3Iainfix <c4V0Aainfix <=c0c4Iainfix <c5V0Aainfix <=c0c5INainfix <ainfix +ainfix +agetV1c0agetV1c1agetV1c2ainfix +ainfix +agetV1c3agetV1c4agetV1c5Iainfix <c0V0Aainfix <=c0c0Iainfix <c1V0Aainfix <=c0c1Iainfix <c2V0Aainfix <=c0c2Iainfix <c3V0Aainfix <=c0c3Iainfix <c4V0Aainfix <=c0c4Iainfix <c5V0Aainfix <=c0c5IaspecV4c0c8V2V3Aainfix <=c0V0Lamk arrayV0V1F"> @@ -325,17 +445,25 @@ prover="0" timelimit="10" memlimit="1000" - obsolete="false" + obsolete="true" archived="false"> + + + @@ -345,17 +473,25 @@ prover="0" timelimit="10" memlimit="1000" - obsolete="false" + obsolete="true" archived="false"> + + + @@ -365,6 +501,14 @@ prover="0" timelimit="10" memlimit="1000" + obsolete="true" + archived="false"> + + + @@ -375,9 +519,9 @@ locfile="../balance.mlw" loclnum="39" loccnumb="6" loccnume="12" expl="17. postcondition" - sum="a3b67d2c6ba952e455a09a5cdfe83011" + sum="2440fb80af7ec657e33026f1e85b604f" proved="true" - expanded="true" + expanded="false" shape="postconditionainfix =ic7c6ainfix <agetV1c6agetV1c7V2Iainfix <c6V0Aainfix <=c0c6Iainfix <c7V0Aainfix <=c0c7INainfix >ainfix +ainfix +agetV1c0agetV1c1agetV1c2ainfix +ainfix +agetV1c3agetV1c4agetV1c5Iainfix <c0V0Aainfix <=c0c0Iainfix <c1V0Aainfix <=c0c1Iainfix <c2V0Aainfix <=c0c2Iainfix <c3V0Aainfix <=c0c3Iainfix <c4V0Aainfix <=c0c4Iainfix <c5V0Aainfix <=c0c5INainfix <ainfix +ainfix +agetV1c0agetV1c1agetV1c2ainfix +ainfix +agetV1c3agetV1c4agetV1c5Iainfix <c0V0Aainfix <=c0c0Iainfix <c1V0Aainfix <=c0c1Iainfix <c2V0Aainfix <=c0c2Iainfix <c3V0Aainfix <=c0c3Iainfix <c4V0Aainfix <=c0c4Iainfix <c5V0Aainfix <=c0c5IaspecV4c0c8V2V3Aainfix <=c0V0Lamk arrayV0V1F"> + + + + + + + -- GitLab