Commit 85f18744 authored by MARCHE Claude's avatar MARCHE Claude

update sessions, once again

parent d3098e35
......@@ -12,14 +12,14 @@ theory int.EuclideanDivision
(* protection against wrongs semantics for negative arguments *)
prelude "logic safe_div: int, int -> int"
prelude "axiom safe_div_def: forall x, y:int. x >= 0 and y > 0 -> safe_div(x,y) = x / y"
prelude "logic safe_eucl_div: int, int -> int"
prelude "axiom safe_eucl_div_def: forall x, y:int. x >= 0 and y > 0 -> safe_eucl_div(x,y) = x / y"
prelude "logic safe_mod: int, int -> int"
prelude "axiom safe_mod_def: forall x, y:int. x >= 0 and y > 0 -> safe_mod(x,y) = x % y"
prelude "logic safe_eucl_mod: int, int -> int"
prelude "axiom safe_eucl_mod_def: forall x, y:int. x >= 0 and y > 0 -> safe_eucl_mod(x,y) = x % y"
syntax function div "safe_div(%1,%2)"
syntax function mod "safe_mod(%1,%2)"
syntax function div "safe_eucl_div(%1,%2)"
syntax function mod "safe_eucl_mod(%1,%2)"
end
......@@ -27,14 +27,14 @@ theory int.ComputerDivision
(* protection against wrongs semantics for negative arguments *)
prelude "logic safe_div: int, int -> int"
prelude "axiom safe_div_def: forall x, y:int. x >= 0 and y > 0 -> safe_div(x,y) = x / y"
prelude "logic safe_comp_div: int, int -> int"
prelude "axiom safe_comp_div_def: forall x, y:int. x >= 0 and y > 0 -> safe_comp_div(x,y) = x / y"
prelude "logic safe_mod: int, int -> int"
prelude "axiom safe_mod_def: forall x, y:int. x >= 0 and y > 0 -> safe_mod(x,y) = x % y"
prelude "logic safe_comp_mod: int, int -> int"
prelude "axiom safe_comp_mod_def: forall x, y:int. x >= 0 and y > 0 -> safe_comp_mod(x,y) = x % y"
syntax function div "safe_div(%1,%2)"
syntax function mod "safe_mod(%1,%2)"
syntax function div "safe_comp_div(%1,%2)"
syntax function mod "safe_comp_mod(%1,%2)"
end
......
......@@ -14,14 +14,14 @@ theory int.EuclideanDivision
(* protection against wrongs semantics for negative arguments *)
prelude "logic safe_div: int, int -> int"
prelude "axiom safe_div_def: forall x, y:int. x >= 0 and y > 0 -> safe_div(x,y) = x / y"
prelude "logic safe_eucl_div: int, int -> int"
prelude "axiom safe_eucl_div_def: forall x, y:int. x >= 0 and y > 0 -> safe_eucl_div(x,y) = x / y"
prelude "logic safe_mod: int, int -> int"
prelude "axiom safe_mod_def: forall x, y:int. x >= 0 and y > 0 -> safe_mod(x,y) = x % y"
prelude "logic safe_eucl_mod: int, int -> int"
prelude "axiom safe_eucl_mod_def: forall x, y:int. x >= 0 and y > 0 -> safe_eucl_mod(x,y) = x % y"
syntax function div "safe_div(%1,%2)"
syntax function mod "safe_mod(%1,%2)"
syntax function div "safe_eucl_div(%1,%2)"
syntax function mod "safe_eucl_mod(%1,%2)"
end
......@@ -29,14 +29,14 @@ theory int.ComputerDivision
(* protection against wrongs semantics for negative arguments *)
prelude "logic safe_div: int, int -> int"
prelude "axiom safe_div_def: forall x, y:int. x >= 0 and y > 0 -> safe_div(x,y) = x / y"
prelude "logic safe_comp_div: int, int -> int"
prelude "axiom safe_comp_div_def: forall x, y:int. x >= 0 and y > 0 -> safe_comp_div(x,y) = x / y"
prelude "logic safe_mod: int, int -> int"
prelude "axiom safe_mod_def: forall x, y:int. x >= 0 and y > 0 -> safe_mod(x,y) = x % y"
prelude "logic safe_comp_mod: int, int -> int"
prelude "axiom safe_comp_mod_def: forall x, y:int. x >= 0 and y > 0 -> safe_comp_mod(x,y) = x % y"
syntax function div "safe_div(%1,%2)"
syntax function mod "safe_mod(%1,%2)"
syntax function div "safe_comp_div(%1,%2)"
syntax function mod "safe_comp_mod(%1,%2)"
end
......
......@@ -35,7 +35,7 @@
name="G1"
locfile="../euclideandivision.why"
loclnum="3" loccnumb="12" loccnume="14"
sum="5b1ad7dfa71a095a49fe7eefd285d02a"
sum="41b42e03fbdbb9d64932bed5e2aa561b"
proved="true"
expanded="true"
shape="ainfix =amodc10c3c1">
......@@ -84,7 +84,7 @@
name="G2"
locfile="../euclideandivision.why"
loclnum="4" loccnumb="12" loccnume="14"
sum="a5683429d73e76f0beb1819e6121cd60"
sum="1c1451b6fefb0560c2d11e28531ac284"
proved="true"
expanded="true"
shape="ainfix =adivc10c3c3">
......
......@@ -179,7 +179,7 @@
locfile="../fibonacci.mlw"
loclnum="82" loccnumb="10" loccnume="16"
expl="VC for logfib"
sum="be18b57a378e8f58833c62cc4852ff5c"
sum="dbb1fd041019fd31fd673671a0b16d35"
proved="true"
expanded="true"
shape="iainfix =V0c0ainfix =apoweramk tc1c1c1c0V0amk tainfix +c1c0c0c0c1iainfix =amodV0c2c0ainfix =apoweramk tc1c1c1c0V0amk tainfix +V3V4V4V4V3Lainfix *V2ainfix +V1ainfix +V1V2Lainfix +ainfix *V1V1ainfix *V2V2ainfix =apoweramk tc1c1c1c0V0amk tainfix +V5V6V6V6V5Lainfix +ainfix *ainfix +V1V2ainfix +V1V2ainfix *V2V2Lainfix *V2ainfix +V1ainfix +V1V2Iainfix =apoweramk tc1c1c1c0adivV0c2amk tainfix +V1V2V2V2V1FAainfix >=adivV0c2c0Aainfix <adivV0c2V0Aainfix <=c0V0Iainfix >=V0c0F">
......@@ -194,7 +194,7 @@
locfile="../fibonacci.mlw"
loclnum="82" loccnumb="10" loccnume="16"
expl="1. postcondition"
sum="54ff9f48d80a0d661479ac9f4110b022"
sum="522e915616232e68873a53b4174b074a"
proved="true"
expanded="true"
shape="ainfix =apoweramk tc1c1c1c0V0amk tainfix +c1c0c0c0c1Iainfix =V0c0Iainfix >=V0c0F">
......@@ -238,7 +238,7 @@
locfile="../fibonacci.mlw"
loclnum="82" loccnumb="10" loccnume="16"
expl="2. variant decrease"
sum="024ee6b3b1eb5f5cb113823603c892cf"
sum="ff1fdb8fdd9b95db7b509de9e6b3285c"
proved="true"
expanded="true"
shape="ainfix <adivV0c2V0Aainfix <=c0V0Iainfix =V0c0NIainfix >=V0c0F">
......@@ -258,7 +258,7 @@
locfile="../fibonacci.mlw"
loclnum="82" loccnumb="10" loccnume="16"
expl="3. precondition"
sum="f98d6f543cdf82e62fc44c18db5e7230"
sum="c3fab51f5189feeb6d55b36867db47a7"
proved="true"
expanded="true"
shape="ainfix >=adivV0c2c0Iainfix =V0c0NIainfix >=V0c0F">
......@@ -286,7 +286,7 @@
locfile="../fibonacci.mlw"
loclnum="82" loccnumb="10" loccnume="16"
expl="4. postcondition"
sum="4124e6c67675b5e5aa3e4feca51111a1"
sum="e0bdbf956c9d4717024dae02ce154e6c"
proved="true"
expanded="true"
shape="iainfix =amodV0c2c0ainfix =apoweramk tc1c1c1c0V0amk tainfix +V3V4V4V4V3Lainfix *V2ainfix +V1ainfix +V1V2Lainfix +ainfix *V1V1ainfix *V2V2ainfix =apoweramk tc1c1c1c0V0amk tainfix +V5V6V6V6V5Lainfix +ainfix *ainfix +V1V2ainfix +V1V2ainfix *V2V2Lainfix *V2ainfix +V1ainfix +V1V2Iainfix =apoweramk tc1c1c1c0adivV0c2amk tainfix +V1V2V2V2V1FIainfix >=adivV0c2c0Iainfix =V0c0NIainfix >=V0c0F">
......@@ -308,7 +308,7 @@
name="fib_m"
locfile="../fibonacci.mlw"
loclnum="105" loccnumb="8" loccnume="13"
sum="a63b2ce2736615025314f4148f50ebfc"
sum="5dc150c77ccd04a05e5575dc1f1d0194"
proved="true"
expanded="true"
shape="ainfix =afibV0aa21V1Aainfix =afibainfix +V0c1aa11V1Lapoweram1110V0Iainfix >=V0c0F">
......@@ -327,7 +327,7 @@
locfile="../fibonacci.mlw"
loclnum="109" loccnumb="6" loccnume="10"
expl="VC for fibo"
sum="c3f07c9fe36f4699cf6d127472aa26e7"
sum="a5ecdb49d122473f5a240831937d6f48"
proved="true"
expanded="false"
shape="ainfix =V2afibV0Iainfix =apoweramk tc1c1c1c0V0amk tainfix +V1V2V2V2V1FAainfix >=V0c0Iainfix >=V0c0F">
......
......@@ -36,7 +36,7 @@
locfile="../gcd.mlw"
loclnum="10" loccnumb="10" loccnume="13"
expl="VC for gcd"
sum="56380e19c2b5b0c876cbe75f8f68d59a"
sum="75ace293f095d31bd096cf04b02fa969"
proved="true"
expanded="true"
shape="iainfix =V1c0ainfix =V0agcdV0V1ainfix =agcdV1amodV0V1agcdV0V1Aainfix >=amodV0V1c0Aainfix >=V1c0Aainfix <amodV0V1V1Aainfix <=c0V1Iainfix >=V1c0Aainfix >=V0c0F">
......@@ -51,7 +51,7 @@
locfile="../gcd.mlw"
loclnum="10" loccnumb="10" loccnume="13"
expl="1. postcondition"
sum="aff67e94d75b8c6f0e60f082ef4fb444"
sum="43faee0bc174e6a5146e7cad8c8327ff"
proved="true"
expanded="true"
shape="ainfix =V0agcdV0V1Iainfix =V1c0Iainfix >=V1c0Aainfix >=V0c0F">
......@@ -87,7 +87,7 @@
locfile="../gcd.mlw"
loclnum="10" loccnumb="10" loccnume="13"
expl="2. variant decrease"
sum="4b4c39ee1875678b00e9c7b278a9c92b"
sum="28c81ed537595e729ecbe25f39c8fa0e"
proved="true"
expanded="true"
shape="ainfix <amodV0V1V1Aainfix <=c0V1Iainfix =V1c0NIainfix >=V1c0Aainfix >=V0c0F">
......@@ -99,7 +99,7 @@
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.21"/>
<result status="valid" time="0.24"/>
</proof>
<proof
prover="2"
......@@ -115,7 +115,7 @@
locfile="../gcd.mlw"
loclnum="10" loccnumb="10" loccnume="13"
expl="3. precondition"
sum="71ef822c09945728e72bb556c54c079b"
sum="0d4b85ba4d93f8d8571d0e20b7c0ae0f"
proved="true"
expanded="true"
shape="ainfix &gt;=amodV0V1c0Aainfix &gt;=V1c0Iainfix =V1c0NIainfix &gt;=V1c0Aainfix &gt;=V0c0F">
......@@ -151,7 +151,7 @@
locfile="../gcd.mlw"
loclnum="10" loccnumb="10" loccnume="13"
expl="4. postcondition"
sum="10b988e8ea93877fe03afeaeedba84b1"
sum="998f11fbe246e7958307c91622bc4300"
proved="true"
expanded="true"
shape="ainfix =agcdV1amodV0V1agcdV0V1Iainfix &gt;=amodV0V1c0Aainfix &gt;=V1c0Iainfix =V1c0NIainfix &gt;=V1c0Aainfix &gt;=V0c0F">
......
This diff is collapsed.
......@@ -200,7 +200,7 @@
name="test2"
locfile="../alt-ergo-models.why"
loclnum="31" loccnumb="5" loccnume="10"
sum="bd78811ee73cff3e51da3e1ed1f502e1"
sum="034acfca05980a946f398c1c7feed86e"
proved="false"
expanded="true"
shape="ainfix =adivV0V0c1F">
......@@ -217,7 +217,7 @@
name="test_overflow"
locfile="../alt-ergo-models.why"
loclnum="33" loccnumb="5" loccnume="18"
sum="1b6dc3ea74be047562b1f69f8f65b741"
sum="6241b04804f22123318a9afefb4d532b"
proved="false"
expanded="true"
shape="ainfix &lt;=ainfix +V0V1c65535Aainfix &lt;=c0ainfix +V0V1Iainfix &lt;=V1c65535Aainfix &lt;=c0V1Aainfix &lt;=V0c65535Aainfix &lt;=c0V0F">
......@@ -234,7 +234,7 @@
name="test_overflow2"
locfile="../alt-ergo-models.why"
loclnum="37" loccnumb="5" loccnume="19"
sum="4b58b728654ff2072f6317dcb41301eb"
sum="9da5be2c245573b39204248338a98e8b"
proved="false"
expanded="true"
shape="ainfix &lt;=ainfix +V0V1c65535Aainfix &lt;=aprefix -c2ainfix +V0V1Iainfix &lt;=V1c65535Aainfix &lt;=aprefix -c2V1Aainfix &lt;=V0c65535Aainfix &lt;=aprefix -c2V0F">
......@@ -251,7 +251,7 @@
name="test_overflow_int16"
locfile="../alt-ergo-models.why"
loclnum="43" loccnumb="5" loccnume="24"
sum="02c71d9f281a6838e6e470d03e9edf76"
sum="152576acfdb7547cd9594784c2d73c65"
proved="false"
expanded="true"
shape="ais_int16ainfix +V0V1Iais_int16V1Aais_int16V0F">
......@@ -268,7 +268,7 @@
name="test_overflow_int16_alt"
locfile="../alt-ergo-models.why"
loclnum="47" loccnumb="5" loccnume="28"
sum="43e5ab45c0e6488a38b842ca5b023b46"
sum="35cb59209eded0f668579236620f0b48"
proved="false"
expanded="true"
shape="ainfix &lt;=ainfix +V0V1c65535Aainfix &lt;=aprefix -c65536ainfix +V0V1Iainfix &lt;=V1c65535Aainfix &lt;=aprefix -c65536V1Aainfix &lt;=V0c65535Aainfix &lt;=aprefix -c65536V0F">
......@@ -285,7 +285,7 @@
name="test_overflow_int16_bis"
locfile="../alt-ergo-models.why"
loclnum="51" loccnumb="5" loccnume="28"
sum="ac90b3f950a194612b923c3993638d54"
sum="2da89b24c9c36d87c535a60197be18c8"
proved="false"
expanded="true"
shape="ais_int16ainfix +V0V1Iainfix &lt;=V0V1Aainfix &lt;=c0V0Aais_int16V1Aais_int16V0F">
......@@ -302,7 +302,7 @@
name="test_overflow_int32"
locfile="../alt-ergo-models.why"
loclnum="58" loccnumb="5" loccnume="24"
sum="fe1d83b19e02f37ccc5837ac472b3f09"
sum="07c221335e96bba1ff3acffca8b3bdd7"
proved="false"
expanded="true"
shape="ais_int32ainfix +V0V1Iais_int32V1Aais_int32V0F">
......@@ -319,7 +319,7 @@
name="test_overflow_int32_bis"
locfile="../alt-ergo-models.why"
loclnum="62" loccnumb="5" loccnume="28"
sum="8220a3f4d9bdd86e8067869ef1ccab3f"
sum="db492895a027e558b75308965d7b5579"
proved="false"
expanded="true"
shape="ais_int32ainfix +V0V1Iainfix &lt;=V0V1Aainfix &lt;=c0V0Aais_int32V1Aais_int32V0F">
......@@ -336,7 +336,7 @@
name="test_overflow_int32_bis_inline"
locfile="../alt-ergo-models.why"
loclnum="66" loccnumb="5" loccnume="35"
sum="0d9a8798aac56361d27bf4a7328d4196"
sum="d877b2055001c4f4cef6977f012a2113"
proved="false"
expanded="false"
shape="ainfix &lt;=ainfix +V0V1c2147483647Aainfix &lt;=aprefix -c2147483648ainfix +V0V1Iainfix &lt;=V0V1Aainfix &lt;=c0V0Aainfix &lt;=V1c2147483647Aainfix &lt;=aprefix -c2147483648V1Aainfix &lt;=V0c2147483647Aainfix &lt;=aprefix -c2147483648V0F">
......
......@@ -59,7 +59,7 @@
name="ok1"
locfile="../div.why"
loclnum="7" loccnumb="7" loccnume="10"
sum="eda768039e7d01cab7cc352411a0b275"
sum="28ae93babf67106fd24043960374f0c0"
proved="true"
expanded="false"
shape="ainfix =adivaprefix -c1c2aprefix -c1">
......@@ -115,9 +115,9 @@
prover="6"
timelimit="5"
memlimit="4000"
obsolete="true"
obsolete="false"
archived="false">
<result status="timeout" time="5.97"/>
<result status="timeout" time="5.23"/>
</proof>
<proof
prover="7"
......@@ -156,7 +156,7 @@
name="ok2"
locfile="../div.why"
loclnum="8" loccnumb="7" loccnume="10"
sum="b4d2e1617531911467f1b60798813040"
sum="3fe176fbe62afa2424f7dce33f6112b9"
proved="true"
expanded="false"
shape="ainfix =amodaprefix -c1c2c1">
......@@ -212,7 +212,7 @@
prover="6"
timelimit="5"
memlimit="4000"
obsolete="true"
obsolete="false"
archived="false">
<result status="timeout" time="5.97"/>
</proof>
......@@ -253,7 +253,7 @@
name="ok3"
locfile="../div.why"
loclnum="9" loccnumb="7" loccnume="10"
sum="059232a74443bb19214b21be9c8da104"
sum="9a6b1a5e5c19da08a720c9147571bf2c"
proved="true"
expanded="false"
shape="ainfix =adivaprefix -c1aprefix -c2c1">
......@@ -309,7 +309,7 @@
prover="6"
timelimit="5"
memlimit="4000"
obsolete="true"
obsolete="false"
archived="false">
<result status="timeout" time="5.96"/>
</proof>
......@@ -350,7 +350,7 @@
name="ok4"
locfile="../div.why"
loclnum="10" loccnumb="7" loccnume="10"
sum="88df0cd2db3816d5b578860b5c99c22e"
sum="a89220dc6f3c5c6578e0a543e588b3c6"
proved="true"
expanded="false"
shape="ainfix =amodaprefix -c1aprefix -c2c1">
......@@ -406,7 +406,7 @@
prover="6"
timelimit="5"
memlimit="4000"
obsolete="true"
obsolete="false"
archived="false">
<result status="timeout" time="5.98"/>
</proof>
......@@ -447,7 +447,7 @@
name="smoke1"
locfile="../div.why"
loclnum="11" loccnumb="7" loccnume="13"
sum="193a748bf5fbe6e02902fc1a40fd9f9c"
sum="ec9a1cd1d17fd9a099c2bb25848f3e76"
proved="false"
expanded="false"
shape="ainfix =adivaprefix -c1c2c0">
......@@ -457,7 +457,7 @@
memlimit="4000"
obsolete="false"
archived="false">
<result status="unknown" time="0.12"/>
<result status="unknown" time="0.28"/>
</proof>
<proof
prover="1"
......@@ -503,7 +503,7 @@
prover="6"
timelimit="5"
memlimit="4000"
obsolete="true"
obsolete="false"
archived="false">
<result status="timeout" time="5.98"/>
</proof>
......@@ -544,7 +544,7 @@
name="smoke2"
locfile="../div.why"
loclnum="12" loccnumb="7" loccnume="13"
sum="0ed544c77c77c905e1a3df3f81340665"
sum="a5dc7a7ca160a0fcb3c05b1b2a89544e"
proved="false"
expanded="false"
shape="ainfix =amodaprefix -c1c2aprefix -c1">
......@@ -554,7 +554,7 @@
memlimit="4000"
obsolete="false"
archived="false">
<result status="unknown" time="0.29"/>
<result status="unknown" time="0.62"/>
</proof>
<proof
prover="1"
......@@ -600,7 +600,7 @@
prover="6"
timelimit="5"
memlimit="4000"
obsolete="true"
obsolete="false"
archived="false">
<result status="timeout" time="5.96"/>
</proof>
......@@ -641,7 +641,7 @@
name="smoke3"
locfile="../div.why"
loclnum="13" loccnumb="7" loccnume="13"
sum="6a4df0cfd27e234f85fdef6b2f35a3a9"
sum="9122358d736b62c6b5d260410809ba66"
proved="false"
expanded="false"
shape="ainfix =adivaprefix -c1aprefix -c2c0">
......@@ -697,9 +697,9 @@
prover="6"
timelimit="5"
memlimit="4000"
obsolete="true"
obsolete="false"
archived="false">
<result status="timeout" time="5.97"/>
<result status="timeout" time="5.26"/>
</proof>
<proof
prover="7"
......@@ -738,7 +738,7 @@
name="smoke4"
locfile="../div.why"
loclnum="14" loccnumb="7" loccnume="13"
sum="f7cef8e1ec4ad2c7f55379a201bc33fc"
sum="ccdad4257ef5e0b90e9a1663aa87b6a6"
proved="false"
expanded="false"
shape="ainfix =amodaprefix -c1aprefix -c2aprefix -c1">
......@@ -794,7 +794,7 @@
prover="6"
timelimit="5"
memlimit="4000"
obsolete="true"
obsolete="false"
archived="false">
<result status="timeout" time="5.97"/>
</proof>
......@@ -898,7 +898,7 @@
prover="6"
timelimit="5"
memlimit="4000"
obsolete="true"
obsolete="false"
archived="false">
<result status="timeout" time="5.31"/>
</proof>
......@@ -995,7 +995,7 @@
prover="6"
timelimit="5"
memlimit="4000"
obsolete="true"
obsolete="false"
archived="false">
<result status="timeout" time="5.08"/>
</proof>
......@@ -1092,7 +1092,7 @@
prover="6"
timelimit="5"
memlimit="4000"
obsolete="true"
obsolete="false"
archived="false">
<result status="timeout" time="5.10"/>
</proof>
......@@ -1189,7 +1189,7 @@
prover="6"
timelimit="5"
memlimit="4000"
obsolete="true"
obsolete="false"
archived="false">
<result status="timeout" time="5.09"/>
</proof>
......@@ -1286,7 +1286,7 @@
prover="6"
timelimit="5"
memlimit="4000"
obsolete="true"
obsolete="false"
archived="false">
<result status="timeout" time="5.06"/>
</proof>
......@@ -1383,7 +1383,7 @@
prover="6"
timelimit="5"
memlimit="4000"
obsolete="true"
obsolete="false"
archived="false">
<result status="timeout" time="5.08"/>
</proof>
......@@ -1480,7 +1480,7 @@
prover="6"
timelimit="5"
memlimit="4000"
obsolete="true"
obsolete="false"
archived="false">
<result status="timeout" time="5.10"/>
</proof>
......@@ -1514,7 +1514,7 @@
memlimit="4000"
obsolete="false"
archived="false">
<result status="timeout" time="5.70"/>
<result status="timeout" time="5.01"/>
</proof>
</goal>
<goal
......@@ -1577,7 +1577,7 @@
prover="6"
timelimit="5"
memlimit="4000"
obsolete="true"
obsolete="false"
archived="false">
<result status="timeout" time="5.17"/>
</proof>
......
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