Slightly different definitions which I found:-
Meyer (Meyer B, Object-Oriented Software Construction 2/e, Upper Saddle River NJ: Prentice-Hall 1997, ch 11, pp331
ff) has two concepts, which I believe are basic to formal software construction;
Correctness. A procedure (method) starts with a precondition, executes, and ensures a post-condition.
Correctness depends on what the method is supposed to do, and you can't have a "correct" method if you don't know what you don't know what you want it to do.
A precondition is something which has to be true before the method starts. If, for example, you are adding an
int value to an
int[] array, there are several preconditions, eg
The array must existThe value added must be in int formatThe place in the array you wish to put the value (the index) is within the bounds of the array. There are several postconditions, ie things which have to be true after you have finished the procedure. In this case they are rather similar to the preconditions.
The array must still existThe bounds of the array haven't changed. These are relatively simple examples; they vary for other examples. Features which must be true before and after and any other time are often called
invariants.
If the preconditions are not fulfilled then there is an error in the calling method. Look at an API class, say java.awt.Color, and look at its last but one constructor, the one with "(int r, int g, int b)" in. Click on the blue writing to get fuller details. The preconditions are declared implicitly by saying "throws some exception or other if . . . ."
The postconditions are also not declared explicitly, but implied. In the case of Color, it is that whichever component you call it on will turn that colour.
A method constitutes a "contract" between whichever class the method is in, and whichever class calls the method. To quote from Meyer (page 341):-
If you promise to call r with pre[conditions] satisfied then, I, in return, promise to deliver a final state in which post[conditions are] satisfied.
Or, in
Java:- If you provide the right arguments to a method, it will provide you with the state of the computer you want.
Meyer points out there are obligations on the calling class, to provide the "right" arguments or preconditions, and the called method, which provides the "right" result or postconditions.
Exceptional events. See
this definition in the Java tutorial. These are usually called exceptions. This is, in Meyer's terminology, what happens when the preconditions are not met. If you are learning Java you will come across exceptions soon, and you ought to be taught about exception handling in Java. If you are not being taught about it, then you already have the Java tutorial link.
Robustness. This is not so much an attribute of a method, but of the whole application. It means the ability to keep running when unexpected events (which can cause Exceptions) occur. The exception handling mechanism quoted above, when used properly, does so.
[ June 13, 2006: Message edited by: Campbell Ritchie ]