Design By Contract

By Gavin Scott, 96150351
For Renaat Verbruggen

Masters in Computer Applications
Dublin City University

Abstract

One of the key programming styles supported by the Eiffel programming language is Design by Contract (DBC). Bertrand Meyer, Eiffel's main designer, states that DBC (or some equivalent idiom) is a basic requirement for reliable, robust, reusable components.

This paper has three objectives: introduce and justify the need for DBC; explain the programming implications and details of DBC; examine the possibility of using the DBC idiom in C++. The sample languages used will be C++ and Eiffel.


Contents

Citation
1 Introduction
1.1 What is Design by Contract?
1.1.1 Reliability
1.1.2 Robustness
1.1.3 Reusability
1.2 Why have Design by Contract?
1.2.1 Maintenance
1.2.2 Win-Win Programming Relationships
1.2.3 Self-Documenting
1.2.4 Testing
2 Design by Contract in Eiffel
2.1 Using Assertions for Reliability
2.1.1 Preconditions and Postconditions
2.1.1.1 Postconditions - an observation
2.1.1.2 Preconditions - some cautionary words
2.1.2 Class Invariants
2.1.2.1 Class Correctness
2.1.3 Loop Invariants and Variants
2.1.4 Check Assertions
2.2 Using Exception Handling for Robustness
2.2.1 Exception Cases
2.2.2 Failure Approaches
2.2.2.1 Retrying
2.2.2.2 Failing
2.2.3 Failure Recording
2.3 Reuse through Inheritance
2.3.1 Rules and Regulations
2.3.1.1 Class Invariants
2.3.1.2 Preconditions and Postconditions
2.4 Design by Contract Considerations
2.4.1 Unexpected Invariant Failures
2.4.2 Runtime Assertion Monitoring
2.4.3 Limits of Logical Expression
2.4.4 Assertions and User Interfaces
3 Design by Contract in C++
3.1 Inheritance in C++
3.2 Exceptions in C++
3.3 Assertions in C++
3.3.1 Placing Assertions in C++
3.3.2 Checking Assertions in C++
3.3.3 Dealing with Violated Assertions in C++
4 Conclusions
5 Annotated References
6 Additional Reading

Citation

Most of the work contained in Section 1 and Section 2 is derived from material found in [4,5] and is assumed to reference same. Items requiring further detail or items from other sources are explicitly referenced. Direct quotations are also referenced.

1 Introduction

1.1 What is Design by Contract?

1.1.1 Reliability

Program testing, formal methods, code inspections, etc. all strive to ensure that a program is correct. (The term program will be used to refer to libraries as well). The lone statement, "a program is correct", has no meaning. A program can only be correct with respect to a specification.

Under DBC, this specification is expressed as a contract between a class and its client code. It expresses what the class requires of its calling client - a precondition - and what the class guarantees to it calling code upon return - a postcondition. E.g.

// precondition x > 0
void make_bigger_than_five (int& x)
{
    x += 10;
}
// postcondition: x > 5
// We could say x > 10 but x > 5 is also true

Pre and post conditions are by no means the full extent of DBC. If they were, DBC would add little to the work of Hoare et al. [3]. Pre and post conditions, or more generally, assertions are DBC's reliability mechanism. They help guarantee that software performs according to its specification (or contract).

NOTE: The term client will be used to refer to the client code/client programmer. The term supplier will be used to refer to the class/class implementor of the class called by the client.

1.1.2 Robustness

Exception handling is DBC's robustness mechanism. It provides a well defined means of handling cases not in the contract, i.e. when an assertion fails.

1.1.3 Reusability

Reusability comes about in two different ways under DBC:

1.2 Why have Design by Contract?

DBC makes significant contributions to code reliability, robustness and reusability as outlined above and elaborated upon below. In addition to these, DBC offers the following benefits:

1.2.1 Maintenance

Eiffel provides assertions, which allows programmers to explicitly record the expected state of scoped data. Code modifications often introduce bugs. Assertions help alleviate this problem in two ways:

Assertions are not exclusive to Eiffel. C supports assertions in a limited manner and may extend its support through use of the #define preprocessor directive. Maguire examines such extensions in detail in [1].

