topical media & game development

[] readme course(s) preface I 1 2 II 3 4 III 5 6 7 IV 8 9 10 V 11 12 afterthought(s) appendix reference(s) example(s) resource(s) _

object-oriented programming

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

Contracts

subsections:

Specifying contractual obligations
Refining a contract
Runtime consistency checking

To establish the interaction between objects in a more precise way, we need a notion of contracts, specifying the requirements a client must comply with when requesting a service from a server object. Our notion of contracts will be based on the notion of types. In the universe of programming, types are above all a means to create order and regularity. Also, in an object-oriented approach, types may play an important role in organizing classes and their relationships. As observed in [HOB87], the notion of types gives a natural criterion for modularization, perhaps not so much as a guideline to arrive at a particular object decomposition, but as a means to judge whether the modular structure of a system is consistently defined, that is technically well-typed. The meaning of a type must be understood as a formal characterization of the behavior of the elements belonging to the type. A type consists of a (possibly infinite) collection of elements which is characterized by the definition of the type. For example, a class defines such a collection, namely the instances of the class, whose behavior is constrained by the specification of the class.

Specifying contractual obligations

A formal specification of the behavior of an object may be given by defining a pre-condition and post-condition for each method. The pre-condition of a method specifies in a logical manner what restrictions the client invoking a particular method is obliged to comply with. When the client fails to meet these requirements the result of the method will be undefined. In effect, after the violation of a pre-condition anything can happen. Usually, this means that the computation may be aborted or that some other means of error-handling may be started. For instance, when the implementation language supports exceptions an exception handler may be invoked. The post-condition of a method states what obligations the server object has when executing the method, provided that the client's request satisfies the method's pre-condition. Apart from specifying a pre-condition and post-condition for each method publicly supported by the class, the designer of the class may also specify a class invariant, to define the invariant properties of the state of each instance of the class. A class annotated with an invariant and pre- and post-conditions for the methods may be regarded as a contract, since it specifies precisely (in an abstract way) the behavioral conformance conditions of the object and the constraints imposed on the interactions between the object and its clients. See slide 3-obligations.

Assertions -- formal specification

require -- method call pre-condition
ensure, promise -- post-condition
invariant -- object invariance

slide: Formal specification of contracts

Intuitively, contracts have a clear analogy to our business affairs in everyday life. For instance, when buying audio equipment, as a client you wish to know what you get for the price you pay, whereas the dealer may require that you pay in cash. Following this metaphor through, we see that the supplier may actually benefit from imposing a (reasonable) pre-condition and that the client has an interest in a well-stated post-condition. Most people are not willing to pay without knowing what they will get for their money.

Language support

The use of contracts was originally proposed by [Meyer88], and is directly supported by the language Eiffel, which offers the keywords require (to indicate a pre-condition), ensure (to indicate a post-condition) and invariant (to indicate the invariance condition). See slide 3-formal. The Eiffel environment has options to dynamically check any of the three kinds of assertions, even selectively per class. The assertions, except for the invariance condition, are directly embedded in the code. Although less elegant, the same functionality can be achieved in C++ by using the assert macro defined in {\tt assert.h} as explained in section ASSERT, which also introduced the require and promise macros for C++.

For dynamically checking the invariance condition, a test should be executed when evaluating the constructor and before and after each method invocation. While a method is being executed, the invariant need not necessarily hold, but it is the responsibility of a method to restore the invariant when it is disrupted. In case object methods are recursively applied, the invariant must be restored when returning to the original caller.

An alternative approach to incorporating assertions in a class description is presented in [Cline], which introduces an extension of C++ called Annotated C++. Instead of directly embedding assertions in the code, Annotated C++ requires the user to specify separately the axioms characterizing the functionality of the methods and their effect on the state of the object.

Interfaces

Contracts may be used to document the method interface of a class. Pre- and post-conditions allow the class designer to specify in a concise manner the functional characteristics of a method, whereas the use of natural language often leads to lengthy (and imprecise) descriptions. Below, an example is given of a contract specifying an account.


  class account {     account  
  public:
  account();
  // assert( invariant() );
  
  virtual float balance() { return _balance; }
  
  void deposit(float x);  to deposit money
  // require(  $x >= 0$  );
  // promise( balance()  $==$  old_balance  $+$  x  && invariant() );
  
  void withdraw(float x);  to withdraw money
  // require( x  $<=$  balance() );
  // promise( balance()  $==$  old_balance  $-$  x && invariant() );
  
  bool invariant() { return balance()  $>=$  0; }
  protected:
  float _balance;
  };

slide: The $account$ contract

