Object and operations may inherit from other objects and operations. Consider again the PersonRecord object defined earlier: class:

object PersonRecord
    components: Name and Age and Address;
    description: (*
        The PersonRecord class contains components that are common
        to all personnel in the database.
    *);
end PersonRecord;

object StaffEmployee extends PersonRecord
    components: HourlyWage and EmploymentStatus;
    operations: ;
    description: (*
        A StaffEmployee is distinguished by HourlyWage and
        EmploymentStatus components.
    *);
end StaffEmployee;

object Programmer
    components: Salary and Step;
    operations: ;
    description: (*
        A Programmer is distinguished by Salary and Step
        components.
    *);
end Programmer;

object Manager extends PersonRecord
    components: Salary and Step and Supervisees;
    description: (*
        A Manager is distinguished by Salary, Step, and Supervisees
        components.
    *);
end Manager;

object Supervisees
    components: (StaffEmployee or Programmer)*;
    description: (*
        This is the list of people that a manager supervises.
    *);
end Supervisees;

As is common in object-oriented language descriptions, the terms "parent" and "child" are used to refer to the relative positions of objects in an inheritance hierarchy. In this example, SPersonRecord is the parent object, StaffEmployee and Manager are child objects. The purpose of a parent is to define components and other attributes that are common to all children. The children automatically inherits the parent attributes, and add zero or more specializing attributes.

Class inheritance may be defined in any number of levels. Consider the following refinement of the preceding example:

object PersonRecord
    components: Name and Age and Address;
    description: (*
        The PersonRecord class contains components that are common
        to all personnel in the database.
    *);
end PersonRecord;

object StaffEmployee extends PersonRecord
    components: HourlyWage and EmploymentStatus;
    operations: ;
    description: (*
        A StaffEmployee is distinguished by HourlyWage and
        EmploymentStatus components.
    *);
end StaffEmployee;

object SalariedEmployee extends PersonRecord
    components: Salary and Step;
end SalariedEmployee;

object Programmer extends SalariedEmployee
    description: (*
        A Programmer is now just an extends SalariedEmployee,
        from which in inherits components Salary and Step components.
    *);
end Programmer;

object Manager extends SalariedEmployee
    components: Supervisees;
    description: (*
        A Manager inherits Salary and Step components.  It
        specializes with Supervisees.
    *);
end Manager;

object Supervisees
    components: (StaffEmployee or SalariedEmployee)*;
    description: (*
        This is the list of people that a manager supervises.
    *);
end Supervisees;

The following rules define precisely what it means for on object to inherit from another.

1. The components of the parent are automatically copied into the components of the child. Any new components specified in the child are anded onto the parent components. Specifically, if the components expression appearing in the parent is E and the components expression appearing in the child is E', then the component expression of the child is defined as E and E'.
2. Any explicitly specified operations and equations are automatically copied into the child, with all occurrences of the parent name substituted with the child name. This leads to the notion of an "inherited operation", the semantics of which are defined shortly.
3. No other parent attributes are inherited.
4. An inherited operation need not be explicitly defined. If it is, its signature must match exactly the signature of the operation generated via the inheritance mechanism, and this explicitly defined operation will be deemed a "defined inherited operation". The operation from which it was derived will be deemed its "parent operation".
5. The pre/post conditions of a parent operation are automatically copied into the pre/post conditions, respectively, of the defined inherited operation. Any new pre/post conditions specified in the defined inherited operation are logically anded onto the parent operation pre/post conditions. I.e., if the pre/post conditions appearing in the parent are P/Q and the pre/post conditions appearing in the defined inherited operation are P'/Q', then the pre/post conditions of the defined inherited operation are defined as (P and P')/(Q and Q').

Multiple inheritance is not currently supported in SpecL.

4.3. Parent Objects as Types

It was noted earlier that an abstract object formally defines a type, in the same sense as in strongly-typed programming languages. In most object- oriented programming languages, the class/subclass relationship formally defines a type/subtype relationship. The same is true in SpecL.

The major effect of subtyping in an object-oriented language relates to the use of class and subclass objects in operation parameters. Specifically, the typing rule for operation parameters is the following:

A formal parameter of a class type may accept an actual parameter of that
type, as well as any inheriting type(s) of which the formal type is an
parent.

Need to cover the issue, with examples, of precisely what it means to inherit from a parent object that is not defined as a tuple. The bottom line is that any non-opaque, non-tuple object is inherited as a single field into the inheriting object. In particular, inheriting from a union means that the inheriting type inherits exactly one field.

The more bottom line here is that inheriting from types other than tuples may not be all the useful in many cases, and in any case, you need to understand what you're getting.

Cover the following exaples, and perhaps more:

• inheritance-from-singletons.sl
• inheritance-from-unions.sl