About

dictionary :

1. abstract data type

One of the simplest abstract data types is the stack. The operations new(), push(v, S), top(S), and popOff(S) may be defined with axiomatic semantics as following.
new() returns a stack
popOff(push(v, S)) = S
top(push(v, S)) = v

where S is a stack and v is a value. (The usual pop operation is a combination of top, to return the top value, and popOff, to remove the top value.) Contrast this with the axiomatic semantics definition of a set, a dictionary, or a queue.

From these axioms, one may define equality between stacks, define a pop function which returns the top value in a non-empty stack, etc. For instance, the predicate isEmpty(S) may be added and defined with the following additional axioms.

isEmpty(new()) = true
isEmpty(push(v, S)) = false

2. Formal Definition: Ignoring size an array may be seen as an abstract data type with the operations new(), set(i, v, A), and get(i, A), where i is a numeric index, v is a value, and A is an array. The operations may be defined with axiomatic semantics as follows.

• new() returns an array
• get(i, set(i, v, A)) = v
• get(i, set(j, v, A)) = get(i, A) if i ≠ jCompare this with a dictionary using integers as keys.

If the contents of a new array are set to some implicit initial value vi, we could add the following rule for get.

• get(i, new()) = vi

Typically arrays have a fixed size and use either 0-based indexing or 1-based indexing. Fixed initial size and 0-based indexing may incorporated as follows.

new(s) returns an array, which has a size s

• size(new(s)) = s
• size(set(i, v, A)) = size(A)
• get(i, set(i, v, A)) = v if 0 ≤ i < size(A)
• get(i, set(j, v, A)) = get(i, A) if i ≠ j