Where academic tradition
meets the exciting future

Contracts, Games and Refinement

Ralph-Johan Back, Joakim von Wright, Contracts, Games and Refinement. Information and Computation 156, 25–45, 2000.

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 com- pute 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.

Files:

Full publication in PDF-format

BibTeX entry:

@ARTICLE{jBaWra,
  title = {Contracts, Games and Refinement},
  author = {Back, Ralph-Johan and Wright, Joakim von},
  journal = {Information and Computation},
  volume = {156},
  pages = {25–45},
  year = {2000},
}

Belongs to TUCS Research Unit(s): Software Construction Laboratorium

Publication Forum rating of this publication: level 3

Edit publication