The following two sections contain the example used throughout this book: a doubly linked list with positions and iterators (module LIST), and a dynamic component with properties (module PROPERTY). To illustrate the concrete syntax of Mojave and to demonstrate the application of the universe type system, we present the implementation of both modules in the following. The classes Node, List, ListPos, and ListProperty also contain specifications. For these classes, we present the abstract fields and type invariants with defand depends-clauses, the requires- and modifies-clauses of their methods, and some pre-post-pairs. In the example, we use true as default formula if reqclauses or single pre- or postconditions are omitted.
Unable to display preview. Download preview PDF.