1.2.2 Win-Win Programming Relationships

The benefit to the client is clear:

The benefits to the supplier are the expected counterpart:

This last point is very important. Complexity creeps into software if programmers are unsure how to handle error conditions properly. E.g.

double sqrt (double num)
{
    if (num < 0)
    {
         // We don't support complex numbers - just check the return type
         // We can:
         // 1) set num = -num and continue
         // 2) throw an exception
         // 3) return (-1);
         // 4) exit (1);
         // 5) prompt the user for a new value
         // 6) ...
    }
    ...
}

With DBC we state as a precondition that num >= 0. The supplier need not check this, nor should he deal with second guessing the client's preferred error handling approach. Meyer is quite explicit about this. He formulates this in his Non-Redundancy Principle [4.1]:

Non-Redundancy Principle

Under no circumstance shall the body of a routine ever test for the routine's precondition.

Meyer believes that you can "guarantee more by checking less" [4.1]. This notion seems counter intuitive. However, while a defensive style of programming, as illustrated above, would seem to make a routine more robust, it does not make the overall software system robust. Suppliers are second-guessing client's error handling requirements rather than letting clients decide for themselves. This increases supplier code complexity and reduces its reusability.

1.2.3 Self-Documenting

Apart from the commenting aspect mentioned in Section 1.2.1, we also have the benefit that code is self-documenting. In C++, an API is published in the form of a header file. Eiffel has no such notion. So how does an Eiffel class publish its interface? It does so by using the short and flat-short form.

These views of a class are generated from an Eiffel development tool. The short form of a class consists of those elements of the class that are visible to a client, excluding any inherited elements. E.g.

class Dig
{
public:
    Dig () {m_x = 0;};
    ~Dig ();
    void out (void);
private:
    void helper (void);
    int m_x;
};
------>
convert
to
short
form
------>
// "interface" added to
// make syntax invalid,
// though the semantics
// remain clear.
class interface Dig
{
public:
    Dig ();
    ~Dig ();
    void out (void);
}

The flat form of a class contains all the elements of a class, both inherited and non. It also contains implementation details (in C++ this would be protected and private members). As with the normal view of an Eiffel class, it is not fit for client consumption.

Hence, there is the flat-short form. This consists of all element available to a client of a class, irrespective of whether the supplier inherited them or added them himself.

Both the short form and the flat-short form contain pre and post conditions. Hence all necessary details of the class may be published without providing the client with any implementation details.

1.2.4 Testing

As Eiffel assertions (preconditions, postconditions and other assertion types that shall follow) are executable, and their violations detectable, the testing process is greatly eased.

For a supplier, it allows test suites to be executed on a class with implicit checking of the expected results, given that the expected results are stated assertions. Test case failure will manifest itself in the form of an exception being thrown to the client program (test harness).

For a client, it allows quicker identification of an error's source, using the following rules of thumb:

In the real world, there are situations where these rules are not quite so hard and fast. There are issues of performance to consider and in the case of concurrent environment, the entire semantics of pre and postconditions change. Concurrency is beyond the scope of this paper but is discussed in [4.6]. Matters of efficiency are covered later in Section 2.4.2.

2 Design by Contract in Eiffel

There are three aspects of DBC covered in this paper:

Each of these is examined below, within the context of the Eiffel programming language.

2.1 Using Assertions for Reliability

Pre and postconditions introduced above are but two of Eiffel's assertion types. Later, the remaining Eiffel assertion types will be covered, namely:

2.1.1 Preconditions and Postconditions

Eiffel's support for pre and postconditions is best seen through an example:

put (x: INTEGER) is
  -- Add x to the list of positive numbers
  require
    positive: x > 0
    not_full: not full
  do
    -- Body goes here
  ensure
    not_empty: not empty
    got_bigger: count = old count + 1
  end

The precondition or require clause is the conjunction of the positive and not_full subclauses. Likewise, the postcondition or ensure clause is the conjunction of the not_empty and got_bigger subclauses.

full, empty and class are all class attributes. not is the negation operator. old is an operator with no equivalent in C++. It is supported in VDM and other languages. In the example above old count refers to the value of count before put was called.

2.1.1.1 Postconditions - an observation

