TY - JOUR
T1 - Predicate transformers and higher-order programs
AU - Naumann, David A.
PY - 1995/10/16
Y1 - 1995/10/16
N2 - 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.
AB - 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.
UR - http://www.scopus.com/inward/record.url?scp=0029391669&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=0029391669&partnerID=8YFLogxK
U2 - 10.1016/0304-3975(94)00247-G
DO - 10.1016/0304-3975(94)00247-G
M3 - Article
AN - SCOPUS:0029391669
SN - 0304-3975
VL - 150
SP - 111
EP - 159
JO - Theoretical Computer Science
JF - Theoretical Computer Science
IS - 1
ER -