Why3 Standard Library index

Peano arithmetic

This module implements the idea described in this paper: How to avoid proving the absence of integer overflows

When extracted to OCaml, the following type `Peano.t` will be mapped to OCaml's type `int` (63-bit signed integers).

See also `mach.onetime`.

```module Peano

use int.Int

type t = abstract { v: int }
meta coercion function v

val to_int (x: t) : int
ensures { result = x.v }

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 }

val pred (x: t) : t
ensures { result.v = x.v - 1 }

val lt (x y: t) : bool
ensures { result <-> x.v < y.v }
val le (x y: t) : bool
ensures { result <-> x.v <= y.v }
val gt (x y: t) : bool
ensures { result <-> x.v > y.v }
val ge (x y: t) : bool
ensures { result <-> x.v >= y.v }
val eq (x y: t) : bool
ensures { result <-> x.v = y.v }
val ne (x y: t) : bool
ensures { result <-> x.v <> y.v }

val neg (x: t) : t
ensures { result.v = - x.v }
val abs (x: t) : t
ensures { result.v = if x.v >= 0 then x.v else - x.v }
val add (x y: t) (low high: t) : t
requires { low.v <= x.v + y.v <= high.v }
ensures  { result.v = x.v + y.v }
val sub (x y: t) (low high: t) : t
requires { low.v <= x.v - y.v <= high.v }
ensures  { result.v = x.v - y.v }
val mul (x y: t) (low high: t) : t
requires { low.v <= x.v * y.v <= high.v }
ensures  { result.v = x.v * y.v }

val of_int (x: int) (low high: t) : t
requires { low.v <= x <= high.v }
ensures  { result.v = x }

(* FIXME could replace low.v  by - max (abs low) (abs high)
high.v by   max (abs low) (abs high)
avoid the computation of the bounds
e.g. addition of two values of different signs
*)

end

module ComputerDivision

use int.Int
use int.ComputerDivision
use Peano

val div (x y: t) : t
requires { y.v <> 0 }
ensures  { result.v = div x.v y.v }

val mod (x y: t) : t
requires { y.v <> 0 }
ensures  { result.v = mod x.v y.v }

end

module MinMax

use int.Int
use int.MinMax
use Peano

val max (x y: t) : t
ensures { result.v = max x.v y.v }

val min (x y: t) : t
ensures { result.v = min x.v y.v }

end

module Int63
use int.Int
use mach.int.Int63
use Peano

val defensive_to_int63 (x:t) : int63
requires { Int63.in_bounds x.v }
ensures { result = x.v }

val partial to_int63 (x:t) : int63
ensures { result = x.v }

val of_int63 (x:int63) (low high: t) : t
requires { low.v <= x <= high.v }
ensures { result.v = x }

end
```

Generated by why3doc 1.5.0