Evolving Contracts

Abstract:

Any formalism to describe contracts must be able to capture evolvability over time, and also to correlate such evolutions to changes in the environment or in the behavior of the parties involved in contracts. Yet, few works have focused on the general problem of verifying evolvable contracts.

In this talk I will present ongoing work on the definition of an abstract theory of dynamic contracts, including some preliminary results concerning verification of static and dynamic contracts. Starting from a very general view of contracts as syntactic entities that characterize sets of traces, I show how to accomodate two essential ingredients of dynamic contracts: spillover, which characterizes the remains of a clause when it is withdrawn from a contract, and power, which characterizes when a principal is entitled to perform a change in a contract. Although the technical development is carried in an abstract setting, I will illustrate our definitions and results using contract languages for rights and obligations; these languages, despite their simplicity, share many essential features with other formalisms for digital right management and access control, and are therefore representative of the potential interest of our approach.