Why3 Standard Library index



Arithmetic for programs


Integer Division

It is checked that divisor is not null.

module Int

  use export int.Int
  use export int.ComputerDivision

  let (/) (x: int) (y: int)
    requires { "expl:check division by zero" y <> 0 }
    ensures  { result = div x y }
  = div x y

  let (%) (x: int) (y: int)
    requires { "expl:check modulo by zero" y <> 0 }
    ensures  { result = mod x y }
  = mod x y

end

Machine integers

Bounded integers, typically n-bit signed and unsigned integers, go here. We first introduce a generic theory Bounded_int of bounded integers, with minimal and maximal values (resp. min and max). Then we instantiate it to get 32-bit and 64-bit signed and unsigned integers (Int32, UInt32, Int64, and UInt64) as well as 31-bit and 63-bit signed integers (Int31 and Int63) to be used in OCaml programs.

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 (+) (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 (-) (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 ( *) (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 (-_) (a:t) : t
    requires { "expl:integer overflow" in_bounds (- to_int a) }
    ensures  { to_int result = - to_int a }

  val eq (a:t) (b:t) : bool
    ensures { to_int a = to_int b -> result }
    ensures { result -> a = b }

  val ne (a:t) (b:t) : bool
    ensures { a <> b -> result }
    ensures { result -> to_int a <> to_int b }

  axiom extensionality: forall x y: t. to_int x = to_int y -> x = y

  val (<=) (a:t) (b:t) : bool
    ensures  { result <-> to_int a <= to_int b }

  val (<) (a:t) (b:t) : bool
    ensures  { result <-> to_int a < to_int b }

  val (>=) (a:t) (b:t) : bool
    ensures  { result <-> to_int a >= to_int b }

  val (>) (a:t) (b:t) : bool
    ensures  { result <-> to_int a > to_int b }

  use import int.ComputerDivision

  val (/) (a:t) (b:t) : t
    requires { "expl:division by zero" to_int b <> 0 }
    requires { "expl:integer overflow" in_bounds (div (to_int a) (to_int b)) }
    ensures  { to_int result = div (to_int a) (to_int b) }

  val (%) (a:t) (b:t) : t
    requires { "expl:division by zero" to_int b <> 0 }
    requires { "expl:integer overflow" in_bounds (mod (to_int a) (to_int b)) }
    ensures  { to_int result = mod (to_int a) (to_int b) }

end

module Unsigned

  use import int.Int

  constant min_unsigned : int = 0

  clone export Bounded_int with
    constant min = min_unsigned

  constant zero_unsigned : t

  axiom zero_unsigned_is_zero : to_int zero_unsigned = 0

  val add_with_carry (x y:t) (c:t) : (t,t)
    requires { 0 <= to_int c <= 1 }
    returns { (r,d) ->
      to_int r + (max+1) * to_int d =
      to_int x + to_int y + to_int c }

  val add3 (x y z:t) : (t,t)
    returns { (r,d) ->
      to_int r + (max+1) * to_int d =
      to_int x + to_int y + to_int z }

  val mul_double (x y:t) : (t,t)
    returns { (r,d) ->
      to_int r + (max+1) * to_int d =
      to_int x * to_int y }

end

module Int31

  use import int.Int

  type int31

  constant min_int31 : int = - 0x40000000
  constant max_int31 : int =   0x3fffffff

  clone export Bounded_int with
    type t = int31,
    constant min = min_int31,
    constant max = max_int31

(*  use bv.BV31

  val to_bv (x: int31) : BV31.t
    ensures { BV31.to_int result = to_int x }
  val of_bv (x: BV31.t) : int31
    ensures { to_int result = BV31.to_int x }
*)
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

  use bv.BV32

  val to_bv (x: int32) : BV32.t
    ensures { BV32.to_int result = to_int x }
  val of_bv (x: BV32.t) : int32
    ensures { to_int result = BV32.to_int x }

end

module UInt32

  type uint32

  constant max_uint32 : int = 0xffffffff

  clone export Unsigned with
    type t = uint32,
    constant max = max_uint32

(*  use bv.BV32

  val to_bv (x: uint32) : BV32.t
    ensures { BV32.to_uint result = to_int x }
  val of_bv (x: BV32.t) : uint32
    ensures { to_int result = BV32.to_uint x }
*)
end

module Int63

  use import int.Int

  type int63

  constant min_int63 : int = - 0x4000000000000000
  constant max_int63 : int =   0x3fffffffffffffff

  clone export Bounded_int with
    type t = int63,
    constant min = min_int63,
    constant max = max_int63

(*  use bv.BV63

  val to_bv (x: int63) : BV63.t
    ensures { BV63.to_int result = to_int x }
  val of_bv (x: BV63.t) : int63
    ensures { to_int result = BV63.to_int x }
*)
end

module Refint63

  use import Int63
  use export ref.Ref

  let incr (r: ref int63) : unit
    requires { "expl:integer overflow" to_int !r < max_int63 }
    ensures  { to_int !r = to_int (old !r) + 1 }
  = r := !r + of_int 1
  let decr (r: ref int63) : unit
    requires { "expl:integer overflow" min_int63 < to_int !r }
    ensures  { to_int !r = to_int (old !r) - 1 }
  = r := !r - of_int 1

  let (+=) (r: ref int63) (v: int63) : unit
    requires { "expl:integer overflow" in_bounds (to_int !r + to_int v) }
    ensures { to_int !r = to_int (old !r) + to_int v }
  = r := !r + v

  let (-=) (r: ref int63) (v: int63) : unit
    requires { "expl:integer overflow" in_bounds (to_int !r - to_int v) }
    ensures  { to_int !r = to_int (old !r) - to_int v }
  = r := !r - v

  let ( *= ) (r: ref int63) (v: int63) : unit
    requires { "expl:integer overflow" in_bounds (to_int !r * to_int v) }
    ensures { to_int !r = to_int (old !r) * to_int v }
  = r := !r * v

end

module MinMax63

  use import Int63

  let min (x y: int63) : int63
    ensures { result = if to_int x <= to_int y then x else y }
  = if x <= y then x else y

  let max (x y: int63) : int63
    ensures { result = if to_int x >= to_int y then x else y }
  = if x >= y then x else y

end

module Int64

  use import int.Int

  type int64

  constant min_int64 : int = - 0x8000000000000000
  constant max_int64 : int =   0x7fffffffffffffff

  clone export Bounded_int with
    type t = int64,
    constant min = min_int64,
    constant max = max_int64

(*  use bv.BV64

  val to_bv (x: int64) : BV64.t
    ensures { BV64.to_int result = to_int x }
  val of_bv (x: BV64.t) : int64
    ensures { to_int result = BV64.to_int x }
*)
end

module UInt64

  use import int.Int

  type uint64

  constant max_uint64 : int =  0xffffffffffffffff

  clone export Unsigned with
    type t = uint64,
    constant max = max_uint64

(*  use bv.BV64

  val to_bv (x: uint64) : BV64.t
    ensures { BV64.to_uint result = to_int x }
  val of_bv (x: BV64.t) : uint64
    ensures { to_int result = BV64.to_uint x }
*)
end

Generated by why3doc 0.88.0