At times, postconditions may seem redundant. Consider

empty: BOOLEAN is
  -- Is the list empty
  do
    Result := (count = 0)
  ensure
    empty_definition: Result = (count = 0)
  end

Despite the postcondition's apparent redundancy, it should not be omitted. Above there is a clear similarity between the syntax of the body and the ensure clause. This is rarely the case. Even with the above example, the body could be changed to:

    if count = 0 then
      Result := True
    else
      Result := False

The syntactic similarity is immediately lost, however, the semantic link still remains.

2.1.1.2 Preconditions - some cautionary words

Meyer states some important principles that preconditions must conform to

  1. Preconditions must be justifiable solely in terms of the specification
    It is not uncommon for implementation decisions to affect client code. Suppose a supplier decides to implement an unbounded stack with an array. What will happen when the array becomes full? In either case, there is an unacceptable situation arising out of violating this principle.
  2. Features appearing a routine's preconditions must be available to the clients that the routine is available to
    Suppose, in C++, we implement a bounded stack and have as a precondition of a public function put that the stack size is less than the maximum. This seems perfectly reasonable. What if the size is a private member with no corresponding accessor function? The client has no way of checking for the precondition. This is clearly unacceptable.
    Similar notions of visibility for postconditions need not apply, as postconditions may contain implementation details.

2.1.2 Class Invariants

Pre and post conditions are concerned with the correctness of individual class members. However, what of the class as a whole?

Consider a class implementing a list of sorted numbers. A given member function may increase, read or decrease the sorted list. The one constant throughout is that the list remains sorted. This is its invariant. The class invariant captures the semantic property of a class as a whole.

Eiffel supports a class invariant as part of a class definition. E.g.

class MYNUMBERS

feature -- Checking

  empty: BOOLEAN is
    do
      Result := (count = 0)
    end

invariant
  count_bounded_below: 0 <= count
  count_bounded_above: count <= max

end

As with pre and post conditions, the invariant clause is taken as the conjunction of its constituent subclauses.

2.1.2.1 Class Correctness

A class is considered correct if:

where valid denotes arguments satisfying the appropriate preconditions.

The class invariant is the business of the supplier. The class invariant must be guaranteed as a result of the constructor and all exported member functions. All access to the class will be provided through exported functions, thus the client should not be able to cause a class invariant violation.

If a class invariant is violated, it suggests an error in supplier code. This will be treated as an assertion violation similar to that of a pre or post condition violation. An unusual assertion violation situation is examined in Section 2.4.1.

2.1.3 Loop Invariants and Variants

Eiffel supports the notion of a loop invariant and variant. These notions are not new and thus are not covered in any detail bar the brief explanation below.

A loop may be seen as a finite set of repeated steps executed to achieve a goal. Given that the loop is finite, it must make an effort to terminate, e.g. decrement a loop counter. The loop variant is an expression that must decrease with each iteration of the loop - if it does not the loop may go on infinitely. In Eiffel, a non decreasing loop variant is seen as an assertion violation.

Stated above, the steps of a loop must achieve a goal. Upon each iteration of the loop, a sub-goal must be achieved. As the loop continues, the sub-goal "grows", eventually becoming the loop goal. This sub-goal is the loop invariant. For example, the invariant of the selection sort is that all elements of the array, up to the current element, are in sorted order. In Eiffel, a loop invariant violation is also considered an assertion violation.

2.1.4 Check Assertions

Eiffel supports one final assertion type - the check assertion. This allows programmers to add assertions to routine bodies to ensure assumed conditions. E.g.

dig (x: INTEGER) is
  do
    x := x + 1
    check
      x > old x
    end
    -- rest of body here
  end

While the above may seem trivial, it detects the case of x+1 becoming negative due to arithmetic overflow, though the Eiffel INTEGER class should pick this up.

2.2 Using Exception Handling for Robustness

Robustness in Eiffel is provided via its exception handling mechanism. Exception handling is not provided as a flow control mechanism but as a failure reporting mechanism. That said, exception will alter the flow of control.

There is a subtle but direct connection between Eiffel exceptions and software failures:

NOTE: In C we could choose not to check a return value, even if it denoted an error condition, with potentially hazardous results. Eiffel does not allow failed calls to go unchecked.

