Unifying wp and wlp

Carroll Morgan*, Annabelle McIver

*Corresponding author for this work

Research output: Contribution to journalArticle

6 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

    Fingerprint

Keywords

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

Cite this