Object-Z allows class types to be defined using a box very
similar to the schema box previously described.
It allows the previously described boxed environments
(as well as nested sub-classes) to be placed within a class box.
In addition, special names can be used for some of the boxed-environments
when they appear within a class box.
The following example illustrates a class definition.
#example71#
The 8 environment hasn't been seen before.
It creates a paragraph of text with the same margins as used
for schemas and other Z environments. It uses a special font
intended for use when placing comments inside classes.
A similar environment, 9, uses the same margins
but with the normal roman font.
The 10 command is an abbreviation for
11. Similarly 12
is a more meaningful synonym for 13.
You will be given LATEX warning messages if you try to
use a 14 environment outside of a class box
or if you try to place an environment such as 15
inside a class. You can ask for additional help in these
cases using the normal LATEX 16 or 17 help commands.
If you proceed with LATEXing, the macros will attempt to
do the best they can to do what you probably intend, even though
you are violating the recommended nesting guidelines.