Abstract
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.
Original language | English |
---|---|
Pages (from-to) | 201-208 |
Number of pages | 8 |
Journal | Information Processing Letters |
Volume | 77 |
Issue number | 2-4 |
DOIs | |
State | Published - 28 Feb 2001 |