A Framework for the Semantics of Behavioral Contracts

摘要

Contracts have proved a powerful concept in software engineering, to the point where we have a well regarded software development approach centered on their use, and native support in programming languages. However, it is not clear that there is a uniform concept of contract 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 reasoning 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.