2.2.1 Exception Cases

Meyer [4.2] lists 11 possible exception cases that may occur. They are listed below:

  1. Invoking on a NULL pointer.
  2. Assigning from a NULL pointer.
  3. Executing an operation that causes an operating system/hardware abnormal condition.
  4. Calling a routine that fails.
  5. Detecting a precondition violation.
  6. Detecting a postcondition violation.
  7. Detecting a class invariant violation.
  8. Detecting a loop invariant violation.
  9. Detecting a non-decreasing loop variant.
  10. Detecting a check assertion violation.
  11. Executing an instruction meant to trigger an exception.

It is this list, in particular items 5 through 10, that provides the link between DBC's notion of reliability and DBC's notion of robustness. In Section 2.1, when dealing with reliability, the concern was with dealing with situations which satisfied the assertions. In Section 1.2.2, it was seen that dealing with situations which didn't satisfy the assertions added unnecessary complexity.

Now that those situations have been explicitly enumerated, a strategy is required for dealing with them. This is the topic of the next section.

2.2.2 Failure Approaches

In the event of a routine detecting an exception, it has only two options. It may:

Eiffel provides support for such a mechanism via its rescue clause. A shell routine is illustrated below:

routine is
  require
    -- precondition
  local
    -- declare local variables
  do
    -- body
  ensure
    -- postcondition
  rescue
    -- rescue clause
  end

The local block is included for completeness - it is of no interest to the discussion. The rescue clause may contain the retry instruction. If encountered, this causes the body to routine body to be retried. If not, the routine fails, throwing an exception to its client.

2.2.2.1 Retrying

If a routine decides to retry, it must first restore the class invariant and precondition. It must also effect a change in the failing component of the body, either by altering its environment or by ensuring an alternate routine will be called. This is the responsibility of the rescue clause. However, the rescue clause should make no attempt to implement the function, only to perform restoration and alter the calling environment.

2.2.2.2 Failing

If a routine decides to fail, it must restore the class invariant and report the failure to the client. As with retrying, it is the responsibility of the rescue clause to restore the class invariant. Eiffel will then report the failure to the client when no retry instruction is encountered.

2.2.3 Failure Recording

In the event of a routine failure, especially in a test environment, it is of interest to see the set of exceptions that resulted in the failure. In a debugger, this would be provided by a stack trace. In Eiffel, an exception history table fulfills this role.

The entries in the table are in the order of exception occurrence, i.e. the reverse order of routine invocation. An entry (row) in the table consist of:

The exception history table proves to be a powerful tool when debugging code. Eiffel also allows programmers access exception information at a similar level of detail through use of its EXCEPTIONS class. For example, a client may determine the original exception type in the current chain of exceptions. Details of this class are best understood by examining its short form, which is detailed in [4.2].

2.3 Reuse through Inheritance

Given that classes (and their routines) are all bound by contract, it is no surprise that derived classes are also bound by contract. What is of interest, however, is the relationship between base class' contracts and derived class' contracts.

Dynamic binding allows a client to call upon a derived class when it believed it was calling upon a base class. This is the nature of inheritance in Eiffel. Similar behaviour occurs in C++ when dealing with base class pointers.

Let us examine an example. The base class is called B and the derived class, D. For simplicity there is only one member function of each class, called f. The respective pre and postconditions for f are pre-b, post-b, pre-d and post-d. The respective class invariants are inv-b and inv-d.

A client of D, thinking it is calling upon B, will attempt to satisfy pre-b. It will expect the class to have the semantic property as expressed in inv-b. Finally, it will expect a result satisfying post-b. Instead what it will find is that it needs to satisfy pre-d, to use a class with semantic property inv-d, which results in satisfying post-d.

There is potential for problems!

2.3.1 Rules and Regulations

2.3.1.1 Class Invariants

We need one rule to ensure that the invariant is maintained. This is the Parents' Invariant Rule [4.4]. Eiffel automatically implements it.

Parents' Invariant Rule

The invariants of all the parents of a class apply to the class itself.

Thus, all ancestor class invariants are logically ANDed together with the derived class invariant to form its true invariant. In this way the semantic properties of the ancestor classes are maintained.

