Abstract
This paper presents a generic method for randomly generating well-typed expressions. It starts from a specification of a typing judgment in PLT Redex and uses a specialized solver that employs randomness to find many different valid derivations of the judgment form.
Our motivation for building these random terms is to more effectively falsify conjectures as part of the tool-support for semantics models specified in Redex. Accordingly, we evaluate the generator against the other available methods for Redex, as well as the best available custom well-typed term generator. Our results show that our new generator is much more effective than generation techniques that do not explicitly take types into account and is competitive with generation techniques that do, even though they are specialized to particular type-systems and ours is not.
Chapter PDF
Similar content being viewed by others
References
Claire, E., Alvis, J.J., Willcock, K.M., Carter, W.E.: Byrd, and Daniel P. Friedman. cKanren: miniKanren with Constraints. In: Proc. Scheme and Functional Programming (2011)
Appel, A.W., Dockins, R., Leroy, X.: A list-machine benchmark for mechanized metatheory. Journal of Automated Reasoning 49(3), 453–491 (2012)
Baader, F., Snyder, W.: Unification Theory. In: Handbook of Automated Reasoning, vol. 1, pp. 445–532 (2001)
Bourjarwah, A.S., Saleh, K.: Compiler test case generation methods: a survey and assessment. Information & Software Technology 39(9), 617–625 (1997)
Byrd, W.E.: Relational Programming in miniKanren: Techniques, Applications, and Implementations. PhD dissertation, Indiana University (2009)
Claessen, K., Duregard, J., Palka, M.H.: Generating Constrained Random Data with Uniform Distribution. In: Proc. Intl. Symp. Functional and Logic Programming, pp. 18–34 (2014)
Claessen, K., Hughes, J.: QuickCheck: A Lightweight Tool for Random Testing of Haskell Programs. In: Proc. ACM Intl. Conf. Functional Programming, pp. 268–279 (2000)
Colmerauer, A.: Equations and Inequations on Finite and Infinite Trees. In: Proc. Intl. Conf. Fifth Generation Computing Systems, pp. 85–99 (1984)
Comon, H., Dauchet, M., Gilleron, R., Loding, C., Jacquemard, F., Lugiez, D., Tison, S., Tommasi, M.: Tree Automata Techniques and Applications (2007), http://www.grappa.univ-lille3.fr/tata
Comon, H., Lescanne, P.: Equational Problems and Disunification. Journal of Symbolic Computation 7, 371–425 (1989)
Duregard, J., Jansson, P., Wang, M.: Feat: Functional Enumeration of Algebraic Types. In: Proc. ACM SIGPLAN Haskell Wksp, pp. 61–72 (2012)
Felleisen, M., Findler, R.B., Flatt, M.: Semantics Engineering with PLT Redex. MIT Press (2010)
Fetscher, B.: The Random Generation of Well-Typed Terms. Northwestern University, NU-EECS-14-05 (2014)
Findler, R.B., Klein, C., Fetscher, B.: The Redex Reference (2014), http://docs.racket-lang.org/redex
Grygiel, K., Lescanne, P.: Counting and generating lambda terms. J. Functional Programming 23(5), 594–628 (2013)
Hanford, K.V.: Automatic Generation of Test Cases. IBM Systems Journal 9(4), 244–257 (1970)
Jaffar, J., Maher, M.J., Marriott, K., Stuckey, P.J.: The Semantics of Constraint Logic Programming. Journal of Logic Programming 37(1-3), 1–46 (1998)
Kennedy, A.J., Vytiniotis, D.: Every bit counts: The binary representation of typed data and programs. J. Functional Programming 22, 529–573 (2012)
Klein, C.: Experience with Randomized Testing in Programming Language Metatheory. MS dissertation, Northwestern University (2009)
Klein, C., Clements, J., Dimoulas, C., Eastlund, C., Felleisen, M., Flatt, M., McCarthy, J.A., Rafkind, J., Tobin-Hochstadt, S., Findler, R.B.: Run Your Research: On the Effectiveness of Lightweight Mechanization. In: Proc. ACM Symp. Principles of Programming Languages (2012)
Klein, C., Findler, R.B.: Randomized Testing in PLT Redex. In: Proc. Scheme and Functional Programming, pp. 26–36 (2009)
Klein, C., Findler, R.B., Flatt, M.: The Racket virtual machine and randomized testing. In: Higher-Order and Symbolic Computation (2013)
Kutsia, T.: Unification with Sequence Symbols and Flexible Arity Symbols and Its Extension with Pattern-Terms. In: Proc. Intl. Conf. Artificial Intelligence, Automated Reasoning, and Symbolic Computation, pp. 290–304 (2002)
Pałka, M.H.: Testing an Optimising Compiler by Generating Random Lambda Terms. Licentiate dissertation, Chalmers University of Technology, Göteborg (2012)
Pałka, M.H., Claessen, K., Russo, A., Hughes, J.: Testing an Optimising Compiler by Generating Random Lambda Terms. In: Proc. International Workshop on Automation of Software Test (2011)
Takikawa, A., Strickland, T.S., Tobin-Hochstadt, S.: Constraining Delimited Control with Contracts. In: Proc. Euro. Symp. Programming, pp. 229–248 (2013)
Yang, X., Chen, Y., Eide, E., Regehr, J.: Finding and Understanding Bugs in C Compilers. In: Proc. ACM Conf. Programming Language Design and Implementation, pp. 283–294 (2011)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2015 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Fetscher, B., Claessen, K., Pałka, M., Hughes, J., Findler, R.B. (2015). Making Random Judgments: Automatically Generating Well-Typed Terms from the Definition of a Type-System. In: Vitek, J. (eds) Programming Languages and Systems. ESOP 2015. Lecture Notes in Computer Science(), vol 9032. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-662-46669-8_16
Download citation
DOI: https://doi.org/10.1007/978-3-662-46669-8_16
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-662-46668-1
Online ISBN: 978-3-662-46669-8
eBook Packages: Computer ScienceComputer Science (R0)