Why3 Standard Library

https://why3.org/stdlib
Admin
Why3 Standard Library provides a comprehensive collection of verified theories, data structures, and...
Tokens:211,295
Snippets:915
Trust Score:7.5
Update:2 weeks ago
Show doc for...
Tokens:
Raw
### Start GenericFloat module with imports

Source: https://why3.org/stdlib/ieee_float.html

Starts the GenericFloat module by importing integer, bit-vector, and real theories, and exports the RoundingMode module. This is the beginning of the generic floating-point theory that implements IEEE-754 operations.

```why3
module GenericFloat

  use int.Int
  use bv.Pow2int
  use real.Abs as Abs
  use real.FromInt as FromInt
  use real.Truncate as Truncate
  use real.RealInfix
  use export RoundingMode

```

--------------------------------

### RegExpr module start

Source: https://why3.org/stdlib/string.html

Starts the RegExpr module, importing String and declaring the type for regular expressions.

```why3
module RegExpr

  use String as S

  type re


```

--------------------------------

### UFloat constants and power-of-two exactness; USingle module start

Source: https://why3.org/stdlib/ufloat.html

Defines constants u0 through u65536 with their real values, a predicate is_positive_power_of_2, and an axiom that division by a positive power of two is exact. Ends the UFloat module and starts the USingle module with a use of real.RealInfix.

```why3
  (* Some constants *)
  constant u0:t
  axiom to_real_u0 : to_real u0 = 0.0
  constant u1:t
  axiom to_real_u1 : to_real u1 = 1.0
  constant u2:t
  axiom to_real_u2 : to_real u2 = 2.0
  constant u4:t
  axiom to_real_u4 : to_real u4 = 4.0
  constant u8:t
  axiom to_real_u8 : to_real u8 = 8.0
  constant u16:t
  axiom to_real_u16 : to_real u16 = 16.0
  constant u32:t
  axiom to_real_u32 : to_real u32 = 32.0
  constant u64:t
  axiom to_real_u64 : to_real u64 = 64.0
  constant u128:t
  axiom to_real_u128 : to_real u128 = 128.0
  constant u256:t
  axiom to_real_u256 : to_real u256 = 256.0
  constant u512:t
  axiom to_real_u512 : to_real u512 = 512.0
  constant u1024:t
  axiom to_real_u1024 : to_real u1024 = 1024.0
  constant u2048:t
  axiom to_real_u2048 : to_real u2048 = 2048.0
  constant u4096:t
  axiom to_real_u4096 : to_real u4096 = 4096.0
  constant u8192:t
  axiom to_real_u8192 : to_real u8192 = 8192.0
  constant u16384:t
  axiom to_real_u16384 : to_real u16384 = 16384.0
  constant u32768:t
  axiom to_real_u32768 : to_real u32768 = 32768.0
  constant u65536:t
  axiom to_real_u65536 : to_real u65536 = 65536.0

  predicate is_positive_power_of_2 (x:t) =
    x = u1 \/ x = u2 || x = u4 || x = u8 || x = u16 || x = u32 || x = u64
    || x = u128 \/ x = u256 || x = u4096 || x = u8192 || x = u16384 || x = u32768
    || x = u65536

  axiom div_by_positive_power_of_2_is_exact :
    forall x y. is_positive_power_of_2 y -> is_exact udiv x y
end

module USingle
  use real.RealInfix

```
```

--------------------------------

### Start UDouble module with udouble type

Source: https://why3.org/stdlib/ufloat.html

Starts the UDouble module, importing real.RealInfix and declaring the udouble type. This is the beginning of the double-precision unbounded float definition.

```why3
module UDouble
  use real.RealInfix
  type udouble


