The New Quickcheck for Isabelle - Random, Exhaustive and Symbolic Testing under One Roof
The New Quickcheck for Isabelle - Random, Exhaustive and Symbolic Testing under One Roof
复制标题
伊莎贝尔的新快速检查 - 一站式随机、详尽和符号测试
DOI：
10.1007/978-3-642-35308-6_10
复制
发表时间：
2012
期刊：
影响因子：
--
通讯作者：
Lukas Bulwahn
中科院分区：
文献类型：
--
作者：
Lukas Bulwahn
新的QuickCheck是Isabelle/HOL的反例生成器，它使用各种测试策略发现错误的规范和无效的猜测。之前的QuickCheck只通过随机测试来测试猜测。新的QuickCheck扩展了以前的QuickCheck，并集成了两种新的测试策略：使用具体值进行穷举测试；以及符号测试，使用缩小策略来评估猜想。与这些策略正交地，我们解决了两个一般问题：第一，我们扩展了可执行猜想和规格说明的类；第二，我们提出了处理条件猜想的技术，即带有前提的猜想。我们在一些规范、功能数据结构和酒店门卡系统上对测试策略和技术进行了评估。
The new Quickcheck is a counterexample generator for Isabelle/HOL that uncovers faulty specifications and invalid conjectures using various testing strategies. The previous Quickcheck only tested conjectures by random testing. The new Quickcheck extends the previous one and integrates two novel testing strategies: exhaustive testing with concrete values; and symbolic testing, evaluating conjectures with a narrowing strategy. Orthogonally to the strategies, we address two general issues: First, we extend the class of executable conjectures and specifications, and second, we present techniques to deal with conditional conjectures, i.e., conjectures with premises. We evaluate the testing strategies and techniques on a number of specifications, functional data structures and a hotel key card system.
登录
查看更多内容
纯函数式惰性非确定性编程
影响因子：
1.1
作者：
Sebastian Fischer;O. Kiselyov;Chung
通讯作者：
Chung
验证酒店钥匙卡系统
影响因子：
2
作者：
T. Nipkow
通讯作者：
T. Nipkow
如何用成功列表替换失败：惰性函数语言中的异常处理、回溯和模式匹配方法
DOI：
10.1007/3-540-15975-4_33
发表时间：
1985
期刊：
J. Funct. Program.
影响因子：
--
作者：
Philip Wadler
通讯作者：
Philip Wadler
高阶逻辑中的类型类和重载
DOI：
10.1007/bfb0028402
发表时间：
1997
期刊：
Proceedings of the 9th Workshop on Programming Languages and Operating Systems
影响因子：
--
作者：
M. Wenzel
通讯作者：
M. Wenzel
在依赖类型理论中结合测试和证明
影响因子：
1.1
作者：
P. Dybjer;Haiyan Qiao;M. Takeyama
通讯作者：
M. Takeyama