Randomized Testing in PLT Redex

Date Added: Jul 2009
Format: PDF

This paper presents new support for randomized testing in PLT Redex, a domain-specific language for formalizing operational semantics. In keeping with the overall spirit of Redex, the testing support is as lightweight as possible Redex programmers simply write down predicates that correspond to facts about their calculus and the tool randomly generates program expressions in an attempt to falsify the predicates. Redex's automatic test case generation begins with simple expressions, but as time passes, it broadens its search to include increasingly complex expressions.