Predicate transformers and higher-order programs

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.