design by contract : Java Glossary

A programming technique most commonly used in Eiffel to pepper your code with assertions. These define a contract on each method — the preconditions the caller must guarantee, and the postconditions the callee guarantees.

One should not write a class without a specification — a contract. The contract lists the internal consistency conditions that the class will maintain (the invariant) and, for each operation, the correctness conditions that are the responsibility of the client (the precondition) and those which the operation promises to establish in return (the postcondition).
Writing a class without its contract would be similar to producing an engineering component (electrical circuit, VLSI (Very Large Scale Integration) chip, bridge, engine…) without a spec. No professional engineer would even consider the idea.
~ Bertrand Meyer (born: 1950 age: 61), creator of design by contract and the Eiffel language. Description of Design By Contract

recommend book⇒Object-Oriented Software Construction

by:

Bertrand Beyer

978-0-13-629155-8

paperback

(born: 1950 age: 61)

978-0-13-629049-0

hardcover

publisher:

Prentice Hall

published:

2000-03-21

This is the classic text on object-oriented programming. This is the best-written computer textbook on any subject I have yet encountered. If you ever plan to write a book, look at this to see how it should be done. He uses the Eiffel language for his examples. This could be confusing if you don’t already have little Java under your belt. This is not a book on coding, but rather on the general object-oriented principles behind the languages.

Greyed out stores probably do not have the item in stock

recommend book⇒Design By Contract

by:

Bertrand Beyer

978-0-13-088921-8

paperback

(born: 1950 age: 61)

publisher:

Prentice Hall

published:

2001-06-15

Difficult to find. Out of print.

Greyed out stores probably do not have the item in stock

There are class invariants, which are conditions about overall class consistency that must be true any time any method completes. The official definition of a class invariant is an assertion which must be satisfied on creation of every instance of a class, and preserved by every exported (public) routine of the class, so that it will be satisfied by all instances of the class whenever they are externally observable. (I’m not sure how they handle multithreading.)

You can also have invariants on the non-public parts. Only the invariants involving purely public features (methods and variables) are in themselves public.

Eiffel lets you talk about both the old and new values of variables in your assertions. In Eiffel, these conditions are a formal part of the language and may optionally be checked at run time. The beautiful part is that the contract is inherited. A subclass may have a tighter, but not looser contract. None of the Java assertion schemes can do this.

Speaking more precisely, in a subclass, preconditions for an inherited method can only be equal to or weaker than that of the original precondition; and postconditions for an inherited method can only be equal to or stronger than that of the original postcondition. In other words, the precondition cannot be modified in the subclass to require more from the client than what is required in the parent class.

Another form of assertion is called the loop invariant, something that must be true each time through a loop. These assertions are not considered part of a method’s or class’s contract with the rest of the world, however. Similarly, there are assertions to ensure a loop eventually terminates.

In Java there are various ways of kludging design by contract and assertions including: iContract, JMSAssert, jContractor, Handshake, Jass, JML and JPP. Starting withJava version 1.4, Java has a weak built-in assertions mechanism. It is a far cry from design by contract.

Learning More

Oracle RFE number 4449383 : JSR to add Design By Contract to Java

@NotNull
@Nullable
assertions
c2 wiki
ContractualJ
Dr. Dobbs interview with Bertrand Meyer
Eiffel
Eiffel DBC definition
JML

	You can get the freshest copy of this page from:	or possibly from your local J: drive (Java virtual drive/mindprod.com website mirror)
	http://mindprod.com/jgloss/designbycontract.html	J:\mindprod\jgloss\designbycontract.html
	Please email your feedback for publication, letters to the editor, errors, omissions, typos, formatting errors, ambiguities, unclear wording, broken/redirected link reports, suggestions to improve this page or comments to Roedy Green : If you want your message kept confidential, not considered for posting, please explicitly specify that.
	Canadian Mind Products
	mindprod.com IP:[65.110.21.43]
view Blog	Your face IP:[38.107.179.210]
Feedback	You are visitor number 14,101.