```

--------------------------------

### length and get functions with axioms

Source: https://why3.org/stdlib/seq.html

Declares the length function with a nonnegative axiom and the get function for element access. The get function has a FIXME comment about a missing requires clause.

```why3
  val function length (seq 'a) : int

  axiom length_nonnegative:
    forall s: seq 'a. 0 <= length s
  meta "remove_unused:dependency" axiom length_nonnegative, function length

  val function get (seq 'a) int : 'a
    (* FIXME requires { 0 <= i < length s } *)

```

--------------------------------

### create

Source: https://why3.org/stdlib/hashtbl.html

Creates a new hash table with an initial size hint. The resulting table maps every key to an empty list.

```APIDOC
## create

### Description
Creates a new hash table with an initial size hint. The resulting table maps every key to an empty list.

### Method
val create (_n:int) : t 'a

### Parameters
- **_n** (int) - Required - Initial size hint for the hash table.

### Returns
- **t 'a** - A new hash table where every key maps to an empty list.

### Postconditions
- For all keys k, result[k] = Nil.
```

--------------------------------

### create

Source: https://why3.org/stdlib/queue.html

Creates a new empty queue.

```APIDOC
## create

### Description
Creates a new empty queue.

### Method
val create () : t 'a

### Parameters
None.

### Returns
- **result** (t 'a) - A new empty queue.

### Postconditions
- result = empty
```

--------------------------------

### fxp_init

Source: https://why3.org/stdlib/mach.fxp.html

Initializes a fixed-point number from an unsigned 64-bit integer and a binary point position.

```APIDOC
## fxp_init

### Description
Initialize a fixed-point number with an integer `x` by setting the position `k` of its binary point.

### Signature
`let fxp_init [@extraction:inline] (x: uint64) (ghost k: int): fxp`

### Parameters
- **x** (uint64) - Required - The integer value to initialize.
- **k** (int, ghost) - Required - The binary point position.

### Returns
- **fxp** - The fixed-point number with `ival = x`, `rval = real(x) * 2^k`, and `iexp = k`.
```

--------------------------------

### Initialize a fixed-point number with fxp_init

Source: https://why3.org/stdlib/mach.fxp.html

Initializes a fixed-point number from an integer `x` and a binary-point position `k`. The integer value is stored directly, and the real value is computed as `x * 2^k`.

```why3
let fxp_init [@extraction:inline] (x: uint64) (ghost k: int): fxp
= { ival = x; rval = FromInt.from_int (to_int x) *. pow2 k; iexp = k }


```

--------------------------------

### Blit array range with blit

Source: https://why3.org/stdlib/array.html

Copies len elements from a1 starting at ofs1 into a2 starting at ofs2. Requires both source and destination ranges to be within bounds, and ensures that only the destination range is modified.

```why3
  let blit (a1: array 'a) (ofs1: int)
                 (a2: array 'a) (ofs2: int) (len: int) : unit writes {a2}
    requires { 0 <= ofs1 /\ 0 <= len /\ ofs1 + len <= length a1 }
    requires { 0 <= ofs2 /\             ofs2 + len <= length a2 }
    ensures  { forall i:int.
      (0 <= i < ofs2 \/ ofs2 + len <= i < length a2) -> a2[i] = old a2[i] }
    ensures  { forall i:int.
      ofs2 <= i < ofs2 + len -> a2[i] = a1[ofs1 + i - ofs2] }
  =
    for i = 0 to len - 1 do
      invariant { forall k. not (0 <= k < i) -> a2[ofs2 + k] = old a2[ofs2 + k] }
      invariant { forall k. 0 <= k < i -> a2[ofs2 + k] = a1[ofs1 + k] }
      a2[ofs2 + i] <- a1[ofs1 + i];
    done

```

--------------------------------

### init

Source: https://why3.org/stdlib/mach.array.html

Initializes an array using a function to compute each element.

```APIDOC
## [Array63] init (n: int63) (f: int63 -> 'a) : array 'a

### Description
Creates a new array of length `n` where each element at index `i` is computed by function `f`.

### Method
let

### Endpoint
init (n: int63) (f: int63 -> 'a) : array 'a

### Parameters
#### Path Parameters
- **n** (int63) - Required - The length of the new array. Must be non-negative.
- **f** (int63 -> 'a) - Required - A function that maps an index to an element value.

### Preconditions
- n >= 0

### Postconditions
- forall i: int63. 0 <= i < n -> result[i] = f i
- length result = n

### Response
#### Success Response
- **result** (array 'a) - The newly created array.

```

--------------------------------

### get

Source: https://why3.org/stdlib/matrix.html

Returns the element at the given row and column of the matrix.

```APIDOC
## get

### Description
Returns the element at the given row and column of the matrix.

### Signature
`val get (a: matrix 'a) (r c: int) : 'a`

### Parameters
- **a** (matrix 'a) - The matrix to access.
- **r** (int) - Row index.
- **c** (int) - Column index.

### Preconditions
- `valid_index a r c` (index in matrix bounds)

### Postconditions
- `result = a.elts r c`

### Exceptions
None.

```

--------------------------------

### Why3 Map module: get, set, [], [<-], Const, MapExt

Source: https://why3.org/stdlib/map.html

Defines the core map type as a total function, with get, set, and the [] and [<-] operators. The second block closes the Map module and adds Const (constant map) and MapExt (extensional equality with a provable lemma).

```why3
module Map

  type map 'a 'b = 'a -> 'b

  let function get (f: map 'a 'b) (x: 'a) : 'b = f x

  let ghost function set (f: map 'a 'b) (x: 'a) (v: 'b) : map 'a 'b =
    fun y -> if pure {y = x} then v else f y

  let function ([]) (f: map 'a 'b) (x: 'a) : 'b = f x
  let ghost function ([<-]) (f: map 'a 'b) (x: 'a) (v: 'b) : map 'a 'b = set f x v


```

```why3
end

module Const

  use Map

  let function const (v: 'b) : map 'a 'b = fun _ -> v

end

module MapExt

  predicate (==) (m1 m2: 'a -> 'b) = forall x: 'a. m1 x = m2 x

  lemma extensionality:
    forall m1 m2: 'a -> 'b. m1 == m2 -> m1 = m2
  (* This lemma is actually provable in Why3, because of how
     eliminate_epsilon handles equality to a lambda-term. *)

  meta extensionality predicate (==)

end



```

--------------------------------

### State63.init

Source: https://why3.org/stdlib/mach.int.html

Initializes an existing state with a new seed.

```APIDOC
## State63.init

### Description
Initializes an existing state with a new seed.

### Method
val

### Signature
val init (s: state) (seed: int63) : unit writes {s}

### Parameters
- **s** (state) - Required - The state to initialize.
- **seed** (int63) - Required - The seed value.

### Effects
Writes to state `s`.

```

--------------------------------

### defensive_get

Source: https://why3.org/stdlib/mach.array.html

Defensive get operation that raises an exception on out-of-bounds access.

```APIDOC
## [Array63] defensive_get (a: array 'a) (i: int63)

### Description
Returns the element at index `i` of array `a`, raising `OutOfBounds` if the index is out of bounds.

### Method
let

### Endpoint
defensive_get (a: array 'a) (i: int63)

### Parameters
#### Path Parameters
- **a** (array 'a) - Required - The array to access.
- **i** (int63) - Required - The index of the element to retrieve.

### Postconditions
- 0 <= i < a.length
- result = a[i]

### Exceptions
- **OutOfBounds** - Raised when i < 0 or i >= a.length.

### Response
#### Success Response
- **result** ('a) - The element at index `i`.

```

--------------------------------

### make

Source: https://why3.org/stdlib/mach.array.html

Creates a new array with a given length and initial value.

```APIDOC
## [Array63] make (n: int63) (v: 'a) : array 'a

### Description
Creates a new array of length `n` with all elements initialized to `v`.

### Method
val

### Endpoint
make (n: int63) (v: 'a) : array 'a

### Parameters
#### Path Parameters
- **n** (int63) - Required - The length of the new array. Must be non-negative.
- **v** ('a) - Required - The initial value for all elements.

### Preconditions
- n >= 0

### Postconditions
- forall i:int. 0 <= i < n -> result[i] = v
- result.length = n

### Response
#### Success Response
- **result** (array 'a) - The newly created array.

```

--------------------------------

### Get queue length

Source: https://why3.org/stdlib/pqueue.html

Returns the number of elements in the queue, equal to the cardinality of the underlying set.

```why3
  val length (q: t) : int
    ensures { result = cardinal q }

```

--------------------------------

### Clone BVCheck_Gen for 8/16/32/64-bit bit-vector sizes

Source: https://why3.org/stdlib/mach.bv.html

These four Why3 modules instantiate the generic BVCheck_Gen for 8-, 16-, 32-, and 64-bit bit-vector sizes. Each module exports the corresponding bv.BVn theory, defines the size-specific constants (minus_one, min_sint, max_sint, max_uint), imports the matching BVConverter_n_128, and clones BVCheck_Gen with the full set of operations and predicates. The 64-bit module is shown without its closing 'end' in the source.

```why3
module BVCheck8
  use export bv.BV8

  constant minus_one : t = 0xFF
  constant min_sint : t = 0x80
  constant max_sint : t = 0x7F
  constant max_uint : t = 0xFF

  use bv.BVConverter_8_128

  clone export BVCheck_Gen with
    type t = t,
    constant size = size,
    constant size_bv = size_bv,
    function two_power_size = two_power_size,
    function two_power_size_minus_one = two_power_size_minus_one,
    function zeros = zeros,
    function minus_one = minus_one,
    function min_sint = min_sint,
    function max_sint = max_sint,
    function max_uint = max_uint,
    function to_uint = t'int,
    function to_int = to_int,
    function of_int = of_int,
    function add = add,
    function sub = sub,
    function mul = mul,
    function udiv = udiv,
    function urem = urem,
    function sdiv = sdiv,
    function srem = srem,
    function lsl = lsl,
    function lsl_bv = lsl_bv,
    function lsr = lsr,
    function lsr_bv = lsr_bv,
    function asr = asr,
    function asr_bv = asr_bv,
    predicate ule = ule,
    predicate ult = ult,
    predicate uge = uge,
    predicate ugt = ugt,
    predicate sle = sle,
    predicate slt = slt,
    predicate sge = sge,
    predicate sgt = sgt,
    function sto_bv128 = stoBig,
    function uto_bv128 = toBig
end
```

```why3
module BVCheck16
  use export bv.BV16

  constant minus_one : t = 0xFFFF
  constant min_sint : t = 0x8000
  constant max_sint : t = 0x7FFF
  constant max_uint : t = 0xFFFF

  use bv.BVConverter_16_128

  clone export BVCheck_Gen with
    type t = t,
    constant size = size,
    constant size_bv = size_bv,
    function two_power_size = two_power_size,
    function two_power_size_minus_one = two_power_size_minus_one,
    function zeros = zeros,
    function minus_one = minus_one,
    function min_sint = min_sint,
    function max_sint = max_sint,
    function max_uint = max_uint,
    function to_uint = t'int,
    function to_int = to_int,
    function of_int = of_int,
    function add = add,
    function sub = sub,
    function mul = mul,
    function udiv = udiv,
    function urem = urem,
    function sdiv = sdiv,
    function srem = srem,
    function lsl = lsl,
    function lsl_bv = lsl_bv,
    function lsr = lsr,
    function lsr_bv = lsr_bv,
    function asr = asr,
    function asr_bv = asr_bv,
    predicate ule = ule,
    predicate ult = ult,
    predicate uge = uge,
    predicate ugt = ugt,
    predicate sle = sle,
    predicate slt = slt,
    predicate sge = sge,
    predicate sgt = sgt,
    function sto_bv128 = stoBig,
    function uto_bv128 = toBig
end
```

```why3
module BVCheck32
  use export bv.BV32

  constant minus_one : t = 0xFFFF_FFFF
  constant min_sint : t = 0x8000_0000
  constant max_sint : t = 0x7FFF_FFFF
  constant max_uint : t = 0xFFFF_FFFF

  use bv.BVConverter_32_128

  clone export BVCheck_Gen with
    type t = t,
    constant size = size,
    constant size_bv = size_bv,
    function two_power_size = two_power_size,
    function two_power_size_minus_one = two_power_size_minus_one,
    function zeros = zeros,
    function minus_one = minus_one,
    function min_sint = min_sint,
    function max_sint = max_sint,
    function max_uint = max_uint,
    function to_uint = t'int,
    function to_int = to_int,
    function of_int = of_int,
    function add = add,
    function sub = sub,
    function mul = mul,
    function udiv = udiv,
    function urem = urem,
    function sdiv = sdiv,
    function srem = srem,
    function lsl = lsl,
    function lsl_bv = lsl_bv,
    function lsr = lsr,
    function lsr_bv = lsr_bv,
    function asr = asr,
    function asr_bv = asr_bv,
    predicate ule = ule,
    predicate ult = ult,
    predicate uge = uge,
    predicate ugt = ugt,
    predicate sle = sle,
    predicate slt = slt,
    predicate sge = sge,
    predicate sgt = sgt,
    function sto_bv128 = stoBig,
    function uto_bv128 = toBig
end
```

```why3
module BVCheck64
  use export bv.BV64

  constant minus_one : t = 0xFFFF_FFFF_FFFF_FFFF
  constant min_sint : t = 0x8000_0000_0000_0000
  constant max_sint : t = 0x7FFF_FFFF_FFFF_FFFF
  constant max_uint : t = 0xFFFF_FFFF_FFFF_FFFF

  use bv.BVConverter_64_128

  clone export BVCheck_Gen with
    type t = t,
    constant size = size,
    constant size_bv = size_bv,
    function two_power_size = two_power_size,
    function two_power_size_minus_one = two_power_size_minus_one,
    function zeros = zeros,
    function minus_one = minus_one,
    function min_sint = min_sint,
    function max_sint = max_sint,
    function max_uint = max_uint,
    function to_uint = t'int,
    function to_int = to_int,
    function of_int = of_int,
    function add = add,
    function sub = sub,
    function mul = mul,
    function udiv = udiv,
    function urem = urem,
    function sdiv = sdiv,
    function srem = srem,
    function lsl = lsl,
    function lsl_bv = lsl_bv,
    function lsr = lsr,
    function lsr_bv = lsr_bv,
    function asr = asr,
    function asr_bv = asr_bv,
    predicate ule = ule,
    predicate ult = ult,
    predicate uge = uge,
    predicate ugt = ugt,
    predicate sle = sle,
    predicate slt = slt,
    predicate sge = sge,
    predicate sgt = sgt,
    function sto_bv128 = stoBig,
    function uto_bv128 = toBig
end
```

--------------------------------

### PowerReal module: real exponentiation

Source: https://why3.org/stdlib/real.html

Defines pow for real base and exponent using exp and log. Includes lemmas for positivity, addition, multiplication, and special values. Requires x > 0.0 for most properties.

```why3
module PowerReal

  use Real
  use ExpLog

  function pow real real : real

  axiom Pow_def:
    forall x y:real. x > 0.0 -> pow x y = exp (y * log x)

  lemma Pow_pos:
    forall x y. x > 0.0 -> pow x y > 0.0

  lemma Pow_plus :
    forall x y z. z > 0.0 -> pow z (x + y) = pow z x * pow z y

  lemma Pow_mult :
    forall x y z. x > 0.0 -> pow (pow x y) z = pow x (y * z)

  lemma Pow_x_zero:
    forall x:real. x > 0.0 -> pow x 0.0 = 1.0

  lemma Pow_x_one:
    forall x:real. x > 0.0 -> pow x 1.0 = x

  lemma Pow_one_y:
    forall y:real. pow 1.0 y = 1.0

  use Square

  lemma Pow_x_two:
    forall x:real. x > 0.0 -> pow x 2.0 = sqr x

  lemma Pow_half:
    forall x:real. x > 0.0 -> pow x 0.5 = sqrt x

  use FromInt
  use int.Power

  lemma pow_from_int: forall x y: int. Int.(<) 0 x -> Int.(<=) 0 y ->
                      pow (from_int x) (from_int y) = from_int (power x y)

end

```

--------------------------------

### Define get_ofs for pointer dereference with offset

Source: https://why3.org/stdlib/mach.c.html

Defines pointer dereference with an offset by combining incr and get. Requires the offset to be within bounds.

```why3
  let get_ofs (p:ptr 'a) (ofs:int32) : 'a
    requires { p.min <= p.offset + ofs < p.max }
    ensures { result = (pelts p)[p.offset + ofs] }
  = get (incr p ofs)

```

--------------------------------

### Declare pointer dereference with get

Source: https://why3.org/stdlib/mach.c.html

Declares pointer dereference that returns the element at the current offset. Requires the offset to be within the valid range.

```why3
  val get (p:ptr 'a) : 'a
    requires { p.min <= p.offset < p.max }
    ensures { result = (pelts p)[p.offset] }

```

--------------------------------

### Induction principles on integers in Why3

Source: https://why3.org/stdlib/int.html

Presents three induction principles: SimpleInduction with base and step axioms, Induction with a strong induction lemma and a bound variant, and HOInduction with a higher-order lemma that uses a recursive lemma to prove the property.

```Why3
module SimpleInduction

  use Int

  predicate p int

  axiom base: p 0

  axiom induction_step: forall n:int. 0 <= n -> p n -> p (n+1)

  lemma SimpleInduction : forall n:int. 0 <= n -> p n

end

```

```Why3
module Induction

  use Int

  predicate p int

  lemma Induction :
    (forall n:int. 0 <= n -> (forall k:int. 0 <= k < n -> p k) -> p n) ->
    forall n:int. 0 <= n -> p n

  constant bound : int

  lemma Induction_bound :
    (forall n:int. bound <= n ->
      (forall k:int. bound <= k < n -> p k) -> p n) ->
    forall n:int. bound <= n -> p n

end

```

```Why3
module HOInduction

  use Int

  let lemma induction (p: int -> bool)
    requires { p 0 }
    requires { forall n. 0 <= n >= 0 -> p n -> p (n+1) }
    ensures  { forall n. 0 <= n -> p n }
  = let rec lemma f (n: int) requires { n >= 0 } ensures  { p n } variant {n}
    = if n > 0 then f (n-1) in f 0

end

```

--------------------------------

### Define fold_right function for sequences

Source: https://why3.org/stdlib/seq.html

Defines fold_right, which applies a binary function from right to left over a sequence, starting with an accumulator. Uses a variant on the sequence length for termination.

```why3
module FoldRight

  use Seq
  use int.Int

  let rec function fold_right (f: 'b -> 'a -> 'a) (s: seq 'b) (acc: 'a) : 'a
    variant { length s }
  = if length s = 0 then acc
    else let acc = f s[length s - 1] acc in fold_right f s[.. length s - 1] acc

```

--------------------------------

### State63.self_init

Source: https://why3.org/stdlib/mach.int.html

Initializes a state with a seed derived from system entropy.

```APIDOC
## State63.self_init

### Description
Initializes a state with a seed derived from system entropy.

### Method
val

### Signature
val self_init (s: state) : unit writes {s}

### Parameters
- **s** (state) - Required - The state to initialize.

### Effects
Writes to state `s`.

```

--------------------------------

### Define fold_left function for sequences

Source: https://why3.org/stdlib/seq.html

Defines fold_left, which applies a binary function from left to right over a sequence, starting with an accumulator. Uses a variant on the sequence length for termination.

```why3
module FoldLeft

  use Seq
  use int.Int

  let rec function fold_left (f: 'a -> 'b -> 'a) (acc: 'a) (s: seq 'b) : 'a
    variant { length s }
  = if length s = 0 then acc else fold_left f (f acc s[0]) s[1 ..]

```

--------------------------------

### Parity module: even/odd predicates and lemmas

Source: https://why3.org/stdlib/number.html

Defines even and odd predicates for integers and proves basic parity lemmas, including that evenness is equivalent to n mod 2 = 0 using int.ComputerDivision.

```why3
module Parity

  use int.Int

  predicate even (n: int) = exists k: int. n = 2 * k
  predicate odd (n: int) = exists k: int. n = 2 * k + 1

  lemma even_or_odd: forall n: int. even n \/ odd n

  lemma even_not_odd: forall n: int. even n -> not (odd n)
  lemma odd_not_even: forall n: int. odd n -> not (even n)

  lemma even_odd: forall n: int. even n -> odd (n + 1)
  lemma odd_even: forall n: int. odd n -> even (n + 1)

  lemma even_even: forall n: int. even n -> even (n + 2)
  lemma odd_odd: forall n: int. odd n -> odd (n + 2)

  lemma even_2k: forall k: int. even (2 * k)
  lemma odd_2k1: forall k: int. odd (2 * k + 1)

  use int.ComputerDivision

  lemma even_mod2 :
    forall n:int. even n <-> mod n 2 = 0

end

```

--------------------------------

### Indexing operator ([]) and extensional equality (==)

Source: https://why3.org/stdlib/seq.html

Defines the indexing operator ([]) as an alias for get, and declares the extensional equality predicate (==) with a postcondition ensuring equal lengths and element-wise equality.

```why3
  let function ([]) (s: seq 'a) (i: int) : 'a =
    get s i

  val predicate (==) (s1 s2: seq 'a)
    ensures { result <-> length s1 = length s2 &&
              forall i: int. 0 <= i < length s1 -> s1[i] = s2[i] }
    ensures { result -> s1 = s2 }

```

--------------------------------

### Push element into queue

Source: https://why3.org/stdlib/pqueue.html

Pushes an element `x` into the queue `q`. The postcondition states that the queue becomes the old queue with `x` added.

```why3
  val push (x: elt) (q: t) : unit
    writes  { q }
    ensures { q = add x (old q) }

```

--------------------------------

### Extract sub-array with sub

Source: https://why3.org/stdlib/array.html

Extracts a sub-array of length len starting at offset ofs. Requires that ofs, len, and ofs+len are within bounds, and returns an array of length len with elements copied from the source.

```why3
  let sub (a: array 'a) (ofs: int) (len: int) : array 'a
    requires { 0 <= ofs /\ 0 <= len /\ ofs + len <= length a }
    ensures  { length result = len }
    ensures  { forall i:int. 0 <= i < len -> result[i] = a[ofs + i] }
  =
    if length a = 0 then begin
     assert { len = 0 };
     empty ()
    end else begin
      let b = make len a[0] in
      for i = 0 to len-1 do
        invariant { forall k. 0 <= k < i -> b[k] = a[ofs+k] }
        b[i] <- a[ofs+i];
      done;
      b
    end

```

--------------------------------

### Why3 model of java.util.Map

Source: https://why3.org/stdlib/mach.java.util.html

Why3 module modeling a subset of java.util.Map. Requires the mach.java.lang.Integer module to translate sizes. Preconditions: get requires the key to be in the map and put preserves the size when the key is already present.

```WHY3
module Map
   use int.Int
   use fmap.Fmap as FM
   use mach.java.lang.Integer

   type map [@java:scalar_objects] 'k 'el = private {
     ghost mutable content : FM.fmap 'k 'el
   }

   val function size (m : map 'k 'el) : integer
     ensures { result = Integer.enforced_integer (FM.size m.content) }

   val function containsKey (m : map 'k 'el) (key : 'k) : bool
     ensures { result = FM.mem key m.content }

   val empty () : map 'k 'el
     ensures { result.content = FM.empty }

   val function get  (m : map 'k 'el) (key : 'k) : 'el
     requires { FM.mem key m.content }
     ensures { result = FM.find key m.content }

   val put (m : map 'k 'el) (key : 'k) (value : 'el) : unit
     writes { m.content }
     ensures { FM.mem key (old m.content)
               -> FM.size m.content = FM.size (old m.content)  }
     ensures { FM.mem key m.content }
     ensures { FM.find key m.content = value }
     ensures { m.content = FM.add key value (old m.content) }

end
```

--------------------------------

### ToList module: convert seq to list with length and nth lemmas

Source: https://why3.org/stdlib/seq.html

Declares a conversion function from sequences to lists and proves its length and nth properties. Includes axioms for empty and cons cases and a recursive lemma showing to_list commutes with cons.

```Why3
module ToList
  use int.Int
  use Seq
  use list.List

  val function to_list (a: seq 'a) : list 'a

  axiom to_list_empty:
    to_list (empty: seq 'a) = (Nil: list 'a)

  axiom to_list_cons:
    forall s: seq 'a. 0 < length s ->
    to_list s = Cons s[0] (to_list s[1 ..])

  use list.Length as ListLength

  lemma to_list_length:
    forall s: seq 'a. ListLength.length (to_list s) = length s

  use list.Nth as ListNth
  use option.Option

  lemma to_list_nth:
    forall s: seq 'a, i: int. 0 <= i < length s ->
    ListNth.nth i (to_list s) = Some s[i]

  let rec lemma to_list_def_cons (s: seq 'a) (x: 'a)
    variant { length s }
    ensures { to_list (cons x s) = Cons x (to_list s) }
  = assert { (cons x s)[1 ..] == s }

end
```

--------------------------------

### Optional module specification

Source: https://why3.org/stdlib/mach.java.util.html

Defines the Optional type with a ghost option value and operations for creating, checking, and retrieving optional values. The get function raises NoSuchElementException when the optional is empty, while get_safe requires a present value.

```why3
module Optional
  use NoSuchElementException
  use option.Option

  type optional [@java:scalar_objects] 'elt = { ghost v : option 'elt }

  val function empty () : optional 'elt
    ensures { result = { v = None } }

  val function build (e : 'elt) : optional 'elt
    ensures { result = { v = Some e } }

  val function is_present (o : optional 'elt) : bool
    ensures { result = not is_none o.v }

  val function is_empty (o : optional 'elt) : bool
    ensures { result = is_none o.v }

  val get (o : optional 'elt) : 'elt
    ensures { o.v = Some result }
    raises { NoSuchElementException.E -> not is_present o }

  val function get_safe (o : optional 'elt) : 'elt
    requires { is_present o }
    ensures { Some result = o.v }

end
```

--------------------------------

### Instantiate MinMax for reals in Why3

Source: https://why3.org/stdlib/real.html

Instantiates the generic MinMax module from the relations library for real numbers, using the standard <= ordering. The clone directive exports the min and max functions and their associated properties.

```why3
module MinMax

  use Real
  clone export relations.MinMax with type t = real, predicate le = (<=), goal .

end

```

--------------------------------

### Defensive get and set with OutOfBounds exception

Source: https://why3.org/stdlib/array.html

Provides unsafe get/set operations with no precondition, raising the OutOfBounds exception when the index is out of bounds. The ensures clauses specify the postconditions for successful access and the raises clauses specify the exception behavior.

```why3
  exception OutOfBounds

  let defensive_get (a: array 'a) (i: int)
    ensures { 0 <= i < length a /\ result = a[i] }
    raises  { OutOfBounds -> i < 0 \/ i >= length a }
  = if i < 0 || i >= length a then raise OutOfBounds;
    a[i]

  let defensive_set (a: array 'a) (i: int) (v: 'a)
    ensures { 0 <= i < length a }
    ensures { a = (old a)[i <- v] }
    raises  { OutOfBounds -> (i < 0 \/ i >= length a) /\ a = old a }
  = if i < 0 || i >= length a then raise OutOfBounds;
    a[i] <- v

```

--------------------------------

### Fmap_ext module with domain and apply

Source: https://why3.org/stdlib/fmap.html

Defines the Fmap_ext module that exports Fmap and provides a domain abbreviation and an apply function for map application. Includes an axiom for apply_result and a dependency meta.

```why3
module Fmap_ext

use map.Map
use set.Fset as S
use export Fmap

function dom (m: fmap 'k 'v) : S.fset 'k = m.domain

```

```why3
function apply (m: fmap 'k 'v) (x: 'k): 'v

```

```why3
axiom apply_result:
  forall m: fmap 'k 'v, x.  mem x m -> mapsto x (apply m x) m
meta "remove_unused:dependency" axiom apply_result, function apply

```

--------------------------------

### Matrix module with safe get and set operations

Source: https://why3.org/stdlib/matrix.html

Defines the Matrix module with a private ghost matrix type, a valid_index predicate, and safe get/update/set operations that require valid indices. The type invariant ensures non-negative rows and columns.

```why3
module Matrix

  use int.Int
  use map.Map

  type matrix 'a = private {
    ghost mutable elts: int -> int -> 'a;
                  rows: int;
               columns: int
  } invariant { 0 <= rows /\ 0 <= columns }

  predicate valid_index (a: matrix 'a) (r c: int) =
    0 <= r < a.rows /\ 0 <= c < a.columns

  function get (a: matrix 'a) (r c: int) : 'a =
    a.elts r c

  val get (a: matrix 'a) (r c: int) : 'a
    requires { [@expl:index in matrix bounds] valid_index a r c }
    ensures  { result = a.elts r c }

  val ghost function update (a: matrix 'a) (r c: int) (v: 'a) : matrix 'a
    ensures  { result.rows = a.rows }
    ensures  { result.columns = a.columns }
    ensures  { result.elts = a.elts[r <- (a.elts r)[c <- v]] }

  val set (a: matrix 'a) (r c: int) (v: 'a) : unit
    requires { [@expl:index in matrix bounds] valid_index a r c }
    writes   { a }
    ensures  { a.elts = (old a.elts)[r <- (old a.elts r)[c <- v]] }


```

--------------------------------

### gen_zero lemmas and GenFloatSpecFull module

Source: https://why3.org/stdlib/floating_point.html

Provides lemmas about gen_zero values and ends the GenFloatFull module. Then declares the GenFloatSpecFull module that clones GenFloatFull with an axiom and imports real.Real, real.Square, Rounding, and SpecialValues.

```why3
  lemma is_gen_zero_comp1 : forall x y:t.
    is_gen_zero x /\ value x = value y /\ is_finite y -> is_gen_zero y

  lemma is_gen_zero_comp2 : forall x y:t.
    is_finite x /\ not (is_gen_zero x) /\ value x = value y
    -> not (is_gen_zero y)

end

module GenFloatSpecFull

  use real.Real
  use real.Square
  use Rounding
  use SpecialValues
  clone export GenFloatFull with axiom .



```

--------------------------------

### Navigate a binary tree using Huet's zipper

Source: https://why3.org/stdlib/bintree.html

Defines a zipper type for navigating a binary tree, with functions to zip, start, go up, go to top, and move down left or right. Includes comments indicating that moving up or down on an empty tree does nothing.

```why3
module Zipper

  use Tree

  type zipper 'a =
    | Top
    | Left  (zipper 'a) 'a (tree 'a)
    | Right (tree 'a)   'a (zipper 'a)

  let rec function zip (t: tree 'a) (z: zipper 'a) : tree 'a =
    match z with
    | Top -> t
    | Left z x r -> zip (Node t x r) z
    | Right l x z -> zip (Node l x t) z
    end

  (* navigating in a tree using a zipper *)

  type pointed 'a = (tree 'a, zipper 'a)

  let function start (t: tree 'a) : pointed 'a = (t, Top)

  let function up (p: pointed 'a) : pointed 'a = match p with
    | _, Top -> p (* do nothing *)
    | l, Left z x r | r, Right l x z -> (Node l x r, z)
  end

  let function top (p: pointed 'a) : tree 'a = let t, z = p in zip t z

  let function down_left (p: pointed 'a) : pointed 'a = match p with
    | Empty, _ -> p (* do nothing *)
    | Node l x r, z -> (l, Left z x r)
  end

  let function down_right (p: pointed 'a) : pointed 'a = match p with
    | Empty, _ -> p (* do nothing *)
    | Node l x r, z -> (r, Right l x z)
  end

end

```

--------------------------------

### Why3 module ExpLog: exponential and logarithm functions

Source: https://why3.org/stdlib/real.html

Declares exp and log functions with axioms for their algebraic properties, defines e as exp 1.0, and provides log2 and log10 derived functions. Includes lemmas for exp_sum_opposite and monotonicity of log2/log10.

```why3
module ExpLog

  use Real

  val function exp real : real
  axiom Exp_zero : exp(0.0) = 1.0
  axiom Exp_sum : forall x y:real. exp (x+y) = exp x * exp y
  axiom exp_increasing : forall x y. x <= y -> exp(x) <= exp(y)
  axiom exp_positive : forall x. exp(x) > 0.0
  axiom exp_inv : forall x. exp (-x) = inv (exp x)
  lemma exp_sum_opposite: forall x : real. exp(x) + exp(-x) >= 2.0

  constant e : real = exp 1.0

  val function log real : real
  axiom Log_one : log 1.0 = 0.0
  axiom Log_mul :
    forall x y:real. x > 0.0 /\ y > 0.0 -> log (x*y) = log x + log y
  axiom log_increasing : forall x y. 0.0 < x <= y -> log(x) <= log(y)

  axiom Log_exp: forall x:real. log (exp x) = x

  axiom Exp_log: forall x:real. x > 0.0 -> exp (log x) = x

  function log2 (x : real) : real = log x / log 2.0
  function log10 (x : real) : real = log x / log 10.0

  lemma log2_increasing : forall x y. 0. < x <= y -> log2(x) <= log2(y)
  lemma log10_increasing : forall x y. 0. < x <= y -> log10(x) <= log10(y)

end

```
Tokens:
Raw