2.1 Basic Specifications

A basic (anonymous, unstructured) specification is a list of basic-items constructs. It is marked up as indicated in Table 1: a BasicSpec environment containing a list of LaTeX \item commands, each with a keyword as argument. Each keyword is marked up as a command with the corresponding spelling, except that the first letter is put in uppercase. For example, \item[\Sorts] marks the start of a sort-items construct. `Bulleted' axioms in a local variable construct are marked up as \item[\.]

A basic-items construct consists of a series of individual basic items (declarations, definitions, or axioms), separated or terminated by semicolons. Each basic item should be separated from following basic items by an explicit newline \\ or by a blank line. To get the first basic item to start on a fresh line, precede it by ~\\.

---

Table 1: BasicSpec

 LaTeX source:

BasicSpec.tex

Formatted:

sort

...; ...;

ops

...;
...;
...

axioms

 
...;
...

---

A sort generation constraint on a group of sort and operation declarations is marked up as indicated in Table 2. The Items environment is used for subsidiary lists of items within basic (and other kinds of) specifications; its contents is marked up as for a BasicSpec environment.

---

Table 2: Generated

 LaTeX source:

Generated.tex

Formatted:

generated {

 

sort

...

ops

...;
...;
... }

axioms

 
...;
...

---