DArray

Arrays which grow in size as needed. These arrays have an actual size (number of elements) and a maximum size (number of elements which can be inserted into the array without exceeding ).

Signature of DArray

List of Import References :
See Array
See BOOL
See Bitset
See DENOTATION
See Nat
See Option

SIGNATURE DArray [data]

$Date: 2010-09-30 18:24:17 +0200 (Do, 30. Sep 2010) $ ($Revision: 616 $)

Parameter

SORT data

Imports

IMPORT Nat ONLY nat
       Option[data] ONLY option

the type itself

SORT dArray

constructing new dArrays

init (n,d) === init (n,\\ _ .d): generate dArray of size n and initial data f(i) for i = 0 .. n-1. init(0, f) is the empty dArray. The maximum size is the double initial size

FUN init: nat**data->dArray                     
    init: nat**(nat->data)->dArray              

As above, butwih additional higher-order parameter to set the maximum size explicitly

FUN init: nat -> nat ** data -> dArray                  
    init: nat -> nat ** (nat -> data) -> dArray         

the empty dArray (maximum size is 16) or explicitly given

FUN empty: dArray
FUN empty: nat -> dArray

working on an dArray

upd (i,d,a) === (a,i) := d: update i-th element of dArray a with value d where i ranges from 0 upto #(a). dArray is extended, as needed.

FUN upd : nat**data**dArray->dArray             
    :=  : dArray**nat**data->dArray

upd (i,f,a): update i-th element of dArray a with value f(a!i) where i ranges from 0 upto #(a).

 
FUN upd : nat**(data->data)**dArray->dArray     
 

swap(a,i,j): swap elements i and j of dArray a; undefined, if either i >= #(a) or j >= #(a)

FUN swap: dArray**nat**nat->dArray              

extend(a,n,d) === extend(a,n,\\ _ . d): extend dArray by n entrys at the end. Informally: extend(a,n,f) == a ++ init(n,f), but maximum size is only extended, if necessary (in contrast to ++).

FUN extend: dArray ** nat ** data -> dArray
    extend: dArray ** nat ** (nat -> data) -> dArray

accessing elements of an dArray

a ! i: select i-th element of dArray a, where i ranges from 0 upto #(a)-1.

FUN !   : dArray**nat->data                     

FUN !?  : dArray ** nat -> option[data]

information about an dArray

#(a): (actual size of dArray a.

FUN #   : dArray->nat   

is dArray empty?

FUN empty? : dArray -> bool

guaranteed free entry

FUN new: dArray -> nat

is Array defined at position

FUN def? : nat ** dArray -> bool

The inner nondynamic array

IMPORT Bitset ONLY set
       Array[data] ONLY array

TYPE dArray == abs(rep: array[data], occ: set, new: nat)

next node: DArrayConv,
prev node: Subsystem Dynamic Arrays,
up to node: Subsystem Dynamic Arrays