Abstract

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. To improve test coverage, test generation exploits the structure of the model’s metafunction and reduction relation definitions. The paper also reports on a case-study applying Redex’s testing support to the latest revision of the Scheme standard. Despite a community review period, as well as a comprehensive, manually constructed test suite, Redex’s random test case generation was able to identify several bugs in the semantics.