The interface for the account class specifies in an abstract way what the user expects of an account. From the perspective of design, the behavioral abstraction expressed by the axioms is exactly what we need, in principle. The implementation must guarantee that these constraints are met.

System development

From the perspective of system development, the notion of contracts has some interesting consequences. Assertions may be used to decide who is responsible for any erroneous behavior of the system. See slide 3-limits.

System development

violated pre-condition -- bug in client
violated post-condition -- bug in supplier

A pre-condition limits the cases that a supplier must handle!

slide: System development with contracts

For example, imagine that you are using a software library to implement a system for financial transactions and that your company suffers a number of losses due to bugs in the system. How would you find out whether the loss is your own fault or whether it is caused by some bug in the library? Perhaps surprisingly, the use of assertions allows you to determine exactly whether to sue the library vendor or not. Assume that the classes in the library are all annotated with assertions that can be checked dynamically at runtime. Now, when you replay the examples that resulted in a loss for your company with the option for checking pre- and post-conditions on, it can easily be decided who is in error. In the case that a pre-condition of a method signals violation, you, as a client of a library object, are in error. However, when no pre-condition violation is signaled, but instead a post-condition is violated, then the library object as the supplier of a service is in error; and you may proceed to go to court, or do something less dramatic such as asking the software vendor to correct the bug.

Realization

The contract specified in the account class interface may actually be enforced in code as illustrated below.


  class account {    account  
  public:
  account() { _balance = 0; assert(invariant()); }
  
  virtual float balance() { return _balance; }
  
  
  void deposit(float x) {
  	require( x >= 0 );  // check precondition
  	hold(); // to save the old state
  	_balance += x; 
  	promise( balance() == old_balance + x );
  	promise( invariant() );
  	}
  
  void withdraw(float x) {
  	require( x <= _balance );  // check precondition
  	hold(); // to save the old state
  	_balance -= x; 
  	promise( balance() == old_balance - x );
  	promise( invariant() );
  	}
  
  virtual bool invariant() { return balance() >= 0; }
  protected:
  float _balance;
  float old_balance; // additional variable
  virtual void hold() { old_balance = _balance; }
  };

slide: The realization of the $account$ contract

The additional variable {\em old_balance} is needed to compare the state preceding an operation with the state that results afterwards. The old state must explicitly be copied by calling hold. In this respect, Eiffel offers better support than C++. Whenever

balance()

proves to be less than zero, the procedure sketched above can be used to determine whether the error is caused by an erroneous method invocation, for example when calling

withdraw(x)

with

x >= balance()

, or whether the implementation code contains a bug. For the developer of the software, pre-conditions offer a means to limit the number of cases that a method must be able to handle. Often, programmers tend to anticipate all possible uses. For instance, many programs or systems have options that may be learned only when inspecting the source code but are otherwise undocumented. \nop{See for example [UndocDos].} Rather than providing all possible options, for now and the future, it is more sensible to delineate in a precise manner what input will be processed and what input is considered illegal. For the developer, this may significantly reduce the effort of producing the software.

Refining contracts

Contracts provide a means to specify the behavior of an object in a formal way by using logical assertions. In particular, a contract specifies the constraints involved in the interaction between a server object and a client invoking a method for that object. When developing a refinement subtype hierarchy we need to establish that the derived types satisfy the constraints imposed by the contract associated with the base type.

To establish that the contract of a derived class refines the contract of the base class it suffices to verify that the following rules are satisfied. See slide 3-inheritance.

Refining a contract -- state responsibilities and obligations

invariance -- respect the invariants of the base class
methods -- services may be added or refined

Refining a method -- like improving a business contract


  class C : public P {
  	virtual void m();
  	}

pre( $m_C$ ) $>=$ pre( $m_P$ )

post( $m_C$ ) $<=$ post( $m_P$ )

slide: Contracts and inheritance

First, the invariant of the base class must apply to all instances of the derived class. In other words, the invariance assertions of the derived class must be logically equal to or stronger than the assertions characterizing the invariant properties of the base class. This requirement may be verified by checking that the invariance properties of the base class can be logically derived from the statement asserting the invariance properties of the derived class. The intuition underlying this requirement is that the behavior of the derived class is more tightly defined and hence subject to stronger invariance conditions. Secondly, each method occurring in the base class must occur in the derived class, possibly in a refined form. Note that from a type-theoretical point of view it is perfectly all right to add methods but strictly forbidden to delete methods, since deleting a method would violate the requirement of behavioral conformance that adheres to the subtype relation. Apart from adding a method, we may also refine existing methods. Refining a method involves strengthening the post-condition and weakening the pre-condition. Suppose that we have a class C derived from a base class P, to verify that the method

m_C

refines the method

m_P

