Commit cfb5f904 authored by MARCHE Claude's avatar MARCHE Claude

Library: module for machine integers

parent eeaa18b0
module Bounded_int
use export int.Int
type t
constant min : int
constant max : int
function to_int (n:t) : int
predicate in_bounds (n:int) = min <= n <= max
axiom to_int_in_bounds: forall n:t. in_bounds (to_int n)
val of_int (n:int) : t
requires { "expl:integer overflow" in_bounds n }
ensures { to_int result = n }
val add (a:t) (b:t) : t
requires { "expl:integer overflow" in_bounds (to_int a + to_int b) }
ensures { to_int result = to_int a + to_int b }
val sub (a:t) (b:t) : t
requires { "expl:integer overflow" in_bounds (to_int a - to_int b) }
ensures { to_int result = to_int a - to_int b }
val mul (a:t) (b:t) : t
requires { "expl:integer overflow" in_bounds (to_int a * to_int b) }
ensures { to_int result = to_int a * to_int b }
use import int.ComputerDivision
val div (a:t) (b:t) : t
requires { "expl:division by zero" to_int b <> 0 }
requires { "expl:integer overflow"
in_bounds (ComputerDivision.div (to_int a) (to_int b)) }
ensures {
to_int result = ComputerDivision.div (to_int a) (to_int b) }
end
module Int32
use import int.Int
type int32
constant min_int32 : int = - 0x80000000
constant max_int32 : int = 0x7fffffff
clone export Bounded_int with
type t = int32,
constant min = min_int32,
constant max = max_int32
end
module UInt32
type uint32
constant min_uint32 : int = 0x00000000
constant max_uint32 : int = 0xffffffff
clone export Bounded_int with
type t = uint32,
constant min = min_uint32,
constant max = max_uint32
end
module TestInt32
use import mach_int.Int32
let mean_wrong (a:int32) (b:int32) : int32 =
div (add a b) (of_int 2)
let mean_ok (a:int32) (b:int32) : int32
requires { 0 <= to_int a <= to_int b }
=
add a (div (sub b a) (of_int 2))
end
module TestUInt32
use import mach_int.UInt32
let mean_wrong (a:uint32) (b:uint32) : uint32 =
div (add a b) (of_int 2)
let mean_ok (a:uint32) (b:uint32) : uint32
requires { to_int a <= to_int b }
=
add a (div (sub b a) (of_int 2))
end
\ No newline at end of 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