Predicate transformers and higher-order programs

Research output: Contribution to journalArticlepeer-review

11 Scopus citations

Abstract

Example higher-order programs are presented in the style of Hoare logic and refinement calculus, as motivation for a study of weak (lax) coexponents in categories of predicate transformers. The preordered category of monotonic predicate transformers between powersets is shown to have weak components that give an operationally sound predicate transformer semantics to higher-order programs and designs. The semantics is for stored programs, orthogonal to (but compatible with) procedures and parameter passing. The weak coexponent is not unique, and may be chosen to represent all designs in refinement calculus, or to represent only feasible programs, or only total deterministic programs. For the latter alternative there is a complete axiomatization in terms of program level laws of refinement, for positively conjunctive predicate transformers. A different alternative makes all program specifications representable. The results exemplify both the benefits and the limitations of categorial axiomatizations of program constructs.

Original languageEnglish
Pages (from-to)111-159
Number of pages49
JournalTheoretical Computer Science
Volume150
Issue number1
DOIs
StatePublished - 16 Oct 1995

Fingerprint

Dive into the research topics of 'Predicate transformers and higher-order programs'. Together they form a unique fingerprint.

Cite this