As noted in the introduction, the primary components of an SpecL definition are objects and operations. Objects and operations have similar forms of definition, as the following subsections illustrate.

3.1. Defining Objects

An object is specified in a fixed format showing its components and other attributes. The general form is as follows (boldface terms are keywords, italic terms are variables, optional terms are enclosed in square brackets [ ... ]):

object name
components: composition expression defining subobjects;
operations: list of applicable operations;
equations: formal equations for operations;
[description: free-form text;]
[other attributes: user-defined information;]
end [name]

The most signficant attribute of an object is components. For this reason, there is a convenient short form of object definition that specifies just the object name and its compoents:

object name = composition expression

The following are example object definitions:

object PersonDatabase
    components: PersonRecord*;
    operations: AddRecord, DeleteRecord, FindRecord, CreateDatabase;

    description: (*
        A PersonDatabase contains zero or more personal information
        records.
    *);
end PersonDatabase;

object PersonRecord
    components: Name and Age and Address;
    description: (*
        A PersonRecord contains the information items for an
        individual in the PersonDatabase.
    *);
end PersonRecord;

object Name = string;
object Age = number;
object Address = string;

Each object definition in a specification defines an individual type of object. In relationship to a typed programming language, object definitions in SpecL are analogous to type definitions in a programming language. That is, each object defines a type structure for a typically infinite set of concrete values. SpecL types are generally more abstract than most programming language types, as will be discussed later.

3.2. Defining Operations

An operation specification is syntactically much like an object specification, in a fixed format of components and other attributes. Here is the general form:

operation name
    components: composition expression defining suboperations ;
    inputs: list of objects;
    outputs: list of objects;
    precondition: formal predicate on inputs];
    postcondition: formal predicate on inputs and outputs];
    [description: free-form text;]
    [other attributes: user-defined information;]
end name

The most signficant attributes of an operation are its inputs and outputs. For this reason, there is a convenient short form of operation definition that specifies just the object name and its compoents:

operation name(list of objects) -> (list of objects)

For example, here are some companion operations to the earlier object examples:

operation AddRecord
    inputs: PersonDatabase, PersonRecord;
    outputs: PersonDatabase;
    description: (*
        Add a new record into a person database.
    *);
end AddRecord;

operation DeleteRecord
    inputs: PersonDatabase, Name;
    outputs: PersonDatabase;
    description: (*
        Delete an existing record by Name.
    *);
end DeleteRecord;

operation FindRecord
    inputs: PersonDatabase, Name, PersonRecord;
    outputs: PersonRecord;
    description: (*
        Find an existing record by Name.
    *);
end FindRecord;

operation CreateDatabase
    inputs: none;
    outputs: PersonDatabase;
    description: (*
        Create an initially empty person database.
    *);
end CreateDatabase;

Operation definitions may be overloaded in the sense of overloading as typically defined in programming languages. That is, an operation of a given name may be defined two or more times, as long as the operation signatures differ. The term signature refers collectively to the inputs and outputs of an operation. Hence, a legal operation overload is a definition in which the type of at least one input or output differs from all other operation definitions of the same name.

3.3. Component Expressions

The components of an object or operation are defined using a composition expression. There are five forms of object composition, as outlined in the introduction of the report: and, or, repetitive, functional, and recursive. Table 4 summarizes the SpecL symbols used in composition expressions.

The symbols for the same composition form are synonyms. That is, ',' and the keyword and have exactly the same meaning. The synonymous forms exist simply for stylistic convenience.

The names that appear in a composition expression are the names of other defined entities. Consider the following example:

object O is
    components: O1 and O2 or O3;
end O;

The precedence of composition operators from lowest to highest is: or, and, '*'. Composition expressions can include parentheses, in the normal way, for grouping and changing precedence. For example,

(A or B) and (C or D).

While any level of parenthesis nesting is possible, it is recommended that parentheses be used sparingly in practice. For example, consider the following definition:

object Database is
    components: (Name and Addr and Age)*;
end DB;

object Database is
    components: Record*;
end DB;

object Record is
    components: Name and Addr and Age;
end Record;

Each of the five composition primitives defines a particular structure. Used in combination, the composition primitives can define a wide variety of structures commonly used in specifications. The following subsections provide further details and examples on the use of the SpecL composition forms.

3.3.1. And Composition

