Why3 Standard Library index

# Arrays with bounded-size integers

Note: We currently duplicate code to get the various modules below but we should eventually be able to implement a single module and then to clone it.

## Arrays with 32-bit indices

```module Array32

use import mach.int.Int32
use import map.Map as M

type array 'a model { length: int32; mutable elts: map int 'a }
invariant { 0 <= to_int 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: int32) : 'a
requires { "expl:index in array bounds" 0 <= to_int i < to_int a.length }
ensures  { result = a[to_int i] }

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

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

```

unsafe get/set operations with no precondition

```  exception OutOfBounds

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

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

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

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

val sub (a: array ~'a) (ofs: int32) (len: int32) : array 'a
requires { 0 <= to_int ofs /\ 0 <= to_int len }
requires { to_int ofs + to_int len <= to_int a.length }
ensures  { result.length = len }
ensures  { forall i:int. 0 <= i < to_int len ->
result[i] = a[to_int ofs + i] }

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

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

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

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

end

```

## Arrays with 31-bit indices

```module Array31

use import mach.int.Int31
use import map.Map as M

type array 'a model { length: int31; mutable elts: map int 'a }
invariant { 0 <= to_int 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: int31) : 'a
requires { "expl:index in array bounds" 0 <= to_int i < to_int a.length }
ensures  { result = a[to_int i] }

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

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

```

unsafe get/set operations with no precondition

```  exception OutOfBounds

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

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

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

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

val sub (a: array ~'a) (ofs: int31) (len: int31) : array 'a
requires { 0 <= to_int ofs /\ 0 <= to_int len }
requires { to_int ofs + to_int len <= to_int a.length }
ensures  { result.length = len }
ensures  { forall i:int. 0 <= i < to_int len ->
result[i] = a[to_int ofs + i] }

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

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

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

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

end

```

## Arrays with 63-bit indices

```module Array63

use import mach.int.Int63
use import map.Map as M

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

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

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

```

syntactic sugar

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

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

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

val length (a: array63 ~'a) : int63 ensures { result = a.length }

```

unsafe get/set operations with no precondition

```  exception OutOfBounds

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

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

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

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

val sub (a: array63 ~'a) (ofs: int63) (len: int63) : array63 'a
requires { 0 <= to_int ofs /\ 0 <= to_int len }
requires { to_int ofs + to_int len <= to_int a.length }
ensures  { result.length = len }
ensures  { forall i:int. 0 <= i < to_int len ->
result[i] = a[to_int ofs + i] }

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

let fill (a: array63 ~'a) (ofs: int63) (len: int63) (v: 'a)
requires { 0 <= to_int ofs /\ 0 <= to_int len }
requires { to_int ofs + to_int len <= to_int a.length }
ensures  { forall i:int.
(0 <= i < to_int ofs \/
to_int ofs + to_int len <= i < to_int a.length) -> a[i] = (old a)[i] }
ensures  { forall i:int. to_int ofs <= i < to_int ofs + to_int len ->
a[i] = v }
= 'Init:
for k = 0 to Int.(-) (to_int len) 1 do (* FIXME: for loop on int63 *)
invariant { forall i:int.
(0 <= i < to_int ofs \/
to_int ofs + to_int len <= i < to_int a.length) ->
a[i] = (at a 'Init)[i] }
invariant { forall i:int. to_int ofs <= i < to_int ofs + k -> a[i] = v }
let k = of_int k in
a[ofs + k] <- v
done

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

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

end

(* TODO
- Array64 ?
*)
```

Generated by why3doc 0.88.0