Refining contracts

intro, methods, objects, contracts, formal, summary, Q/A, literature

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$ )
weaken pre-condition
post( $m_C$ ) $<=$ post( $m_P$ )
strengthen post-condition

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.