Runtime Verification for Generic Classes with CONGU2 - Formal Methods: Foundations and Applications - page 35

Fig. 1. The three elements involved in the specification of lists with merge ADT

The specification ListWM presented in Figure 1 is an example of a parameterized
specification. Its parameter is the specification Mergeable , also presented in the figure.
Each specification introduces a sort. In our example, Mergeable introduces a simple sort
named after it while ListWM introduces the parameterized sort ListMW[Mergeable]

.

The sort , representing the domain of integer numbers, is primitive in the language.

Then, each specification declares three sets of operations and predicates. Operations
declared as constructors are those from which all values of the introduced sort can be
built. The other two sets include the operations and also predicates that provide funda-
mental information about the values of the sort, or are redundant, but useful, operations.
The sort of the first argument of these operations is required to be the introduced sort.
The difference between the two groups is only on the syntactical structure of the ax-
ioms that can be used to define their properties. Axioms for observers are required to be
expressed in terms of their application to constructors as first argument and variables

int