Lazy generation of canonical test programs

Abstract

Property-based testing can be a highly effective form of lightweight verification, but it relies critically on the method used to generate test cases. If we wish to test properties of compilers and related tools we need a generator for source programs as test cases. We describe experiments generating functional programs in a core first-order language with algebraic data types. Candidate programs are generated freely over a syntactic representation with positional names. Static conditions for program validity and canonical representatives of large equivalence classes are defined separately. The technique is used to investigate the correctness properties of a program optimisation and two language implementations. © 2012 Springer-Verlag.