The and composition operator defines a heterogeneous collection of objects. In mathematical terms, an and-structure is a tuple. In relation to a programming language, an and-structure is analogous to a record type. That is, the and operator defines an object with a fixed number of components, where the components may be any other type of object. For example, the following definition specifies an object with exactly three components:

object A is
    components: X and Y and Z;
end A;

The components of an and-structure are never optional. That is, each component is always present.

3.3.2. Or Composition

The or composition operator also defines a heterogeneous collection of objects. In mathematical terms, an or-structure is a tuple of boolean-tagged elements, where exactly one of the elements is tagged true, and all other pairs are tagged false. The true tag indicates which of the or-structure elements is present. In relation to a programming language, an or-structure is analogous to a union type or variant record.

The following definition specifies an object with one of three possible components:

object O is
    components: X or Y or Z;
end O;

The repetitive composition operator defines a homogeneous collection of zero or more objects. In mathematical terms, a repetitive structure is an indexed bag (a bag is a set with duplicate entries allowed). In relation to a programming language, a repetitive structure is analogous to a list or array. However, a repetitive structure differs significantly from an array in that a repetitive structure is not of a fixed size.

The following definition specifies an object with zero or more components:

object L is
    components: X*;
end L;

Functional composition defines an object which is a function from zero or more inputs to zero or more outputs. In mathematical terms, SpecL function composition corresponds directly to the mathematical function composition of higher-order logics. In relation to a programming language, a function composition is analogous to a procedure or function type, or a function pointer. However, function composition differs from most programming languages in that multiple output types are possible, whereas in programming languages typically only a single output type is allowed.

In SpecL, functional composition provides a conceptual connection between objects and operations. Specifically, any operation definition defines a value of a function type.

The following definition specifies an object composed as a function from types X and Y to types X, Y, and Z.

object F is
    components: op(X,Y)->(X,Y,Z);
end F;

Unlike the preceding three composition forms, recursive composition has no explicit composition operator. A recursive definition results when an object is defined such that it contains itself as a component, or subcomponent. In mathematical terms, a recursive structure corresponds to a recursive mathematical definition. In relation to a programming language, a recursive structure corresponds to a recursive type definition, which is typically defined using a pointer. However, a recursive structure in SpecL is not a pointer-based definition. SpecL contains no pointers.

The following are examples of recursive definitions:

object R is
    components: X and Y and R;
end R;

object R1
    components: R2 and R3 and R4;
end R1;

object R2 is
    components: R5 and R6;
end R2;

object R5 is
    components: R7 and R1;
end R5;

The PersonDatabase object in Section 3.3.1 is a good example of and-composition. An example of or-composition is

object MaritalStatus is
    components: Married or Unmarried or Widowed or Divorced;
end MaritalStatus;

It is common in specifications to define an object that contains any of a number of subobjects, intermixed in any order. Consider the following example:

object UnformattedDocument
    components: (RawText or FormattingCommand)*;
    description: (*
        An UnformattedDocument contains RawText strings and
        formatting commands intermixed in any order.
    *);

components: (A or B or ... )*;

components: (A* and B* and ...)

The following example illustrates a practical use of recursive composition:

In operation definitions, only and-composition is meaningful. The use of or-composition in an operation definition is equivalent to and-composition and the use of list-composition is ignored. For example, the following two operation definitions are equivalent:

operation O1 is
    components: O2 or O3 or O4*;
end O1

operation O1 is
    components: O2 and O3 and O4;
end O1

As in a programming language, operation input/output lists define the formal parameter types that are accepted and produced by an operation. In contexts where operations are used with actual parameters, the same sort of type checking applies in SpecL as in a programming language. Namely, the type of each actual parameter must agree with the type of the corresponding formal parameter.

As noted in the introduction, all the operations defined in a specification are side effect free. This means that an operation cannot use any object unless that object is an explicit input. Further, an operation may effect change only through an explicit output. In the nomenclature of programming languages, SpecL is a fully functional language.

The notion that operations effect change rather than modify objects is also an important aspect of functional definition. An operation does not modify objects to produce output objects. Rather, a fully functional operation can only create new objects.

Consider the AddRecord example defined above. When this operation performs its function, it accepts a database and record as inputs. What it outputs is a new copy of the input database, with a new copy of the input record added into the database. In programming language terms, functional specifications have no global variables, no global files, and no call-by-var parameters. In this sense, SpecL functional definitions are similar to definitions in functional programming languages such as pure LISP and ML.

