Calculating sharp adaptation rules

Research output: Contribution to journalArticlepeer-review

16 Scopus citations

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 languageEnglish
Pages (from-to)201-208
Number of pages8
JournalInformation Processing Letters
Volume77
Issue number2-4
DOIs
StatePublished - 28 Feb 2001

Fingerprint

Dive into the research topics of 'Calculating sharp adaptation rules'. Together they form a unique fingerprint.

Cite this