Software components whose behavior is not completely specified cannot be trusted. This should be obvious to anyone in the software industry. And yet the majority of systems out there are made up of parts most of which are only (at best) partially specified, usually by natural language comments. This is not enough. We need to be more complete, and we need to be more precise.
Components based on object-oriented abstraction lend themselves perfectly to a successful marriage with elements coming from the research on formal specifikation. Objects offer their services through operations that can be furnished with pre- and postconditions expressed as simple boolean expressions involving the supplied arguments, if any, and the current state of the object. The precondition stipulates what must be fulfilled before a client is allowed to invoke the operation, and the postcondition specifies what is guaranteed to be fulfilled directly after the call, provided that the precondition was true at the time of invocation.
If a precondition is false at the time of the call, this constitutes an error on behalf of the client, and the call is invalid. If the corresponding postcondition is false directly after a valid call, the error is on the supplier side. Besides pre- and postconditions, which specify the behavior of individual operations, a class invariant can be added which specifies general conditions that must always be true before and after a call to any operation. Invariants tell you something about the inherent properties of the whole abstraction, as opposed to the behaviors of individual operations.
Using formal specification in this way gives us double advantages:
contrary to human language, the assertions are precise, leaving no doubt about what is really meant
the specifications can be used as basis for a disciplined exception handling mechansim and for automatic assertion checking at run-time, yielding a very powerful debugging aid
Design by contract was invented by Bertrand Meyer, see his article "Building bug-free O-O Software" for an overview, and chapter eleven of his standard reference book on object-oriented concepts, "Object-Oriented Software Construction", 2nd ed., Prentice Hall 1997, for a thorough explanation. For an introductory book, see "Design by Contract by Example" by James McKim and Richard Mitchell, Addison Wesley 2001.
See also pp. 205-212 in "Seamless Object-Oriented Software Architecture" and a presentation at the web site of Eiffel Software, part 1 and part 2.