Types as behavior

In the previous chapter we have developed a formal definition of types and the subtyping relation. However, we have restricted ourselves to (syntactic) signatures only, omitting (semantic) behavioral properties associated with function and object types.

Subtype requirements -- signature and behavior

preservation of behavioral properties

Safety properties -- nothing bad

invariant properties -- true of all states
history properties -- true of all execution sequences

slide: Subtyping and behavior

From a behavioral perspective, the subtype requirements (implied by the substitutability property) may be stated abstractly as the preservation of behavioral properties. According to [Liskov93], behavioral properties encompass safety properties (which express that nothing bad will happen) and liveness properties (which express that eventually something good will happen). For safety properties we may further make a distinction between invariant properties (which must be satisfied in all possible states) and history properties (which hold for all possible execution sequences). See slide 10-properties. Behavioral properties (which are generally not captured by the signature only) may be important for the correct execution of a program. For example, when we replace a stack by a queue (which both have the same signature if we rename push and insert into put, and pop and retrieve into get) then we will get incorrect results when our program depends upon the LIFO (last-in first-out) behavior of the stack. As another example, consider the relation between a type FatSet (which supports the methods insert, select and size) and a type IntSet (which supports the methods insert, delete, select and size). See slide 10-history.

Example -- $IntSet \not<= FatSet$

FatSet -- insert, select, size
IntSet -- insert, delete, select, size

History property -- not satisfied by $IntSet$

$\A s : FatSet. \A %f, %q : State. %f < %q /\ s \e dom (%q).$
\hspace{2cm} $\A x : Int. x \e s_{%f} => x \e s_{%q}$

slide: History properties -- example

With respect to its signature, IntSet merely extends FatSet with a delete method and hence could be regarded as a subtype of FatSet. However, consider the history property stated above, which says that for any (FatSet) s, when an integer x is an element of s in state

%f

then x will also be an element of s in any state

%q

that comes after

%f

. This property holds since instances of FatSet do not have a method delete by which elements can be removed. Now if we take this property into account, IntSet may not be regarded as a subtype of FatSet, since instances of IntSet may grow and shrink and hence do not respect the FatSet history property. This observation raises two questions. Firstly, how can we characterize the behavior of an object or function and, more importantly, how can we extend our notion of types to include a behavioral description? And secondly, assuming that we have the means to characterize the behavior of a function or object type, how can we verify that a subtype respects the behavioral constraints imposed by the supertype?

The answer to the first question is suggested by the observation that we may also express the constraints imposed by the signature by means of logical formulae that state the constraints as assertions which must be satisfied.

Types as behavior -- constraints

$x : 9..11$ $<=>$ $x : Int /\ 9 <= x <= 11$

Behavioral constraints -- signature versus assertions

$f(x:9..11) : 3..5 { ... }$


    int f(int x) {
       require( 9 <= x  && x <= 11 );
       ...
       promise( 3 <= result && result <= 5);
       return result;
       }

slide: Types and behavioral constraints

For example, we may express the requirement imposed by typing a variable as an element of an integer subrange also by stating that the variable is an integer variable that respects the bounds of the subrange. Similarly, we can express the typing constraints on the domain and range of a function by means of pre- and post-conditions asserting these constraints. See slide 10-constraints. More generally, we may characterize the behavior of a function type by means of pre- and post-conditions and the behavior of an object type by means of pre- and post-conditions for its methods and an invariant clause expressing the invariant properties of its state and behavior. Recall that this is precisely what is captured in our notion of contract, as discussed in section contracts. With regard to the second question, to verify behavioral properties (expressed as assertions) we need an assertion logic in the style of Hoare. Such a logic will be discussed in the next section. In addition, we need a way in which to verify that (an instance of) a subtype respects the behavioral properties of its supertype. In section correspondence we will give precise guidelines for a programmer to check the behavioral correspondence between two types.

[] readme course preface 1 2 3 4 5 6 7 8 9 10 11 12 appendix lectures resources

eliens@cs.vu.nl

draft version 0.1 (15/7/2001)