A framework for the semantics of behavioral contracts
Ashley McNeile · 2010
Abstract. Contracts have proved a powerful concept in software engi-neering, to the point where we have a well regarded software development approach centered on their use, and native support in programming lan-guages. However, it is not clear that there is a uniform concept of con-tract that can be applied to both algorithmic and interactive software. We propose a framework for thinking about software contracts based on the idea that a contract aims to preserve a formal proposition about the software system being built, and the form of the contract must reflect both the proposition whose truth is to be preserved and the formal rea-soning system used for verification. In particular, we believe that very different forms of contract are needed for algorithmic and interactive software and illustrate this with examples. 1