Contracts, games, and refinement.

*(English)*Zbl 1046.68571Summary: 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.

##### MSC:

68Q55 | Semantics in the theory of computing |

68Q60 | Specification and verification (program logics, model checking, etc.) |

68Q85 | Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) |

91A05 | 2-person games |

##### Keywords:

predicate transformer semantics
PDF
BibTeX
XML
Cite

\textit{R.-J. Back} and \textit{J. von Wright}, Inf. Comput. 156, No. 1--2, 25--45 (2000; Zbl 1046.68571)

Full Text:
DOI

##### References:

[1] | Abadi, M.; Lamport, L.; Wolper, P., Realizable and unrealizable specifications of reactive systems, (), 1-17 |

[2] | Back, R.J., Correctness preserving program refinements: proof theory and applications, Mathematical centre tracts, 131, (1980), Mathematical Centre Amsterdam · Zbl 0451.68018 |

[3] | Back, R.J., Changing data representation in the refinement calculus, 21st hawaii international conference on system sciences, (1989) |

[4] | Back, R.J.; von Wright, J., Refinement calculus: A systematic introduction, (1998), Springer-Verlag New York/Berlin · Zbl 0949.68094 |

[5] | Back, R.J.; von Wright, J., Duality in specification languages: A lattice-theoretical approach, Acta inform., 27, 583-625, (1990) · Zbl 0699.68038 |

[6] | Back, R.J.; von Wright, J., Games and winning strategies, Inform. process. lett., 53, 165-172, (1995) · Zbl 0875.68630 |

[7] | Dijkstra, E.W., A discipline of programming, (1976), Prentice-Hall Englewood Cliffs · Zbl 0286.00013 |

[8] | Hoare, C.A.R., Communicating sequential processes, (1985), Prentice-Hall Englewood Cliffs · Zbl 0637.68007 |

[9] | Milner, R., Communication and concurrency, (1989), Prentice-Hall Englewood Cliffs · Zbl 0683.68008 |

[10] | Morgan, C.C., Data refinement by miracles, Inform. process. lett., 26, 243-246, (1988) |

[11] | Morgan, C.C., Programming from specifications, (1990), Prentice-Hall Englewood Cliffs · Zbl 0697.68018 |

[12] | Morris, J.M., A theoretical basis for stepwise refinement and the programming calculus, Sci. comput. programming, 9, 287-306, (1987) · Zbl 0624.68017 |

[13] | Plotkin, G.D., Tech. rep., (1981) |

This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.