The examples in the body of the manual show how objects and operations can be
defined in a number of forms. This Appendix summarizes each of the
definitional forms.
A.1. Object Definition Forms
The most complete form of object definition is the following:
object name iswhere the square brackets denote optional terms. This long-form specifies a composite type if the components attribute is non-empty, or an opaque type if the components attribute is missing or defined as empty.
[components: ...;]
[operations: ...;]
[equations: ...;]
[description: ...;]
[<user-defined attributes>; ... ;]
end <name>
The following is a shorter definition form used to specify atomic types:
object name is name [Notice in this shorter form that the components attribute is missing. The other attributes remain optional in the short form.
[operations: ...;]
[equations: ...;]
[description: ...;]
[<user-defined attributes>; ... ;]
end <name>]
Replacing the keyword is with '=' defines a concrete value rather than an abstract type. The general format for a concrete object definition is as follows:
object name = expression [Notice that components, operations, and equations attributes are all missing in a concrete value definition. Formally, it is inappropriate to include these attributes for a concrete value, so their inclusion is disallowed syntactically.
[description: ...;]
[<user-defined attributes>; ... ;]
end <name>]
The simplest form of object specification is a fully opaque type, defined as:
object name;
The following short-form definitions may be used:
obj name is composition expression [Here the object components or expression are specified immediately after the keyword is or the "=" symbol, and all other attributes are optional. Note where the keyword with may be optionally added for readability.
[with]
[operations: ...;]
[equations: ...;]
[description: ...;]
[<user-defined attributes>; ... ;]
end <name>]
obj name is composition expression [
[with]
[description: ...;]
[<user-defined attributes>; ... ;]
end <name>]
The general forms for operation definition are analogous to the object forms. The long-form operation definition is the following:
operation name isThis form defines a user-visible operation with optional attributes. A non-user-visible auxiliary function can be defined in two forms, the first of which is:
[components: ...;]
[inputs: ...;]
[outputs: ...;]
[precondition: ...;]
[postcondition: ...;]
[description: ...;]
[<user-defined attributes>; ... ;]
end <name>
function name isThis form defines a non-constructive auxiliary function. The formal specification of such functions is given with pre/postconditions or equationally.
[inputs: ...;]
[outputs: ...;]
[precondition: ...;]
[postcondition: ...;]
[description: ...;]
[<user-defined attributes>; ... ;]
end <name>
The final function definition form is:
function name = (inputs):(outputs) = epxrThis form defines a constructive auxiliary function, where the given expression defines the concrete value computed by the function. Notice that a constructive function may optionally include pre/postconditions so that a both constructive and predicative definition can be supplied if desired. The two definitions can provide complementary but equivalent specifications.
[precondition: ...;]
[postcondition: ...;]
[description: ...;]
[<user-defined attributes>; ... ;]
end <name>