Unifying wp and wlp

Carroll Morgan*, Annabelle McIver

*Corresponding author for this work

Research output: Contribution to journalArticle

7 Citations (Scopus)

Abstract

Boolean-valued predicates over a state space are isomorphic to its characteristic functions into {0, 1}. Enlarging that range to {-1, 0, 1} allows the definition of extended predicates whose associated transformers generalise the conventional wp and wlp. The correspondingly extended healthiness conditions include the new "sub-additivity", an arithmetic inequality over predicates.

Original languageEnglish
Pages (from-to)159-163
Number of pages5
JournalInformation Processing Letters
Volume59
Issue number3
DOIs
Publication statusPublished - 12 Aug 1996
Externally publishedYes

Keywords

  • Egli-Milner order
  • Formal semantics
  • Program correctness
  • Weakest liberal precondition
  • Weakest precondition

Fingerprint Dive into the research topics of 'Unifying wp and wlp'. Together they form a unique fingerprint.

Cite this