Though, x and x is logically equivalent to x, it is less efficient. Thus, when dealing with class invariants, a derived class should not repeat the invariant of its ancestor class(es).

2.3.1.2 Preconditions and Postconditions

The example given in Section 2.3 of classes B and D lead to the general observation Meyer states as the Assertion Redeclaration Rule (1) [4.4]:

Assertion Redeclaration Rule (1)

A routine redeclaration may only replace the original precondition by one equal or weaker, and the original postcondition by one equal or stronger.

This thus allows a client satisfy pre-b and expect post-b even when class D is being invoked upon.

However, Eiffel does not trust the programmer to ensure that the new precondition is equal to or weaker than the old one, nor does it trust the programmer to ensure that the new postcondition is equal to or stronger than the old one.

Observe that precondition x or y is equal to or weaker than precondition x. Also observe that postcondition z and w is equal to or stronger than postcondition z. I.e. ORing a precondition will make it more general, i.e. weaker and ANDing a postcondition will make it more specific, i.e. stronger.

This is what we required as stated in the Assertion Redeclaration Rule 1. Eiffel supports this notion using an extended syntax for the require and ensure clauses. These clauses respectively ORed and ANDed are require else and ensure then clauses. The Assertion Redeclaration Rule is thus extended [4.4]:
Assertion Redeclaration Rule (2)

In the redeclared version of a routine, it is not permitted to use a require or ensure clause. Instead, you may:
  • Use a clause introduced by require else, to be ORed with the original precondition.
  • Use a clause introduced by ensure then, to be ANDed with the original postcondition.
In the absence of such a clause, the original assertion is retained.

2.4 Design by Contract Considerations

The outline of DBC above is by no means complete. However, it does cover most of the main elements of the topic. Before finished with DBC in Eiffel, it is worth highlighting a few issues, which are expanded upon further in [4.1].

2.4.1 Unexpected Invariant Failures

It is possible that between invocations on an object, its invariant will fail. Suppose we have a linked list of objects. A C++ invariant for a connected object might be that next->prev == this. This could be violated by altering a different object, the one referred to by next. Such an alteration could take place unbeknownst to the original object. Research in this area is ongoing [4.1].

2.4.2 Runtime Assertion Monitoring

Eiffel allows for different levels of assertion monitoring at runtime. They are detailed in [4.1]. Each level encompasses all the previous levels. So, when the final level of checking is turned on, all assertions are checked.

This can have an undesired overhead. Meyer recommends such levels of monitoring during testing and development. Despite its impact on efficiency, Meyer makes a fair, and often overlooked point, "If the software does not perform its function, the rest [including efficiency] is useless." [4.1]

Meyer concedes that certain preconditions may be essentially uncheckable [4.5]. E.g. inverting a matrix should state that the matrix is invertable as a precondition. However calculating this precondition is virtually as expensive as computing the inverse. He suggests that in such an event the violation should be reported as early as possible.

2.4.3 Limits of Logical Expression

Neither C++ nor Eiffel supports first order predicate calculus. Making universal quantifications and existential qualifications thus appears impossible. However, functions may be written to test such boolean expressions. Such functions must not alter the structure of the class nor alter the routine's arguments.

Mutual infinite recursion in assertion checking is avoided automatically in Eiffel. It is easy to see how it may occur. E.g. for some collection class, Full would list Result = True implies not Empty in its ensure clause. Empty would list Result = True implies not Full in its ensure clause. Each would infinitely recurse the other. Eiffel guards against this by stating that assertion evaluation should not take place in one routine when it is called as part of another's assertion evaluation.

2.4.4 Assertions and User Interfaces

Assertions are not used to validate user input. This should be performed by conventional control structures (if then else). These control structures may be contained in routines. Before handing over control to the supplier's processing routines, the supplier's preconditions must be satisfied. That is to say, the input validation routines must guarantee a state at least as strict as that defined by the supplier's preconditions.

3 Design by Contract in C++

Given the strong justification for DBC in Section 1.2, it seems a pity not to use it, or some of its principles in C++. C++ provides no direct support for DBC and this was one of Meyer's reasons for inventing Eiffel over using C++[2]. The absence of garbage collection in C++ was another motivating factor. This somewhat limits the extent to which we can implement DBC in C++.

