Contracts, games, and refinement

Abstract

We consider the notion of a contract that governs the behavior of a collection of agents. In particular, we study the question of whether a group among these agents can achieve a given goal by following the contract. We show that this can be reduced to studying the existence of winning strategies in a two-person game. A notion of correctness and refinement is introduced for contracts and contracts are shown to form a lattice and a monoid with respect to the refinement ordering. We define a weakest precondition semantics for contracts that permits us to compute the initial states from which a group of agents has a winning strategy to reach their goal. This semantics generalizes the traditional predicate transformer semantics for program statements to contracts and games. Ordinary programs and interactive programs are special kinds of contracts. © 2000 Academic Press.