QuickSpec: Guessing Formal Specifications Using Testing
QuickSpec: Guessing Formal Specifications Using Testing
复制标题
QuickSpec：使用测试猜测正式规格
DOI：
10.1007/978-3-642-13977-2_3
复制
发表时间：
2010
期刊：
影响因子：
--
通讯作者：
John Hughes
中科院分区：
文献类型：
--
作者：
Koen Claessen;Nicholas Smallbone;John Hughes
我们提出QuickSpec，该工具自动生成一组纯函数的代数规格。该工具基于测试，而不是静态分析或定理证明。 QuickSpec面孔的主要挑战是在保持完整性的同时，将生成的方程数保持在最低限度。我们通过探索使用两个案例研究生成的法律来展示QuickSpec如何改善对程序模块的理解：Haskell的堆库和Erlang的定点算术库。
We present QUICKSPEC, a tool that automatically generates algebraic specifications for sets of pure functions. The tool is based on testing, rather than static analysis or theorem proving. The main challenge QUICKSPEC faces is to keep the number of generated equations to a minimum while maintaining completeness. We demonstrate how QUICKSPEC can improve one's understanding of a program module by exploring the laws that are generated using two case studies: a heap library for Haskell and a fixed-point arithmetic library for Erlang.