Commit 075c3788 authored by Mário Pereira's avatar Mário Pereira
Browse files

McCarthy's 91 function: machine integers implementation.

No extra annotations needed in order to prove overflow absence.
parent 88c5725a
......@@ -74,3 +74,71 @@ module McCarthy91
with Stop -> !n end
end
module McCarthy91Mach
use import int.Int
use import mach.int.Int63
function spec (x: int) : int = if x <= 100 then 91 else x-10
let rec f91 (n: int63) : int63
variant { 101 - n }
ensures { result = spec n }
= if n <= of_int 100 then
f91 (f91 (n + of_int 11))
else
n - of_int 10
use import mach.peano.Peano
use import mach.int.Refint63
use import int.Iter
let f91_nonrec (n0: int63) : int63
ensures { result = spec n0 }
= let e = ref one in
let n = ref n0 in
while gt !e zero do
invariant { !e >= 0 /\ iter spec !e !n = spec n0 }
variant { 101 - !n + 10 * !e, !e:int }
if !n > Int63.of_int 100 then begin
n := !n - Int63.of_int 10;
e := pred !e
end else begin
n := !n + Int63.of_int 11;
e := succ !e
end
done;
!n
exception Stop
let f91_pseudorec (n0: int63) : int63
ensures { result = spec n0 }
= let e = ref one in
let n = ref n0 in
let bloc () : unit
requires { !e >= 0 }
ensures { !(old e) > 0 }
ensures { if !(old n) > 100 then !n = !(old n) - 10 /\ !e = !(old e) - 1
else !n = !(old n) + 11 /\ !e = !(old e) + 1 }
raises { Stop -> !e = !(old e) = 0 /\ !n = !(old n) }
= if not (gt !e zero) then raise Stop;
if !n > Int63.of_int 100 then begin
n := !n - Int63.of_int 10;
e := pred !e
end else begin
n := !n + Int63.of_int 11;
e := succ !e
end
in
let rec aux () : unit
requires { !e > 0 }
variant { 101 - !n }
ensures { !e = !(old e) - 1 /\ !n = spec !(old n) }
raises { Stop -> false }
= let u = !n in bloc (); if u <= Int63.of_int 100 then (aux (); aux ()) in
try aux (); bloc (); absurd
with Stop -> !n end
end
\ No newline at end of file
......@@ -2,17 +2,28 @@
<!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN"
"http://why3.lri.fr/why3session.dtd">
<why3session shape_version="4">
<prover id="1" name="Alt-Ergo" version="1.30" timelimit="10" steplimit="0" memlimit="1000"/>
<file name="../mccarthy.mlw" expanded="true">
<theory name="McCarthy91" sum="13b896e51d6f77e4be03ed7c66d03ca8" expanded="true">
<goal name="VC f91" expl="VC for f91" expanded="true">
<proof prover="1"><result status="valid" time="0.00" steps="31"/></proof>
<prover id="1" name="Alt-Ergo" version="1.30" timelimit="5" steplimit="0" memlimit="1000"/>
<file name="../mccarthy.mlw">
<theory name="McCarthy91" sum="13b896e51d6f77e4be03ed7c66d03ca8">
<goal name="VC f91" expl="VC for f91">
<proof prover="1" timelimit="10"><result status="valid" time="0.00" steps="31"/></proof>
</goal>
<goal name="VC f91_nonrec" expl="VC for f91_nonrec" expanded="true">
<proof prover="1"><result status="valid" time="0.29" steps="517"/></proof>
<goal name="VC f91_nonrec" expl="VC for f91_nonrec">
<proof prover="1" timelimit="10"><result status="valid" time="0.29" steps="517"/></proof>
</goal>
<goal name="VC f91_pseudorec" expl="VC for f91_pseudorec" expanded="true">
<proof prover="1"><result status="valid" time="0.01" steps="49"/></proof>
<goal name="VC f91_pseudorec" expl="VC for f91_pseudorec">
<proof prover="1" timelimit="10"><result status="valid" time="0.01" steps="49"/></proof>
</goal>
</theory>
<theory name="McCarthy91Mach" sum="b37d5db478b81235db7385d87cd66422">
<goal name="VC f91" expl="VC for f91">
<proof prover="1"><result status="valid" time="0.07" steps="336"/></proof>
</goal>
<goal name="VC f91_nonrec" expl="VC for f91_nonrec">
<proof prover="1"><result status="valid" time="4.23" steps="10650"/></proof>
</goal>
<goal name="VC f91_pseudorec" expl="VC for f91_pseudorec">
<proof prover="1"><result status="valid" time="0.26" steps="925"/></proof>
</goal>
</theory>
</file>
......
......@@ -14,6 +14,9 @@ module Peano
val constant zero : t
ensures { result.v = 0 }
val constant one : t
ensures { result.v = 1 }
val succ (x: t) : t
ensures { result.v = x.v + 1 }
......@@ -74,4 +77,3 @@ module Peano
ensures { result.v = min x.v y.v }
end
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