Unifying wp and wlp

Carroll Morgan; Annabelle McIver

doi:10.1016/0020-0190(96)00093-2

Unifying wp and wlp

Carroll Morgan^*, Annabelle McIver

^*Corresponding author for this work

Research output: Contribution to journal › Article › peer-review

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 language	English
Pages (from-to)	159-163
Number of pages	5
Journal	Information Processing Letters
Volume	59
Issue number	3
DOIs	https://doi.org/10.1016/0020-0190(96)00093-2
Publication status	Published - 12 Aug 1996
Externally published	Yes

Keywords

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

Access to Document

10.1016/0020-0190(96)00093-2

Cite this

@article{30685943e44b417ab0238fbc84e76065,

title = "Unifying wp and wlp",

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.",

keywords = "Egli-Milner order, Formal semantics, Program correctness, Weakest liberal precondition, Weakest precondition",

author = "Carroll Morgan and Annabelle McIver",

year = "1996",

month = aug,

day = "12",

doi = "10.1016/0020-0190(96)00093-2",

language = "English",

volume = "59",

pages = "159--163",

journal = "Information Processing Letters",

issn = "0020-0190",

publisher = "Elsevier",

number = "3",

}

TY - JOUR

T1 - Unifying wp and wlp

AU - Morgan, Carroll

AU - McIver, Annabelle

PY - 1996/8/12

Y1 - 1996/8/12

N2 - 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.

AB - 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.

KW - Egli-Milner order

KW - Formal semantics

KW - Program correctness

KW - Weakest liberal precondition

KW - Weakest precondition

UR - https://www.scopus.com/pages/publications/0003857861

U2 - 10.1016/0020-0190(96)00093-2

DO - 10.1016/0020-0190(96)00093-2

M3 - Article

AN - SCOPUS:0003857861

SN - 0020-0190

VL - 59

SP - 159

EP - 163

JO - Information Processing Letters

JF - Information Processing Letters

IS - 3

ER -

Unifying wp and wlp

Abstract

Keywords

Access to Document

Other files and links

Fingerprint

Cite this