Dealing with the hypothetical in contracts

The notion of a contract as an agreement regulating the behaviour of two (or more) parties has long been studied, with most work focusing on the interaction between the contract and the parties. This view limits the analysis of contracts as first-class entities — which can be studied independently of the parties they regulate. Deontic logic [1] has long sought to take a contract-centric view, but has been marred with problems arising from paradoxes and practical oddities [2]. Within the field of computer science, the holy grail of contracts is that of a deontic logic sufficiently expressive to enable reasoning about real-life contracts but sufficiently restricted to avoid paradoxes and to be computationally tractable. Contract automata [3–5] have been proposed as a way of expressing the expected behaviour of interacting systems, encompassing the deontic notions of obligation, prohibition and permission. For instance, the contract automaton shown in Fig. 1 expresses the contract which states that ‘the client is permitted to initialise a service, after which, he or she is obliged to submit valid user credentials and the provider is prohibited from increasing the price of the service.’ Note that the states are tagged with the deontic information, explicitly stating what actions are obliged (O), permitted (P) and forbidden (F) by which party (given in the subscript). The transitions are tagged with actions which when taken by the parties induce a change of state, with ∗ being used as shorthand to denote anything-else.peer-reviewe