C-2 -- 2.3 Structured and Architectural Specifications

Go backward to 2.2 Basic Items
Go up to 2 Simple Mark-Up

2.3 Structured and Architectural Specifications

A definition of a structured specification is marked up as indicated in Table 3: a list of item commands in a SpecDefn environment, with the name of the specification as argument. The keyword before the name is by default `spec'; it can be changed to `arch spec' by inserting the optional argument [\Arch~\Spec] for the SpecDefn environment, and similarly for `unit spec' and `view'. The equality sign of the definition is written after the specification name.

Table 3: SpecDefn
LaTeX source:
SpecDefn.tex
Formatted:

spec
Spec_Name ... =
...
...
...
...
...
...
...

end

A specification name in mixed upper and lower case is formatted in SMALL_CAPS by LaTeX, but merely in a larger font by Hyperlatex. Any underlined spaces have to be marked up as \_. A reference to the specification name is marked up using the command \SpecName{...}.

Any generic parameters and imports are inserted between the specification name and the equality sign.

Each part of a compound structured specification is marked up by a \item[...] command, often with with a keyword as its optional argument, e.g., \item[\Then]. The keyword is marked up as command with the corresponding spelling, except that the first letter is put in uppercase.

The Items environment may be used to produce indentation and alignment of parts of structured specifications, as described in Section 2.1. Some of the various possibilities are indicated in Table 4. Lists of basic items within items should be themselves enclosed in Items environments.

Table 4: Structured-Alignment
LaTeX source:
Structured-Alignment.tex
Formatted:

spec
A_Spec ... =
{
...
...
...
...
...
... }

then

...
...
...
...
...
...

then
... and

B_Spec with
... ^_|-> ...,

...,

... ^_|-> ...

then

free

...
hide
...

CoFI Note: C-2 -- Version: 0.3 (for CASL v1.0) -- 30 November 1998.
Comments to mosses@csl.sri.com