The fully functional specification of operations is sometimes counter- intuitive, particularly in the case of large objects in a transaction-oriented system. For example, one might consider the explicit input and output of a large database to be unnecessary and/or inefficient. It is necessary since in order to construct a result that contains a new record, the original database must be input. It cannot be assumed that the operation will read from some stored database file or other external storage structure.

With regards to implementation efficiency, this matter is strictly not of concern in an SpecL specification. It is almost certainly not the case that a DBMS implementation would copy entire databases from input to output. However, such implementation concerns are beyond the scope of an SpecL specification. The specification states in functional terms what an operation does, including all inputs and outputs that it uses. A subsequent implementation can use whatever efficient techniques are available, as long as the implementation meets the abstract specification.

3.5. Names and Types

In the examples thus far, the components of an entity have been shown as simple names. Consider the PersonRecord example from above:

object PersonRecord
    components: Name and Age and Address;
    description: (*
        A PersonRecord contains the information items for an
        individual in the PersonDatabase.
    *);
end PersonRecord;
object Name = string;
object Age = number;
object Address = string;

object PersonRecord
    components: n:Name and a:Age and ad:Address;
    description: (*
        A PersonRecord contains the information items for an
        individual in the PersonDatabase.
    *);
end PersonRecord;

Here the components are defined using name/type pairs. The component structure of PersonRecord is precisely the same in both of the above two definitions. The name component of the name/type pair is a local subobject name by which the component can be referenced. The names are n, a, and ad in this example. The type half of a name/type pair is the name of a defined object. The object types in this example are Name, Age, and Address.

Name/type pairs can also be used in operation inputs and outputs, as in this example:

operation AddRecord is
    inputs: pdb:PersonDatabase, pr:PersonRecord;
    outputs: pdb':PersonDatabase;
    description: (*
        Add a new record into a person database.
    *);
end AddRecord;

Component and input/output definitions can be legally specified with or without name/type pairs. Name/type pairs are necessary in formal SpecL specifications, as discussed later in Sections 7 and 8.

Name/type pairs can also be used to make an object definition more compact. Consider the following alternative example of the previously-defined PersonRecord:

object PersonRecord
    components: name:string and age:integer and address:string;
    description: (*
        A PersonRecord contains the information items for an
        individual in the PersonDatabase.
    *);
end PersonRecord;

Neither of the two forms is more correct than the other. The compact form saves some space, at the expense of potential object reuse. For example, of the Name object was used in multiple definitions, it could be clearer to use the less compact form of definition. Another advantage of the less compact form of definition is that the base atomic types can be given individual descriptions, for documenatary purposes, as in

object Name = string
    description: (* The name in a person record, or any other named object. *)
end

It is instructive to compare the use of name/type pairs in SpecL and common programming languages. Consider, for example, the equivalent of the last original PersonRecord definition in a C-like language:

typedef char* Name;
typedef int Number;
typedef char* Address;
typedef struct {
    Name n;
    Age a;
    Address a;
} PersonRecord;

As another example, consider the equivalent definition of PersonRecord in a Java-like language:

class PersonRecord {
    String name;
    int age;
    String address;
}

A significant difference between SpecL and most programming languages is that component names are not required in SpecL. Consider the following fictitious C and Java definitions, which are would-be equivalents to the most original SpecL definition of PersonRecord:

typedef char* Name;
typedef int Number;
typedef char* Address;
typedef struct {
    Name;
    Age;
    Address;
} PersonRecord;

class PersonRecord {
    String;
    int;
    String;
}

Any object defined with a non-empty components field is composite. An atomic object is one of the following:

• an object defined as a built-in type,
• an object with no components field, or
• an object defined with "components: empty".

An atomic object can be defined using the general object definition form:

object name
    components: type name;
        . . .
end name

object name = type name;

A special form of atomic definition is an opaque object. The general form of opaque definition is either of the following:

object name ;

object name
    components: ;
    . . .
end name

If the components keyword is given in an opaque definition, it must be followed by an empty components expression, or by the single keyword empty. The use of opaque definitions is discussed further in Section 3.8.

Opaque definitions are usefule to define "black box" objects. The mnemonic object name describes its purpose, but it has no other structure. A typical use for atomic object is in enumerated types, as in

object DayOfTheWeek = Sun or Mon or Tue or Wed or Thu or Fri or Sat;
object Sun;
object Mon;
object Tue;
object Wed;
object Thu;
object Fri;
object Sat;

typedef enum {Sun, Mon, Tue, Wed, Thu, Fri, Sat} DayOfTheWeek;

