Why3 Standard Library index

# Arrays

## Generic Arrays

The length is a non-mutable field, so that we get for free that modification of an array does not modify its length.

```module Array

use import int.Int
use import map.Map as M

type array 'a model { length : int; mutable elts : map int 'a }
invariant { 0 <= self.length }

function get (a: array ~'a) (i: int) : 'a = M.get a.elts i

function set (a: array ~'a) (i: int) (v: 'a) : array 'a =
{ a with elts = M.set a.elts i v }

```

syntactic sugar

```  function ([]) (a: array 'a) (i: int) : 'a = get a i
function ([<-]) (a: array 'a) (i: int) (v: 'a) : array 'a = set a i v

val ([]) (a: array ~'a) (i: int) : 'a
requires { "expl:index in array bounds" 0 <= i < length a }
ensures  { result = a[i] }

val ([]<-) (a: array ~'a) (i: int) (v: 'a) : unit writes {a}
requires { "expl:index in array bounds" 0 <= i < length a }
ensures  { a.elts = M.set (old a.elts) i v }

val length (a: array ~'a) : int ensures { result = a.length }

```

unsafe get/set operations with no precondition

```  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 /\ 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

val make (n: int) (v: ~'a) : array 'a
requires { "expl:array creation size" n >= 0 }
ensures { length result = n }
ensures { forall i:int. 0 <= i < n -> result[i] = v }

val append (a1: array ~'a) (a2: array 'a) : array 'a
ensures { length result = length a1 + length a2 }
ensures { forall i:int. 0 <= i < length a1 -> result[i] = a1[i] }
ensures {
forall i:int. 0 <= i < length a2 -> result[length a1 + i] = a2[i] }

val 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] }

val copy (a: array ~'a) : array 'a
ensures  { length result = length a }
ensures  { forall i:int. 0 <= i < length result -> result[i] = a[i] }

let fill (a: array ~'a) (ofs: int) (len: int) (v: 'a)
requires { 0 <= ofs /\ 0 <= len /\ ofs + len <= length a }
ensures  { forall i:int.
(0 <= i < ofs \/ ofs + len <= i < length a) -> a[i] = (old a)[i] }
ensures  { forall i:int. ofs <= i < ofs + len -> a[i] = v }
= 'Init:
for k = 0 to len - 1 do
invariant { forall i:int.
(0 <= i < ofs \/ ofs + len <= i < length a) -> a[i] = (at a 'Init)[i] }
invariant { forall i:int. ofs <= i < ofs + k -> a[i] = v }
a[ofs + k] <- v
done

val 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] }

val self_blit (a: array ~'a) (ofs1: int) (ofs2: int) (len: int) : unit
writes {a}
requires { 0 <= ofs1 /\ 0 <= len /\ ofs1 + len <= length a }
requires { 0 <= ofs2 /\             ofs2 + len <= length a }
ensures  { forall i:int.
(0 <= i < ofs2 \/ ofs2 + len <= i < length a) -> a[i] = (old a)[i] }
ensures  { forall i:int.
ofs2 <= i < ofs2 + len -> a[i] = (old a)[ofs1 + i - ofs2] }

end

```

## Sorted Arrays

```module IntArraySorted

use import int.Int
use import Array
clone import map.MapSorted as M with type elt = int, predicate le = (<=)

predicate sorted_sub (a : array int) (l u : int) =
M.sorted_sub a.elts l u
```

`sorted_sub a l u` is true whenever the array segment `a(l..u-1)` is sorted w.r.t order relation `le`

```  predicate sorted (a : array int) =
M.sorted_sub a.elts 0 a.length
```

`sorted a` is true whenever the array `a` is sorted w.r.t `le`

```end

module Sorted

use import int.Int
use import Array

type elt

predicate le elt elt

predicate sorted_sub (a: array elt) (l u: int) =
forall i1 i2 : int. l <= i1 <= i2 < u -> le a[i1] a[i2]
```

`sorted_sub a l u` is true whenever the array segment `a(l..u-1)` is sorted w.r.t order relation `le`

```  predicate sorted (a: array elt) =
forall i1 i2 : int. 0 <= i1 <= i2 < length a -> le a[i1] a[i2]
```

`sorted a` is true whenever the array `a` is sorted w.r.t `le`

```end

```

## Arrays Equality

