The Sequence Abstract Data Type

A text editor maintains a sequence of characters, by implementing some variant of the abstract date type Sequence. One definition of the Sequence abstract data type is:

Domains:

• ITEM -- the data type that this is a sequence of (in most cases it will be an ASCII character).
• SEQUENCE -- an ordered set of ITEMs.
• POSITION -- an index into the SEQUENCE which identifies the ITEMs (in this case it will be a natural number from 0 to the length of the SEQUENCE minus one).

Syntax:

• Empty : SEQUENCE
• Insert : SEQUENCE POSITION ITEM SEQUENCE
• Delete : SEQUENCE POSITION SEQUENCE
• ItemAt : SEQUENCE POSITION ITEM {EndOfFile}

Types:

• s : SEQUENCE;
• i : ITEM;
• p, , : POSITION;

Axioms:

1. Delete(Empty,p) = Empty

2. if then

   if then s

   if then

3. ItemAt(Empty, p) = EndOfFile

4. if then

   if then i

   if then

The definition of a SEQUENCE is relatively simple. Axiom 1 says that deleting from an Empty SEQUENCE is a no-op. This could be considered an error. Axiom 2 allows the reduction of a SEQUENCE of Inserts and Deletes to a SEQUENCE containing only Inserts. This defines a canonical form of a SEQUENCE which is a SEQUENCE of Inserts on a initial Empty SEQUENCE. Axiom 3 implies that reading outside the SEQUENCE returns a special EndOfFile item. This also could have been an error. Axiom 4 defines the semantics of a SEQUENCE by defining what is at each position of a canonical SEQUENCE.