4.1 Pre- and Postcondition Specifications

Pre- and postcondition specifications are probably the most common form of component contracts. The precondition expresses an assumption that must be satisfied when calling the component. The postcondition states the promises of what the component guarantees to establish.

Unfortunately, postconditions tend to get very big and unreadable. Because postconditions cannot contain any procedure calls, the semantics of the called procedures has to be expanded into the postcondition. Hence, the approach does not scale well. It is impossible, to specify the state at which external calls are made or the order of calls (Sect. 2.1, Fig. 3). Hence, pre- and postcondition specifications are ill-suited for grey-box component descriptions.