Abstract
We present a new technique called type targeted testing, which translates precise refinement types into comprehensive test-suites. The key insight behind our approach is that through the lens of SMT solvers, refinement types can also be viewed as a high-level, declarative, test generation technique, wherein types are converted to SMT queries whose models can be decoded into concrete program inputs. Our approach enables the systematic and exhaustive testing of implementations from high-level declarative specifications, and furthermore, provides a gradual path from testing to full verification. We have implemented our approach as a Haskell testing tool called TARGET, and present an evaluation that shows how TARGET can be used to test a wide variety of properties and how it compares against state-of-the-art testing approaches.
Chapter PDF
Similar content being viewed by others
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
Beyer, D., Chlipala, A.J., Henzinger, T.A., Jhala, R., Majumdar, R.: Generating tests from counterexamples. In: ICSE 2004: Software Engineering, pp. 326–335 (2004)
Boyapati, C., Khurshid, S., Marinov, D.: Korat: Automated testing based on Java predicates. In: ISSTA 2002: Software Testing and Analysis, pp. 123–133. ACM (2002)
Claessen, K., Duregård, J., Palka, M.H.: Generating constrained random data with uniform distribution. In: FLOPS 2014, pp. 18–34 (2014)
Claessen, K., Hughes, J.: QuickCheck: a lightweight tool for random testing of haskell programs. In: ICFP. ACM (2000)
Csallner, C., Smaragdakis, Y.: Check ’n’ crash: combining static checking and testing. In: ICSE, pp. 422–431 (2005)
Neto, A.C.D., Subramanyan, R., Vieira, M., Travassos, G.H.: A survey on model-based testing approaches: A systematic review. In: WEASELTech 2007. ACM (2007)
Dunfield, J.: Refined typechecking with Stardust. In: PLPV (2007)
Erkök, L.: SBV: SMT based verification in haskell, http://leventerkok.github.io/sbv/
Findler, R.B., Felleisen, M.: Contract soundness for object-oriented languages. In: OOPSLA, pp. 1–15 (2001)
Flanagan, C., Leino, K.R.M., Lillibridge, M., Nelson, G., Saxe, J.B., Stata, R.: Extended static checking for Java. In: PLDI (2002)
Gill, A., Runciman, C.: Haskell program coverage. In: Haskell 2007. ACM (2007)
Godefroid, P., Klarlund, N., Sen, K.: Dart: directed automated random testing. In: PLDI, pp. 213–223 (2005)
Jackson, D.: Alloy: a lightweight object modelling notation. ACM Transactions on Software Engineering and Methodology (TOSEM) 11(2), 256–290 (2002)
Köksal, A.S., Kuncak, V., Suter, P.: Constraints as control. In: POPL 2012, pp. 151–164. ACM, New York (2012)
Magalhães, J.P., Dijkstra, A., Jeuring, J., Löh, A.: A generic deriving mechanism for haskell. In: Haskell Symposium. ACM (2010)
Marick, B.: How to misuse code coverage. In: Proceedings of the 16th Interational Conference on Testing Computer Software, pp. 16–18 (1999)
Marinov, D., Khurshid, S.: Testera: A novel framework for automated testing of java programs. In: ASE 2001. IEEE Computer Society, Washington, DC (2001)
de Moura, L., Bjørner, N.: Generalized, efficient array decision procedures. In: FMCAD (2009)
Nelson, G.: Techniques for program verification. Tech. Rep. CSL81-10, Xerox Palo Alto Research Center (1981)
Nystrom, N., Saraswat, V.A., Palsberg, J., Grothoff, C.: Constrained types for object-oriented languages. In: OOPSLA, pp. 457–474 (2008)
Runciman, C., Naylor, M., Lindblad, F.: Smallcheck and lazy smallcheck: Automatic exhaustive testing for small values. In: Haskell Symposium. ACM (2008)
Sen, K., Marinov, D., Agha, G.: Cute: A concolic unit testing engine for c. In: ESEC/FSE. ACM (2005)
Swamy, N., Chen, J., Fournet, C., Strub, P.-Y., Bhargavan, K., Yang, J.: Secure distributed programming with value-dependent types. In: ICFP (2011)
Tillmann, N., de Halleux, J.: Pex–white box test generation for.NET. In: Beckert, B., Hähnle, R. (eds.) TAP 2008. LNCS, vol. 4966, pp. 134–153. Springer, Heidelberg (2008)
Vazou, N., Rondon, P.M., Jhala, R.: Abstract refinement types. In: Felleisen, M., Gardner, P. (eds.) ESOP 2013. LNCS, vol. 7792, pp. 209–228. Springer, Heidelberg (2013)
Vazou, N., Seidel, E.L., Jhala, R.: Liquidhaskell: Experience with refinement types in the real world. In: Haskell Symposium (2014)
Vazou, N., Seidel, E.L., Jhala, R., Vytiniotis, D., Peyton-Jones, S.: Refinement types for haskell. In: ICFP (2014)
Veanes, M., Campbell, C., Grieskamp, W., Schulte, W., Tillmann, N., Nachmanson, L.: Model-based testing of object-oriented reactive systems with spec explorer. In: Hierons, R.M., Bowen, J.P., Harman, M. (eds.) FORTEST. LNCS, vol. 4949, pp. 39–76. Springer, Heidelberg (2008)
Xi, H., Pfenning, F.: Eliminating array bound checking through dependent types. In: PLDI (1998)
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
Seidel, E.L., Vazou, N., Jhala, R. (2015). Type Targeted Testing. 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_33
Download citation
DOI: https://doi.org/10.1007/978-3-662-46669-8_33
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)