2.2 Proof Tasks and Code Reuse  

Components can be reused if they bridge the gap between the clients stated pre- and postcondition. Proof tasks formalize this relation; their exact nature determines form and effects of reuse.

The most efficient form of reuse takes place if the gap between the client's offer (the precondition) and his wishes (the postcondition) is bridged completely. A component c can be plugged in and thus close the gap if it has a weaker pre- and a stronger postcondition than the client requires in his query q. This ideal situation is usually formalized in the following condition, or proof task:

$$(\mbox{\em pre\/}_q\Rightarrow\mbox{\em pre\/}_c) \wedge (\mbox{\em post\/}_c\Rightarrow\mbox{\em post\/}_q)$$ (1)

This proof task is however not adequate if q is a partial function but not c. If we want c to match q even if its results on the extended domain do not fit the original query, we must restrict the implication between the postconditions on the domain given by $\mbox{\em pre\/}_q$. We thus work with proof tasks of the form

$$(\mbox{\em pre\/}_q\Rightarrow\mbox{\em pre\/}_c) \wedge (\m... ...\/}_q \wedge \mbox{\em post\/}_c\Rightarrow\mbox{\em post\/}_q)$$ (2)

This so-called plug-in compatibility supports safe reuse. The retrieved components may be considered as black boxes and may be reused ``as is'', without further proviso or modification.

Another, weaker form of the proof tasks emphasizes the clients postcondition and retrieves all components which satisfy it at least on their own domain:

$$\mbox{\em pre\/}_c \wedge \mbox{\em post\/}_c\Rightarrow\mbox{\em post\/}_q$$ (3)

Generally, code reuse based on this conditional compatibility is potentially unsafe because the client has to satisfy the open obligation $\mbox{\em pre\/}_c$.In a formal framework, however, (3) is justified because it describes a normal refinement step: the client trades his own open contract $\mbox{\em post\/}_q$ against the usually simpler $\mbox{\em pre\/}_c$ by re-using c. Note that (3) is also more efficient to check, as only one implication has to be proven.

To increase the recall, conditional compatibility can be relaxed further by again taking the client's precondition into account. But in contrast to (2) it is now added to the premise:

$$\mbox{\em pre\/}_c\wedge\mbox{\em pre\/}_q\wedge\mbox{\em post\/}_c\Rightarrow\mbox{\em post\/}_q$$ (4)

Hence, partial compatibility retrieves all components which do ``the right thing'' at least on a domain restricted by $\mbox{\em pre\/}_c\wedge\mbox{\em pre\/}_q$.By varying $\mbox{\em pre\/}_q$, clients can control recall and granularity of reuse. The stronger it is, the more components are retrieved but the smalller is their respective benefit, simply because $\mbox{\em pre\/}_q$ acts as an additional open obligation.