Unifying theories distil common features of programming languages and design methods by means of algebraic operators and their laws. Several practical concerns---e.g., improvement of a program, conformance of code with design, correctness with respect to specified requirements---are subsumed by the beautiful notion that programs and designs are special forms of specification and their relationships are instances of logical implication between specifications. Mathematical development of this idea has been very successful but limited to an impoverished notion of specification: trace properties. Some mathematically precise properties of programs---dubbed hyperproperties---refer to traces collectively. For example, confidentiality involves knowledge of possible traces. This article reports on both obvious and surprising results about lifting algebras of programming to hyperproperties, especially in connection with loops, and suggests directions for further research. The main results are: the first compositional semantics of imperative programs with loops, at the hyper level, and a proof that this semantics is the same as the direct image of a standard semantics, for subset closed hyperproperties.
The textbook of Back and von Wright @cite_10 explores predicate transformer semantics and refinement calculus. The use of @math and @math in ) is part of the extensive algebra connecting predicate transformers and relations using categorical notions @cite_17 . Upward closed sets of predicates play an important role in that algebra @cite_30 , which should be explored in connection with the present investigation and its potential application to higher order programs. The extension of functional programming calculus to imperative refinement is one setting in which strong laws (Cartesian closure) for a well-behaved subset are expressed as implications with inequational antecedents @cite_23 @cite_26 . These works use backward predicate transformers in order to model general specifications and in particular the combination of angelic and demonic nondeterminacy. Alternative models with similar aims can be found in Martin @cite_7 and Morris @cite_20 .
@cite_30 @cite_26 @cite_7 @cite_23 @cite_10 @cite_20 @cite_17
2113550426 2173455755 2003145055 2008212936
The order-enriched category of monotonic predicate transformers over posets is a model of the refinement calculus of higher order imperative programs and pre-post specifications. This category is shown to be equivalent to the category of spans over ideal relations, and ideal relations are shown to be spans over monotonic functions between posets. To do this we use a skew span construction because the standard categorical span constructions are inapplicable. Axioms are given for products and coproducts of underlying posets as well as the homset as a coexponent, using inequations (for various kinds of lax adjunctions) and conditional equations (for adjunctions in subcategories) that are shown to uniquely determine the structures. The model is described in elementary terms using power allegories, an axiomatic calculus of relations, which makes the proofs accessible to non-specialists and shows that the results generalize to other base categories. In this paper we present an algebraic construction of the category of monotonic predicate transformers from the category of relations which is similar to the standard algebraic construction of the integers from the natural numbers. The same construction yields the category of relations from the category of total functions. This provides a mechanism through which the rich type structure of the category of total functions can be promoted to successively weaker ones in the categories of relations and predicate transformers. In addition, it has exposed two complete rules for the refinement and composition of specifications in Morgan's refinement calculus. This paper presents an introduction to a calculus of binary multirelations, which can model both angelic and demonic kinds of non-determinism. The isomorphism between up-closed multirelations and monotonic predicate transformers allows a different view of program transformation, and program transformation calculations using multirelations are easier to perform in some circumstances. Multirelations are illustrated by modelling both kinds of nondeterministic behaviour in games and resource-sharing protocols. Using 2-categorical laws of algorithmic refinement, we show soundness of data refinement for stored programs and hence for higher order procedures with value result parameters. The refinement laws hold in a model that slightly generalizes the standard predicate transformer semantics for the usual imperative programming constructs including prescriptions.