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.87.3