Unifying wp and wlp

Carroll Morgan*, Annabelle McIver

*Corresponding author for this work

Research output: Contribution to journalArticlepeer-review

6 Citations (Scopus)


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
Issue number3
Publication statusPublished - 12 Aug 1996
Externally publishedYes


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


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

Cite this