| | | A Specification Language |
In this appendix, we describe the language for constructing specifications. The main syntactic elements of specifications are type expressions, value expressions, and declaration expressions denoting at the semantic level types, values, and declarations. We will frequently not distinguish between expressions and their denotations, and call both "types", "values", and "declarations", respectively.
In the following, the variables T, T1, T2, ..., Tn denote types, the variables E, E1, E2, ..., En denote values, the variables D, D1, D2, ..., Dn denote declarations, and the variables I, I1, I2, ..., In denote identifiers.
As for the lexical grammar (the rules for forming words) of the language, a specification consists of a sequence of tokens separated by white-space (which includes indentations and line breaks that have thus no significance). If a line contains the comment token %, the rest of the line (including the token) is ignored.
As for the syntactical grammar (the rules for forming sentences) of the language, a specification consists of a sequence of declarations each of which is terminated by a semicolon:
D1;
D2;
...
Dn;
The lexical grammar and the syntactical grammar of the language are defined in Appendix F.
As for the semantics of a specification, the following sections describe the language's types, values, and declarations in an informal style. The primary purpose of these descriptions is easy readability, not ultimate preciseness; a formal definition of the language semantics remains subject of another paper.
| | | A Specification Language |