Combining Testing and Proving in Dependent Type Theory
Combining Testing and Proving in Dependent Type Theory
复制标题
在依赖类型理论中结合测试和证明
DOI：
10.1007/10930755_12
复制
发表时间：
2003
影响因子：
1.1
通讯作者：
M. Takeyama
中科院分区：
文献类型：
--
作者：
P. Dybjer;Haiyan Qiao;M. Takeyama
我们使用 Claessen 和 Hughes 工具 QuickCheck 的修改版本扩展了依赖类型理论的证明助手 Agda/Alfa，用于功能程序的随机测试。通过这种方式，我们将测试和证明结合在一个系统中。测试用于在尝试证明之前调试程序和规范。此外，我们通过示例演示了如何在证明过程中重复使用测试来测试合适的子目标。我们的工具使用 Agda/Alfa 内部定义的测试数据生成器。因此，我们可以使用类型系统来证明它们的属性，特别是满射性，表明所有可能的测试用例确实可以生成。
We extend the proof assistant Agda/Alfa for dependent type theory with a modified version of Claessen and Hughes' tool QuickCheck for random testing of functional programs. In this way we combine testing and proving in one system. Testing is used for debugging programs and specifications before a proof is attempted. Furthermore, we demonstrate by example how testing can be used repeatedly during proof for testing suitable subgoals. Our tool uses testdata generators which are defined inside Agda/Alfa. We can therefore use the type system to prove properties about them, in particular surjectivity stating that all possible test cases can indeed be generated.