Type Targeted Testing
Type Targeted Testing
复制标题
类型针对性测试
DOI：
--
复制
发表时间：
2014
期刊：
影响因子：
--
通讯作者：
Ranjit Jhala
中科院分区：
文献类型：
--
作者：
Eric L. Seidel;Niki Vazou;Ranjit Jhala
我们提出了一种称为靶向测试的新技术，该技术将精确的细化类型转化为全面的测试服务。我们方法背后的关键见解是，通过SMT求解器的镜头，改进类型也可以看作是一种高级，声明性的，测试生成技术，其中类型被转换为SMT查询，其模型可以被解码为混凝土程序输入。我们的方法可以从高级声明规格中对实现的系统和详尽的测试，此外，还提供了从测试到完整验证的逐渐途径。我们已经将方法作为一种称为目标的Haskell测试工具实施，并提出了一项评估，该评估表明如何使用目标来测试各种属性，以及如何与最新的测试方法进行比较。
We present a new technique called type targeted testing, which translates precise refinement types into comprehensive test-suites. The key insight behind our approach is that through the lens of SMT solvers, refinement types can also be viewed as a high-level, declarative, test generation technique, wherein types are converted to SMT queries whose models can be decoded into concrete program inputs. Our approach enables the systematic and exhaustive testing of implementations from high-level declarative specifications, and furthermore, provides a gradual path from testing to full verification. We have implemented our approach as a Haskell testing tool called TARGET, and present an evaluation that shows how TARGET can be used to test a wide variety of properties and how it compares against state-of-the-art testing approaches.