Falling Back on Executable Specifications
Falling Back on Executable Specifications
复制标题
依靠可执行的规范
DOI：
--
复制
发表时间：
2010
期刊：
影响因子：
--
通讯作者：
T. Millstein
中科院分区：
文献类型：
--
作者：
Hesam Samimi;Ei Darli Aung;T. Millstein
我们描述了一种新的方法，采用规范的软件可靠性。而不是仅仅使用规范来验证实现，我们还采用规范作为这些实现的可靠替代方案。我们的方法，我们称之为计划B，执行方法的动态契约检查。然而，而不是停止违反合同的程序，我们采用了约束求解器自动执行规范，以允许程序继续正常。本文介绍了计划B以及它的实例化扩展到Java的可执行规范，我们称之为PBnJ（计划B在Java中）。我们提出了PBnJ的设计，通过例子和描述其实现，它利用了Kodkod关系约束求解器。我们还描述了我们的经验，使用该语言来增强几个现有的Java应用程序的可靠性和功能。
We describe a new approach to employing specifications for software reliability. Rather than only using specifications to validate implementations, we additionally employ specifications as a reliable alternative to those implementations. Our approach, which we call Plan B, performs dynamic contract checking of methods. However, instead of halting the program upon a contract violation, we employ a constraint solver to automatically execute the specification in order to allow the program to continue properly. This paper describes Plan B as well as its instantiation in an extension to Java with executable specifications that we call PBnJ (Plan B in Java). We present the design of PBnJ by example and describe its implementation, which leverages the Kodkod relational constraint solver. We also describe our experience using the language to enhance the reliability and functionality of several existing Java applications.