Random testing in Isabelle/HOL
Random testing in Isabelle/HOL
复制标题
伊莎贝尔/HOL 随机测试
DOI：
10.1109/sefm.2004.36
复制
发表时间：
2004
期刊：
影响因子：
--
通讯作者：
T. Nipkow
中科院分区：
文献类型：
--
作者：
Stefan Berghofer;T. Nipkow
当在定理证明器中开发非平凡的形式化时，大量的时间被用于通过失败的证明尝试来“调试”规范和说明。为了在证明的早期检测到这些问题并节省开发时间，我们扩展了Isabelle定理证明器，并使用一个工具来测试规范，通过将随机值分配给自由变量来评估命题。通过突变测试优化测试数据的分布。技术贡献是早期工作的扩展，涉及归纳定义和随机生成递归数据类型元素的通用方法。
When developing non-trivial formalizations in a theorem prover, a considerable amount of time is devoted to "debugging" specifications and conjectures by failed proof attempts. To detect such problems early in the proof and save development time, we have extended the Isabelle theorem prover with a tool for testing specifications by evaluating propositions under an assignment of random values to free variables. Distribution of the test data is optimized via mutation testing. The technical contributions are an extension of earlier work with inductive definitions and a generic method for randomly generating elements of recursive datatypes.