enum DayOfTheWeek {Sun, Mon, Tue, Wed, Thu, Fri, Sat};

Object definitions that use the keyword object define a formal object type. The keyword value is used to define a concrete value of some type. A type represents an abstract set of many possible values, typically an infinite set. A value represents a single concrete instance. For example, the standard type number represents the infinite set of all possible numbers. The value 10 represents the single numeric value 10.

As a user-defined example, the following object definition represents the set of all possible values that have a number component and a string component:

object NumberAndString
    components: number and string;
end NumberAndString;

value TenXYZ:NumberAndString = {10, "xyz"};

value value-name = value-expression
[ . . .
end name ]

value value-object-name:type-object-name = value-expression
[ . . .
end name ]

The second form is necessary when the type of the value expression cannot be inferred to a particular type. For example, in the definition

value TwoTuple = {10, "xyz"};

value TenXyz:NumberAndString = {10, "xyz"};

The value expression to the right of the "=" denotes the concrete value. A numeric value is denoted by a numeric literal. A string is denoted by a double-quoted string literal. A boolean value is denoted by one of the standard identifiers true or false.

A concrete composite and value is constructed using curly brace operators "{" and "}". A concrete composite list value is constructed using square bracket operators "[" and "]". For example, the object value {1, "abc", true} is an and'd value containing the number 1, string "abc", and boolean value true; [1, 2, 3] is a composite list value consisting of the numbers 1, 2 and 3. Composite values can be nested to any depth. Borrowing from normal mathematics terminology, an and'd value can be referred to as a tuple.

3.8. The Representational Base of Object Hierarchies

In order for an SpecL definition to be complete, all referenced entities must be defined. In particular, there must be a definition for any object referenced by name in the components part of another definition or in the input/output lists of an operation. At some point, the hierarchy of object definitions must "bottom out" at atomic objects. Given the forms of atomic object discussed above, there are three levels of abstraction for defining the atomic basis of an object hierarchy:

1. opaque objects
2. atomic objects defined as one of the built-in atomic types
3. atomic objects defined as a specific concrete value

As an example, recall the DatabaseQuery definition from above. In that example, the atomic objects NameKey, AgeKey, etc. were defined as opaque types. They could alternatively have been defined as string types, with the following definitions:

object NameKey = string;
object AgeKey = string;
object AddressKey = string;
object EqualsSign = string;
object OrQueryOperator = string;
object AndQueryOperator = string;

The most concrete definition of NameKey, etc., is as specific values, for example mnemonic strings. The following value-based definitions illustrate this most concrete level of refinement:

value NameKey = "NAME"
value AgeKey = "AGE";
value AddressKey = "ADDRESS";
value EqualsSign = "=";
value OrQueryOperator = "OR";
value AndQueryOperator = "AND";

When concrete objects are defined in a specification, it can be useful to specify operations that accept these objects as inputs and/or produce them as outputs. Consider the following addition to the PersonDatabase example presented earlier:

object DefaultName = "Name Unknown";
object DefaultAge = -1;
object DefaultAddress = "Address Unknown";
object DefaultPersonRecord = {DefaultName, DefaultAge, DefaultAddress};

operation AddRecord is
    inputs: PersonDatabase, PersonRecord:=DefaultPersonRecord;
    outputs: PersonDatabase;
    description: (*
        Add a new record into a person database.
    *);
end AddRecord;

The general format for defining default operation parameters is the following:

operation name is
inputs: type-name:=value-name, ... ;
outputs: type-name:=value-name, ... ;
end name;

A default value in a parameter list specifies what the standard parameter value should be, if no other value is given when an operation is invoked. Using parameter defaults, a specifier can define specific concrete values that constitute the standard required data for a system. When the system is implemented, these standard data will be those installed for initial system operation. In the absence of other user input that changes these values, the defaults will remain in use.

3.10. Definition Short Forms

In practice, the primary attribute specified for an object is its components and the primary attributes for an operation are its inputs and outputs. Given this, SpecL supports short-form definitions that allow objects and operations to be defined less verbosely than with the full-form notation used above. The short form definitions are:

obj name is composition expression;

op name (inputs)->(outputs);

object name is
components: composition expression;
end name

operation name is
inputs: inputs;
outputs: outputs;
end name;

object PersonRecord is Name and Age and Address
    description: (*
        A PersonRecord contains the information items for an
        individual in the PersonDatabase.
    *);
end PersonRecord;