From behavioural contracts to smart contracts

The notion of contract in computer science has been associated with several fields and application. The term of contract programming was firstly conceived in 1986 by Bertrand Meyer in connection with the design of the Eiffel programming language. The idea was that software systems collaborate on the basis of mutual obligations and benefits. The widespread of distributed application and the interaction with third party services brought to the adoption of contracts in defining software behaviours. In such settings, contracts are important for correctly designing, implementing, and composing distributed software services. They can be used at different levels of abstraction and with different purposes, e.g. to model the possible interaction patterns of services, with the typical goal of composing honest services which guarantee deadlock-free interactions, or to model Service Level Agreements (SLAs), specifying what has to be expected from a service, and what from the client. Recently, the notion of smart contracts was introduced in 1997 by Nick Szabo to describe agreements between two or more parties that can be automatically enforced without a trusted intermediary. With the advent of distributed ledger technologies, led by Bitcoin and Ethereum, smart contracts are rendered as computer programs under the control of a peer-to-peer network that creates and executes them. Moreover, smart contracts control valuable assets. In recent years several attacks were carried on against organization and platforms, leading to huge money losses. Formal models have always been paramount in abstracting complex and elaborated realities and providing solid bases to enable formal reasoning about problems. While this aspects were largely considered for behavioural contracts, they are still a novelty for smart contracts. Moreover, domain-specific languages (DSLs) are crucial in simplifying the adoption of new technologies and help developers in avoiding common mistakes. This thesis presents the application of formal methods and DSLs both to behavioral contracts and smart contracts.