Keywords: current

Next: 1.5.1.3 Examples Up: 1.5.1 The Design Recipe Previous: 1.5.1.1 Data Analysis and

### 1.5.1.2 Contract and Header

Since Java is a strongly typed language, it mandates the declaration of a type ``contract'' for each method in a class. This contract simpy specifies the types of the method arguments and the type of the result. On the other hand, Java does not mandate the inclusion of a contract stating (i) what if any additional preconditions (beyond the the types of the arguments) must hold for the method to be called, and (ii) what relationship exists between the inputs and output of a method. The latter is often called a postcondition or output condition for the method. Well-written Java programs include a ``behavioral contract'' for every method, specifying any additional constraints on the inputs and what value (as a function of the inputs) the method returns.

For methods defined over composite types (abstract classes at the top of composite class hierarchies), the behavioral contract should be attached as a comment to the abstract method definition in the top class.