Calculating sharp adaptation rules

Adaptation rules adapt the pre-post specification of a procedure to context s where it is called. Such rules are important for practical reasons and ne cessary for completeness for languages with recursive procedures. A sharp r ule is one that gives the weakest precondition with respect to a given post condition. A number of rules have been proposed, most unsound or incomplete or non-sharp. Using refinement algebra, we clarify and extend the applicab ility of previously proposed sharp rules for total correctness and show how further rules may be found. (C) 2001 Elsevier Science B.V. All rights rese rved.