```module ArrayEq

use import int.Int
use import Array
use import map.MapEq

predicate array_eq_sub (a1 a2: array 'a) (l u: int) =
a1.length = a2.length /\ 0 <= l <= a1.length /\ 0 <= u <= a1.length /\
map_eq_sub a1.elts a2.elts l u

predicate array_eq (a1 a2: array 'a) =
a1.length = a2.length /\ map_eq_sub a1.elts a2.elts 0 (length a1)

end

module ArrayExchange

use import int.Int
use import Array
use import map.MapExchange as M

predicate exchange (a1 a2: array 'a) (i j: int) =
a1.length = a2.length /\
M.exchange a1.elts a2.elts 0 a1.length i j
```

`exchange a1 a2 i j` means that arrays `a1` and `a2` only differ by the swapping of elements at indices `i` and `j`

```end

```

## Permutation

```module ArrayPermut

use import int.Int
use import Array
use import map.MapPermut as M
use import map.MapEq
use import ArrayEq
use export ArrayExchange

predicate permut (a1 a2: array 'a) (l u: int) =
a1.length = a2.length /\ 0 <= l <= a1.length /\ 0 <= u <= a1.length /\
M.permut a1.elts a2.elts l u
```

`permut a1 a2 l u` is true when the segment `a1(l..u-1)` is a permutation of the segment `a2(l..u-1)`. Values outside of the interval (l..u-1) are ignored.

```  predicate permut_sub (a1 a2: array 'a) (l u: int) =
map_eq_sub a1.elts a2.elts 0 l /\
permut a1 a2 l u /\
map_eq_sub a1.elts a2.elts u (length a1)
```

`permut_sub a1 a2 l u` is true when the segment `a1(l..u-1)` is a permutation of the segment `a2(l..u-1)` and values outside of the interval (l..u-1) are equal.

```  predicate permut_all (a1 a2: array 'a) =
a1.length = a2.length /\ M.permut a1.elts a2.elts 0 a1.length
```

`permut_all a1 a2 l u` is true when array `a1` is a permutation of array `a2`.

```  lemma exchange_permut_sub:
forall a1 a2: array 'a, i j l u: int.
exchange a1 a2 i j -> l <= i < u -> l <= j < u ->
0 <= l -> u <= length a1 -> permut_sub a1 a2 l u

```

we can always enlarge the interval

```  lemma permut_sub_weakening:
forall a1 a2: array 'a, l1 u1 l2 u2: int.
permut_sub a1 a2 l1 u1 -> 0 <= l2 <= l1 -> u1 <= u2 <= length a1 ->
permut_sub a1 a2 l2 u2

```

### lemmas about `permut_all`

```  lemma exchange_permut_all:
forall a1 a2: array 'a, i j: int.
exchange a1 a2 i j -> permut_all a1 a2

end

module ArraySwap

use import int.Int
use import Array
use export ArrayExchange

let swap (a:array 'a) (i:int) (j:int) : unit
requires { 0 <= i < length a /\ 0 <= j < length a }
writes   { a }
ensures  { exchange (old a) a i j }
= let v = a[i] in
a[i] <- a[j];
a[j] <- v

end

```

## Sum of elements

```module ArraySum

use import Array
use import map.MapSum as M

```

`sum a l h` is the sum of `a[i]` for `l <= i < h`

```  function sum (a: array int) (l h: int) : int = M.sum a.elts l h

end

```

## Number of array elements satisfying a given predicate

```module NumOf
use import Array
use HighOrd
use import Bool
use int.NumOf as N

```

the number of a`i` such that `l <= i < u` and `pr i a[i]`

```  function numof (pr: int -> 'a -> bool) (a: array 'a) (l u: int) : int =
N.numof (\ i. pr i a[i]) l u

end

```

the number of a`i` such that `l <= i < u` and `a[i] = v`

```module NumOfEq
use import Array
use int.NumOf as N

function numof (a: array 'a) (v: 'a) (l u: int) : int =
N.numof (\ i. a[i] = v) l u
end

module ToList
use import int.Int
use import Array
use import list.List

function to_list (a: array 'a) (l u: int) : list 'a

axiom to_list_empty:
forall a: array 'a, l u: int. u <= l ->
to_list a l u = Nil

axiom to_list_cons:
forall a: array 'a, l u: int. l < u ->
to_list a l u = Cons a[l] (to_list a (l+1) u)

val to_list (a: array 'a) (l u: int) : list 'a
ensures { result = to_list a l u }

end
```

Generated by why3doc 0.87.3