Improved semantics and implementation through property-based testing with QuickCheck
Improved semantics and implementation through property-based testing with QuickCheck
复制标题
通过 QuickCheck 基于属性的测试改进了语义和实现
DOI：
10.1145/2593501.2593509
复制
发表时间：
2014
期刊：
影响因子：
--
通讯作者：
S. Thompson
中科院分区：
文献类型：
--
作者：
Huiqing Li;S. Thompson
测试是验证软件实现是否满足其规范的主要方法。在本文中，我们演示了一种在QuickCheck中使用基于属性和模型的随机测试来验证可执行语义的方法，以自动化和统一语义及其实现的测试。我们的方法表明，使用可执行语义之间的正式数学规范和实现的差距的桥梁，以及强调功能性编程语言的适用性-在这种情况下，Erlang -编写可执行语义。
通过一个具体的例子说明了这种方法，在这个例子中，对Erlang编程语言的一个扩展--可伸缩组--的实现进行了测试。这个新组件带有一个用数学符号编写的小步操作语义，最初使用单元测试进行了测试。通过我们的工作，我们能够在实现和规范中找到新的bug。
Testing is the primary method to validate that a software implementation meets its specification. In this paper, we demonstrate an approach to validating an executable semantics using property- and model-based random testing in QuickCheck to automate and unify the testing of the semantics and its implementation. Our approach shows the use of executable semantics to bridge the gap between formal mathematical specification and implementation, as well as emphasising the suitability of functional programming languages -- in this case Erlang -- for writing executable semantics.
The approach is illustrated through a concrete example, in which the implementation of a proposed extension to the Erlang programming language -- scalable groups -- is tested. This new component comes with a small-step operational semantics written in mathematical notation, and was initially tested using unit testing. Through our work, we were able to find new bugs in both the implementation and the specification.