Context-Aware Contracts as a Lingua Franca for Behavioral Specification
摘要
Formal specification is the prerequisite for verification of behavioral properties of programs. Most specification languages are tied to the programming language they specify, the features and the verification techniques they support can differ substantially. Complex, particularly, concurrent behavior, requires non-intuitive and low-level specifications. Together with language-specificity, this causes specification languages to suffer from a lack of interoperability. Even when two specifications expressed in different languages are intended to describe the same behavior, they cannot be easily compared, let alone formally analyzed. Context-aware trace contracts (CATs) are a highly expressive specification trace logic that can describe complex behaviors intuitively and independently of an underlying programming language. We propose CATs as a lingua franca for behavioral specification. We demonstrate how target language-specific formalisms can be desugared into CATs, resulting in intuitive, comparable specifications, that are independent of code. We illustrate the desugaring process for the Java Modeling Language and apply it to an excerpt of the Casino case study.