An article of this size can not hope to provide a solution to the problem of using DBC in C++. However, it can highlight some of the programming principles and supporting class requirements that would go a long way towards achieving DBC in C++.

The previous sections concentrated on three aspects of Eiffel that were connected to DBC:

I shall examine these items in reverse order, based on the ease at which C++ supports such notions.

3.1 Inheritance in C++

There are three Eiffel requirements that must be satisfied in the case of a derived class:

These may be easily programmed by the supplier of a derived class. For ease of programming, the invariant and routine pre and postconditions would be virtual functions and would stick to an easily used naming convention. E.g.

#include "base.h"
class Derived : public Base
{
public:
    virtual bool func1_pre (...) const;
    virtual bool func1_post (...) const;

    virtual bool check_func1_pre (...) const
    {
        return Base::check_func1_pre(...) && func1_pre(...);
    };
    virtual bool check_func1_post (...) const
    {
        return Base::check_func1_post(...) && func1_post(...);
    };
    ...
protected:
    virtual bool invariant (void) const;
    virtual bool check_invariant (void) const
    {
        return Base::check_invariant() && invariant();
    };
    ...
};

This solution is not the most elegant, however, it should work. It could be made easier on the eye by the simple use of macros. These macros would come supplied part of a DBC helper header file and library, referred to below as dbc.h.

Slightly different approaches are required in the use of friend functions. These are not examined here. Nor is multiple inheritance, nor inheritance other than public inheritance.

3.2 Exceptions in C++

Though Meyer is against the idea of an exception object [4.2], the notion is suitable for implementing DBC from existing C++ language constructs alone. Such an object, provided by dbc.h would allow for the collection of exception information similar to that of the exception history table of Section 2.2.3. It could also be queried using routines similar to those mentioned in the same section.

Exceptions in C++ are not too dissimilar to their counterpart in Eiffel, with the following (pardon the pun) exceptions:

Thus, some variation from the Eiffel coding style may be required to support DBC error handling in C++.

3.3 Assertions in C++

Three main problems must be addressed when implementing Eiffel like assertions in C++

  1. Where should they be placed in the code?
  2. How do we check them?
  3. What do we do if an assertion is violated?

3.3.1 Placing Assertions in C++

Assertion placement would vary depending on the requirements of client visibility and derived class visibility. As was seen above in Section 3.1, the preconditions would double the size of the API. This is not a desirable solution and an alternative should be investigated. Likewise for postconditions and other assertions.

3.3.2 Checking Assertions in C++

When checking assertions, we wish to avoid the mutual recursion problem described in Section 2.4.3. We could attempt may do so by associating an (untriggered) exception object with an association check - this requires an extra function parameter to all assertion checks. This object would have a flag stating whether assertions were to be checked, based on whether or not we were dealing with a "nested assertion".

We also require that the different levels of assertion checking be implemented. This could either be at run time, i.e. dynamic if (level < x) checks, or at compile time, i.e. #ifdef LEVEL_X. The costs and benefits of both approaches would need to be weighted up.

3.3.3 Dealing with Violated Assertions in C++

Violated assertions would result in an exception object being thrown. This object would contain information regarding the current object, class, routine, exception type and effect, i.e. the information required for the exception history table. The object would be the this pointer. The class name would be accessible through some const accessor function to static class data. This function would be consistently named in all classes. The routine name would be picked up through some local variable containing the routine name. This would be declared in each routine. The exception would be determined by the exception originator. The behaviour of the resuce in Section 3.2 would need to update the effect field.

4 Conclusions

Design by Contract is a powerful software engineering technique. It promises reliability, robustness and reuse. Eiffel has complete support for the technique, while C++ has no explicit support. However, C++ may support elements of DBC relatively easily. Full DBC in C++ requires the definition of support classes and much further investigation.

5 Annotated References

