Commit 9d269a3f authored by Guillaume Melquiond's avatar Guillaume Melquiond
Browse files

Remove some obsolete conversions between machine integers and unbounded integers.

parent fb5ed0f0
...@@ -85,10 +85,10 @@ module McCarthy91Mach ...@@ -85,10 +85,10 @@ module McCarthy91Mach
let rec f91 (n: int63) : int63 let rec f91 (n: int63) : int63
variant { 101 - n } variant { 101 - n }
ensures { result = spec n } ensures { result = spec n }
= if n <= of_int 100 then = if n <= 100 then
f91 (f91 (n + of_int 11)) f91 (f91 (n + 11))
else else
n - of_int 10 n - 10
use import mach.peano.Peano use import mach.peano.Peano
use import mach.int.Refint63 use import mach.int.Refint63
...@@ -101,11 +101,11 @@ module McCarthy91Mach ...@@ -101,11 +101,11 @@ module McCarthy91Mach
while gt !e zero do while gt !e zero do
invariant { !e >= 0 /\ iter spec !e !n = spec n0 } invariant { !e >= 0 /\ iter spec !e !n = spec n0 }
variant { 101 - !n + 10 * !e, !e:int } variant { 101 - !n + 10 * !e, !e:int }
if !n > Int63.of_int 100 then begin if !n > 100 then begin
n := !n - Int63.of_int 10; n := !n - 10;
e := pred !e e := pred !e
end else begin end else begin
n := !n + Int63.of_int 11; n := !n + 11;
e := succ !e e := succ !e
end end
done; done;
...@@ -124,11 +124,11 @@ module McCarthy91Mach ...@@ -124,11 +124,11 @@ module McCarthy91Mach
else !n = !(old n) + 11 /\ !e = !(old e) + 1 } else !n = !(old n) + 11 /\ !e = !(old e) + 1 }
raises { Stop -> !e = !(old e) = 0 /\ !n = !(old n) } raises { Stop -> !e = !(old e) = 0 /\ !n = !(old n) }
= if not (gt !e zero) then raise Stop; = if not (gt !e zero) then raise Stop;
if !n > Int63.of_int 100 then begin if !n > 100 then begin
n := !n - Int63.of_int 10; n := !n - 10;
e := pred !e e := pred !e
end else begin end else begin
n := !n + Int63.of_int 11; n := !n + 11;
e := succ !e e := succ !e
end end
in in
...@@ -137,8 +137,8 @@ module McCarthy91Mach ...@@ -137,8 +137,8 @@ module McCarthy91Mach
variant { 101 - !n } variant { 101 - !n }
ensures { !e = !(old e) - 1 /\ !n = spec !(old n) } ensures { !e = !(old e) - 1 /\ !n = spec !(old n) }
raises { Stop -> false } raises { Stop -> false }
= let u = !n in bloc (); if u <= Int63.of_int 100 then (aux (); aux ()) in = let u = !n in bloc (); if u <= 100 then (aux (); aux ()) in
try aux (); bloc (); absurd try aux (); bloc (); absurd
with Stop -> !n end with Stop -> !n end
end end
\ No newline at end of file
...@@ -3,27 +3,27 @@ ...@@ -3,27 +3,27 @@
"http://why3.lri.fr/why3session.dtd"> "http://why3.lri.fr/why3session.dtd">
<why3session shape_version="4"> <why3session shape_version="4">
<prover id="1" name="Alt-Ergo" version="1.30" timelimit="5" steplimit="0" memlimit="1000"/> <prover id="1" name="Alt-Ergo" version="1.30" timelimit="5" steplimit="0" memlimit="1000"/>
<file name="../mccarthy.mlw"> <file name="../mccarthy.mlw" proved="true">
<theory name="McCarthy91" sum="13b896e51d6f77e4be03ed7c66d03ca8"> <theory name="McCarthy91" proved="true" sum="13b896e51d6f77e4be03ed7c66d03ca8">
<goal name="VC f91" expl="VC for f91"> <goal name="VC f91" expl="VC for f91" proved="true">
<proof prover="1" timelimit="10"><result status="valid" time="0.00" steps="31"/></proof> <proof prover="1" timelimit="10"><result status="valid" time="0.00" steps="31"/></proof>
</goal> </goal>
<goal name="VC f91_nonrec" expl="VC for f91_nonrec"> <goal name="VC f91_nonrec" expl="VC for f91_nonrec" proved="true">
<proof prover="1" timelimit="10"><result status="valid" time="0.29" steps="517"/></proof> <proof prover="1" timelimit="10"><result status="valid" time="0.29" steps="517"/></proof>
</goal> </goal>
<goal name="VC f91_pseudorec" expl="VC for f91_pseudorec"> <goal name="VC f91_pseudorec" expl="VC for f91_pseudorec" proved="true">
<proof prover="1" timelimit="10"><result status="valid" time="0.01" steps="49"/></proof> <proof prover="1" timelimit="10"><result status="valid" time="0.01" steps="49"/></proof>
</goal> </goal>
</theory> </theory>
<theory name="McCarthy91Mach" sum="b37d5db478b81235db7385d87cd66422"> <theory name="McCarthy91Mach" proved="true" sum="7d4600e0ee1b08517405296863b5c9d8">
<goal name="VC f91" expl="VC for f91"> <goal name="VC f91" expl="VC for f91" proved="true">
<proof prover="1"><result status="valid" time="0.07" steps="336"/></proof> <proof prover="1"><result status="valid" time="0.07" steps="1067"/></proof>
</goal> </goal>
<goal name="VC f91_nonrec" expl="VC for f91_nonrec"> <goal name="VC f91_nonrec" expl="VC for f91_nonrec" proved="true">
<proof prover="1"><result status="valid" time="4.23" steps="10650"/></proof> <proof prover="1"><result status="valid" time="6.06" steps="12891"/></proof>
</goal> </goal>
<goal name="VC f91_pseudorec" expl="VC for f91_pseudorec"> <goal name="VC f91_pseudorec" expl="VC for f91_pseudorec" proved="true">
<proof prover="1"><result status="valid" time="0.26" steps="925"/></proof> <proof prover="1"><result status="valid" time="0.08" steps="432"/></proof>
</goal> </goal>
</theory> </theory>
</file> </file>
......
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