Commit 24fc5f16 by Léon Gondelman

new example for balance

parent 37162168
 ... ... @@ -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
 ... ... @@ -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">
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!