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:
Syntax:
Types:
Axioms:
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.