Calculating sharp adaptation rules

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. A sharp 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.