Commit 07d327b3 authored by Guillaume Melquiond's avatar Guillaume Melquiond

Use range types and coercions.

parent 74db69c8
......@@ -26,34 +26,31 @@ module SwapInt32
(* a simple model of 32-bit integers with addition, subtraction,
and possible overflows *)
type int32
type int32 = < range -0x8000_0000 0x7fff_ffff >
constant min_int32 : int = - 0x80000000
constant max_int32 : int = 0x7fffffff
constant width : int = max_int32 - min_int32 + 1
meta coercion function int32'int
function to_int (n: int32) : int
constant width : int = int32'maxInt - int32'minInt + 1
val (+) (a: int32) (b: int32) : int32
ensures { to_int result =
if to_int a + to_int b < min_int32 then to_int a + to_int b + width
else if to_int a + to_int b > max_int32 then to_int a + to_int b - width
else to_int a + to_int b }
ensures { result =
if a + b < int32'minInt then a + b + width
else if a + b > int32'maxInt then a + b - width
else a + b }
val (-) (a: int32) (b: int32) : int32
ensures { to_int result =
if to_int a - to_int b < min_int32 then to_int a - to_int b + width
else if to_int a - to_int b > max_int32 then to_int a - to_int b - width
else to_int a - to_int b }
ensures { result =
if a - b < int32'minInt then a - b + width
else if a - b > int32'maxInt then a - b - width
else a - b }
predicate in_bounds (n: int32) = min_int32 <= to_int n <= max_int32
predicate in_bounds (n: int32) = int32'minInt <= n <= int32'maxInt
(* purely applicative version first *)
let swap (a b: int32) : (int32, int32)
requires { in_bounds a /\ in_bounds b }
returns { x,y ->
to_int x = to_int b /\ to_int y = to_int a }
returns { x,y -> int32'int x = b /\ int32'int y = a }
=
let a = a + b in
let b = a - b in
......@@ -65,7 +62,7 @@ module SwapInt32
let swap_ref (a b: ref int32) : unit
requires { in_bounds !a /\ in_bounds !b }
writes { a, b }
ensures { to_int !a = old (to_int !b) /\ to_int !b = old (to_int !a) }
ensures { int32'int !a = old !b /\ int32'int !b = old !a }
=
a := !a + !b;
b := !a - !b;
......
......@@ -3,18 +3,18 @@
"http://why3.lri.fr/why3session.dtd">
<why3session shape_version="4">
<prover id="2" name="Alt-Ergo" version="1.30" timelimit="5" steplimit="0" memlimit="1000"/>
<file name="../swap.mlw" expanded="true">
<theory name="Swap" sum="31dd0e454abcc8d0c446f24eb3f7c4ad" expanded="true">
<goal name="VC swap" expl="VC for swap" expanded="true">
<file name="../swap.mlw" proved="true">
<theory name="Swap" proved="true" sum="31dd0e454abcc8d0c446f24eb3f7c4ad">
<goal name="VC swap" expl="VC for swap" proved="true">
<proof prover="2"><result status="valid" time="0.00" steps="4"/></proof>
</goal>
</theory>
<theory name="SwapInt32" sum="4cf775d81f506d0bd75554828de2319b" expanded="true">
<goal name="VC swap" expl="VC for swap" expanded="true">
<proof prover="2"><result status="valid" time="0.01" steps="50"/></proof>
<theory name="SwapInt32" proved="true" sum="4a80606ec224f7ae51bcf34942a25e80">
<goal name="VC swap" expl="VC for swap" proved="true">
<proof prover="2"><result status="valid" time="0.01" steps="48"/></proof>
</goal>
<goal name="VC swap_ref" expl="VC for swap_ref" expanded="true">
<proof prover="2"><result status="valid" time="0.01" steps="50"/></proof>
<goal name="VC swap_ref" expl="VC for swap_ref" proved="true">
<proof prover="2"><result status="valid" time="0.01" steps="46"/></proof>
</goal>
</theory>
</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