defined for the base class P, we must check, assuming that the signatures of

m_C

and

m_P

are compatible, that the post-condition of

m_C

is not weaker than the post-condition of

m_P

, and also that the pre-condition of

m_C

is not stronger than the pre-condition of

m_P

. This rule may at first sight be surprising, because of the asymmetric way in which post-conditions and pre-conditions are treated. But reflecting on what it means to improve a service, the intuition underlying this rule, and in particular the contra-variant relation between the pre-conditions involved, is quite straightforward. To improve or refine a service, in our commonsense notion of a service, means that the quality of the product or the result delivered becomes better. Alternatively, a service may be considered as improved when, even with the result remaining the same, the cost of the service is decreased. In other words, a service is improved if either the client may have higher expectations of the result or the requirements on the client becomes less stringent. The or is non-exclusive. A derived class may improve a service while at the same time imposing fewer constraints on the clients.

Example

As an example of improving a contract, consider the refinement of the class account into a class {\em credit_account}, which allows a consumer to overdraw an account to a limit of some maximum amount.


  class credit_account : public account {    credit_account  
  public:
  credit_account(float x) { _maxcredit = x; _credit = 0; }
  
  float balance() { return _balance + _credit; }
  
  float credit(float x) { 
  	require( x + _credit <= _maxcredit );
  	hold();
  	_credit += x;
  	promise( _credit = old_credit + x );
  	promise( _balance = old_balance);
  	promise( invariant() );
  	}
  
  void reduce(float x) {
  	require( 0 <= x && x <= _credit );
  	hold();
  	_credit -= x;
  	promise( _credit = old_credit - x );
  	promise( _balance = old_balance );
  	promise( invariant() );
  	}
  
  
  bool invariant() {
  	return _credit <= _maxcredit && account::invariant();
  	}
  protected:
  float _maxcredit, _credit;
  float old_credit;
  void hold() { old_credit = _credit; account::hold(); }
  };

slide: Refining the account contract

As a first observation, we may note that the invariant of account immediately follows from the invariant of credit_account. Also, we may easily establish that the pre-condition of withdraw has (implicitly) been weakened, since we are allowed to overdraw the {\em credit_account} by the amount given by credit. Note, however, that this is implied by the virtual definition of

balance()

. To manage the credit given, the methods credit and reduce are supplied. This allows us to leave the methods deposit and withdraw unmodified.

Runtime consistency checking

Debugging is a hopelessly time-consuming and unrewarding activity. Unless the testing process is guided by clearly specified criteria on what to test for, testing in the sense of looking for errors must be considered as ordinary debugging, that is running the system to see what will happen. Client/server contracts, as introduced in section contracts as a method for design, do offer such guidelines in that they enable the programmer to specify precisely the restrictions characterizing the legal states of the object, as well as the conditions that must be satisfied in order for legal state transitions to occur. See slide 4-contracts.

Assertions -- side-effect free

contracts

require -- test on delivery
promise -- test during development

Object invariance -- exceptions

invariant -- verify when needed

Global properties -- requirements

interaction protocols -- formal specification

slide: Runtime consistency checking

The Eiffel language is the first (object-oriented) language in which assertions were explicitly introduced as a means to develop software and to monitor the runtime consistency of a system. Contracts as supported by Eiffel were primarily influenced by notions concerning the construction of correct programs. The unique contribution of [Meyer88] consists of showing that these notions may be employed operationally by specifying the pragmatic meaning of pre- and post-conditions defining the behavior of methods. To use assertions operationally, however, the assertion language must be restricted to side-effect free boolean expressions in the language being used. Combined with a bottom-up approach to development, the notion of contracts gives rise to the following guidelines for testing. Post-conditions and invariance assertions should primarily be checked during development. When sufficient confidence is gained in the reliability of the object definitions, checking these assertions may be omitted in favor of efficiency. However, pre-conditions must be checked when delivering the system to ensure that the user complies with the protocol specified by the contract. When delivering the system, it is a matter of contractual agreement between the deliverer and user whether pre- and/or post-conditions will be enabled. The safest option is to enable them both, since the violation of a pre-condition may be caused by an undetected violated post-condition. In addition, the method of testing for identity transitions may be used to cover higher level invariants, involving multiple objects. To check whether the conditions with respect to complex interaction protocols are satisfied, explicit consistency checks need to be inserted by the programmer. See also section global-invariants.

[] readme course(s) preface I 1 2 II 3 4 III 5 6 7 IV 8 9 10 V 11 12 afterthought(s) appendix reference(s) example(s) resource(s) _

You may not copy or print any of this material without explicit permission of the author or the publisher. In case of other copyright issues, contact the author.