[1] Steve Maguire, Writing Solid Code, 1993,
Microsoft Press, ISBN 1-55615-551-4
This book is an excellent guide to writing solid programs in C. OO variations on themes contained therein would be well worth exploring. However, the only material directly influencing this paper is: Chapter 2, Assert Yourself, pp. 13-44.
[2] Bertrand Meyer, "Eiffel vs. C++. Eiffel - One language designer's view", 1989,
http://www.progsoc.uts.edu.au/~geldridg/bmefcpp.htm
This is one of many URLs containing Meyer's 1989-06-04 posting to newsgroups comp.lang.eiffel and comp.lang.c++ stating why (he feels) Eiffel is better than C++. Some of the criticisms of C++ are now no longer valid as C++ has changed quite a bit in the last nine years. Thus, only the currently valid aspects of the article are referred to.
[3] Bertrand Meyer, "Eiffel's Design by Contract: Predecessors and Original Contributions", 1997-03-12,
URL http://www.progsoc.uts.edu.au/~geldridg/eiffel/liberty/v1/n1/bm/bmdbc.html
Meyer describes the influences behind Eiffel and the significant contributions he feels Eiffel has made.
[4] Bertrand Meyer, Object-Oriented Software Construction, 2nd ed., 1997,
Prentice Hall, ISBN 0-13-629155-4
For a summary see URL http://www.eiffel.com/doc/oosc.html
This, very long text, is Meyer's complete guide to OO with the sample language used being Eiffel. The following chapters/sections are relevant to DBC
  1. Chapter 11, Design by Contract: Building Reliable Software, pp. 331-410,
    A detailed guide to DBC's necessity and use
  2. Chapter 12, When the Contract is Broken: Exception Handling, pp. 411-438,
    Using exception handling to deal with contracts that are broken
  3. Chapter 15, Multiple Inheritance, Section 15.3, Flattening the Structure, pp.541-543,
    An explanation of the notions of the flat form and flat-short form
  4. Chapter 16, Inheritance Techniques, Section 16.1, Inheritance and Assertions, pp. 569-580,
    DBC's role with respect to inheritance
  5. Chapter 23, Principles of Class Design, Section 23.6, Dealing with Abnormal Cases, pp. 797-801,
    The nature of exceptions within the context of proper API design
  6. Chapter 30, Concurrency, Distribution, Client-Server and the Internet, Section 30.7, Wait Conditions, pp. 990-998,
    The difficulties and solutions to using DBC in a concurrent programming environment
[5] Tower Technology Corporation, "Getting Started with TowerEiffel", 1996,
URL http://www.cs.cf.ac.uk/TowerEiffel/tut.htm Tower Technology's TowerEiffel documentation describes the TowerEiffel development environment, the Eiffel language and its concepts. The following chapters/sections are relevant to DBC
  1. Chapter 3, Introduction to OO Concepts, Section 3.5, Design by Contract
  2. Chapter 4, Introduction to Eiffel Programming Constructs, Section 4.7, Assertions
  3. Chapter 5, Eiffel Engineering, Section 5.5, Design by Contract
  4. Chapter 5, Eiffel Engineering, Section 5.7, The Many Faces of a Class: Views, Contracts, and Types

6 Additional Reading

If the above only served to whet you appetite for Eiffel, DBC and C++, then check out the articles below. These were not used in this article.

[6] Ken Garlington, "Critique of 'Put it in the contract: The lessons of Ariane'", 1997-08-03,
URL http://www.progsoc.uts.edu.au/~geldridg/eiffel/ariane/index.html
[7] Interactive Software Engineering, "Why your next project should use Eiffel",
URL http://www.eiffel.com/eiffel/why_eiffel.html
[8] Paul Johnson, "Why Eiffel is better than C++ (for big projects)",
URL http://www.progsoc.uts.edu.au/~geldridg/eiffel/liberty/johnson-paul/why-eiffel/index.html
[9] Ian Joyner, "C++??: A Critique of C++", 3rd ed., 1996-10,
URL http://www.progsoc.uts.edu.au/~geldridg/cpp/cppcv3.html

NOTE: Given the "dynamic" nature of the Internet, it is possible that the URLs listed above will become invalid. This is not to say that the material will not be available elsewhere. http://www.progsoc.uts.edu.au/~geldridg/ was used extensively as it was the best site found. The Eiffel home page, http://www.eiffel.com, contains duplicates of or alternate links to many of the above articles, if required.