Adaptation rules adapt the pre-post specification of a procedure to contexts where it is called. Such rules are important for practical reasons and necessary for completeness for languages with recursive procedures. Moreover, the specification statement on which refinement calculus is based has as its semantics the predicate transformer representation of an adaptation rule.

A sharp adaptation rule is one that gives the weakest precondition with respect to a given postcondition. A number of rules have been proposed, most unsound or incomplete or non-sharp.

Using refinement algebra, we clarify and extend the applicability of previously proposed sharp rules for total correctness, and show how further rules may be found. Our results justify the semantics of the specification statement used in the Co-op project, and we account for the alternative semantics which is suitable for refinement of conjunctive commands.