Predicate Transformers

Abstract

We described the basic notion of a contract between independent agents in the introduction and showed a number of properties that it would be reasonable to expect contracts to have. We did not, however, say what kind of mathematical entities contracts are. The interpretation of contracts depends on what features are considered essential and what are inessential. We now make the assumption that the essential feature of a contract is what can be achieved with it. From this point of view, contracts can be interpreted as predicate transformers, functions from predicates to predicates. We will explore this approach below in detail, concentrating first on basic mathematical properties of predicate transformers and on how contracts are interpreted as predicate transformers.