Beginner's Luck A Language for Property-Based Generators

被引:25
作者
Lampropoulos, Leonidas [1 ]
Gallois-Wong, Diane [2 ,3 ]
Hritcu, Catalin [2 ]
Hughes, John [4 ]
Pierce, Benjamin C. [1 ]
Xia, Li-yao [2 ,3 ]
机构
[1] Univ Penn, Philadelphia, PA 19104 USA
[2] INRIA, Paris, France
[3] ENS Paris, Paris, France
[4] Chalmers Univ, Gothenburg, Sweden
基金
美国国家科学基金会;
关键词
random testing; property-based testing; narrowing; constraint solving; domain specific language; SAMPLERS;
D O I
10.1145/3093333.3009868
中图分类号
TP31 [计算机软件];
学科分类号
081202 ; 0835 ;
摘要
Property-based random testing a la QuickCheck requires building efficient generators for well-distributed random data satisfying complex logical predicates, but writing these generators can be difficult and error prone. We propose a domain-specific language in which generators are conveniently expressed by decorating predicates with lightweight annotations to control both the distribution of generated values and the amount of constraint solving that happens before each variable is instantiated. This language, called Luck, makes generators easier to write, read, and maintain. We give Luck a formal semantics and prove several fundamental properties, including the soundness and completeness of random generation with respect to a standard predicate semantics. We evaluate Luck on common examples from the property-based testing literature and on two significant case studies, showing that it can be used in complex domains with comparable bug-finding effectiveness and a significant reduction in testing code size compared to handwritten generators.
引用
收藏
页码:114 / 129
页数:16
相关论文
共 68 条
[1]  
[Anonymous], 2014, AAAI
[2]  
[Anonymous], 2012, ACM QUEUE, DOI DOI 10.1145/2090147.2094081
[3]  
[Anonymous], [No title captured]
[4]  
[Anonymous], UAI
[5]  
[Anonymous], 2002, Isabelle/HOL: a proof assistant for higher-order logic
[6]  
Antoy S., 2000, JACM
[7]  
Arts T., 2008, 7 ACM SIGPLAN WORKSH
[8]  
Avgerinos T., 2014, ICSE
[9]   A Decade of Software Model Checking with SLAM [J].
Ball, Thomas ;
Levin, Vladimir ;
Rajamani, Sriram K. .
COMMUNICATIONS OF THE ACM, 2011, 54 (07) :68-76
[10]  
Blanchette J. C., 2010, ITP