Checking Well-Formedness of Pure-Method Specifications
Checking Well-Formedness of Pure-Method Specifications
复制标题
检查纯方法规范的格式良好性
DOI：
10.1007/978-3-540-68237-0_7
复制
发表时间：
2008
期刊：
影响因子：
--
通讯作者：
Peter Müller
中科院分区：
文献类型：
--
作者：
A. Rudich;Ádám Darvas;Peter Müller
契约语言（如JML和Spec#）使用编程语言的无副作用表达式（特别是纯方法）来指定不变量和前置条件和后置条件。为了使这样的契约有意义，它们必须是格式良好的：首先，它们必须尊重操作的规范性，例如，契约中使用的纯方法的先决条件。其次，它们必须在程序逻辑中实现纯方法的一致编码，这要求它们的规范是可满足的，并且递归规范是有根据的。
本文提出了一种检查合同格式良好性的技术。我们给出的证明义务足以保证纯方法规范模型的存在。我们通过提供一个系统的解决方案，包括一个健全的结果，并通过支持更多形式的递归规范，改进了早期的工作。我们的技术已在Spec#编程系统中实现。
Contract languages such as JML and Spec# specify invariants and pre- and postconditions using side-effect free expressions of the programming language, in particular, pure methods. For such contracts to be meaningful, they must be well-formed: First, they must respect the partiality of operations, for instance, the preconditions of pure methods used in the contract. Second, they must enable a consistent encoding of pure methods in a program logic, which requires that their specifications are satisfiable and that recursive specifications are well-founded.
This paper presents a technique to check well-formedness of contracts. We give proof obligations that are sufficient to guarantee the existence of a model for the specification of pure methods. We improve over earlier work by providing a systematic solution including a soundness result and by supporting more forms of recursive specifications. Our technique has been implemented in the Spec# programming system.