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.

错误:搜索内容不能为空,请输入英文关键词
错误:关键词超出字数限制,请精简
高级检索

Context-Aware Contracts as a Lingua Franca for Behavioral Specification

  • Marco Scaletta,
  • Reiner Hähnle

摘要

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.