Skip to main content
SpringerLink
Log in

CurryCheck: Checking Properties of Curry Programs

  • Conference paper
  • First Online:
Logic-Based Program Synthesis and Transformation (LOPSTR 2016)

Part of the book series: Lecture Notes in Computer Science ((LNTCS,volume 10184))

Abstract

We present CurryCheck, a tool to automate the testing of programs written in the functional logic programming language Curry. CurryCheck executes unit tests as well as property tests which are parameterized over one or more arguments. CurryCheck tests properties by systematically enumerating test cases so that, for smaller finite domains, CurryCheck can actually prove properties. Unit tests and properties can be defined in a Curry module without being exported. Thus, they are also useful to document the intended semantics of the source code. Furthermore, CurryCheck also supports the automated checking of specifications and contracts occurring in source programs. Hence, CurryCheck is a useful tool that contributes to the property- and specification-based development of reliable and well tested declarative programs.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 39.99
Price excludes VAT (USA)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Notes

  1. 1.

    One can also provide several module names so that they are tested at once. Furthermore, CurryCheck has various options to influence the number of test cases, default types for polymorphic properties, etc.

  2. 2.

    In order to get an idea of the distribution of the generated test data, CurryCheck also provides property combinators collect and classify known from QuickCheck.

  3. 3.

    The property “always \(\;x\)” is satisfied if all values of x are True.

  4. 4.

    See http://www.informatik.uni-kiel.de/~pakcs/lib/Combinatorial.html for an example.

References

  1. Amaral, C., Florido, M., Santos Costa, V.: PrologCheck – property-based testing in prolog. In: Codish, M., Sumii, E. (eds.) FLOPS 2014. LNCS, vol. 8475, pp. 1–17. Springer, Cham (2014). doi:10.1007/978-3-319-07151-0_1

    Chapter  Google Scholar 

  2. Antoy, S., Echahed, R., Hanus, M.: A needed narrowing strategy. J. ACM 47(4), 776–822 (2000)

    Article  MathSciNet  MATH  Google Scholar 

  3. Antoy, S., Hanus, M.: Declarative programming with function patterns. In: Hill, P.M. (ed.) LOPSTR 2005. LNCS, vol. 3901, pp. 6–22. Springer, Heidelberg (2006). doi:10.1007/11680093_2

    Chapter  Google Scholar 

  4. Antoy, S., Hanus, M.: Overlapping rules and logic variables in functional logic programs. In: Etalle, S., Truszczyński, M. (eds.) ICLP 2006. LNCS, vol. 4079, pp. 87–101. Springer, Heidelberg (2006). doi:10.1007/11799573_9

    Chapter  Google Scholar 

  5. Antoy, S., Hanus, M.: Set functions for functional logic programming. In: Proceedings of the 11th ACM SIGPLAN International Conference on Principles and Practice of Declarative Programming (PPDP 2009), pp. 73–82. ACM Press (2009)

    Google Scholar 

  6. Antoy, S., Hanus, M.: Functional logic programming. Commun. ACM 53(4), 74–85 (2010)

    Article  Google Scholar 

  7. Antoy, S., Hanus, M.: Contracts and specifications for functional logic programming. In: Russo, C., Zhou, N.-F. (eds.) PADL 2012. LNCS, vol. 7149, pp. 33–47. Springer, Heidelberg (2012). doi:10.1007/978-3-642-27694-1_4

    Chapter  Google Scholar 

  8. Antoy, S., Hanus, M.: Default rules for Curry. Theory Pract. Logic Program. 17(2), 121–147 (2017)

    Article  MathSciNet  Google Scholar 

  9. Antoy, S., Hanus, M.: Eliminating irrelevant non-determinism in functional logic programs. In: Lierler, Y., Taha, W. (eds.) PADL 2017. LNCS, vol. 10137, pp. 1–18. Springer, Cham (2017). doi:10.1007/978-3-319-51676-9_1

    Chapter  Google Scholar 

  10. Antoy, S., Hanus, M., Libby, S.: Proving non-deterministic computations in Agda. In: Proceeding of the 24th International Workshop on Functional and (Constraint) Logic Programming (WFLP 2016), vol. 234 of Electronic Proceedings in Theoretical Computer Science, pp. 180–195. Open Publishing Association (2017)

    Google Scholar 

  11. Bernardy, J.-P., Jansson, P., Claessen, K.: Testing polymorphic properties. In: Gordon, A.D. (ed.) ESOP 2010. LNCS, vol. 6012, pp. 125–144. Springer, Heidelberg (2010). doi:10.1007/978-3-642-11957-6_8

    Chapter  Google Scholar 

  12. Braßel, B., Hanus, M., Huch, F.: Encapsulating non-determinism in functional logic computations. J. Funct. Logic Program. 2004(6) (2004)

    Google Scholar 

  13. Braßel, B., Hanus, M., Peemöller, B., Reck, F.: KiCS2: a new compiler from Curry to Haskell. In: Kuchen, H. (ed.) WFLP 2011. LNCS, vol. 6816, pp. 1–18. Springer, Heidelberg (2011). doi:10.1007/978-3-642-22531-4_1

    Chapter  Google Scholar 

  14. Christiansen, J., Fischer, S.: EasyCheck — test data for free. In: Garrigue, J., Hermenegildo, M.V. (eds.) FLOPS 2008. LNCS, vol. 4989, pp. 322–336. Springer, Heidelberg (2008). doi:10.1007/978-3-540-78969-7_23

    Chapter  Google Scholar 

  15. Claessen, K., Hughes, J.: QuickCheck: a lightweight tool for random testing of Haskell programs. In: International Conference on Functional Programming (ICFP 2000), pp. 268–279. ACM Press (2000)

    Google Scholar 

  16. Claessen, K., Hughes, J.: Testing monadic code with QuickCheck. ACM SIGPLAN Not. 37(12), 47–59 (2002)

    Article  Google Scholar 

  17. Fähndrich, M., Logozzo, F.: Static contract checking with abstract interpretation. In: Beckert, B., Marché, C. (eds.) FoVeOOS 2010. LNCS, vol. 6528, pp. 10–30. Springer, Heidelberg (2011). doi:10.1007/978-3-642-18070-5_2

    Chapter  Google Scholar 

  18. González-Moreno, J.C., Hortalá-González, M.T., López-Fraguas, F.J., Rodríguez-Artalejo, M.: An approach to declarative programming based on a rewriting logic. J. Logic Program. 40, 47–87 (1999)

    Article  MathSciNet  MATH  Google Scholar 

  19. Hanus, M.: A unified computation model for functional and logic programming. In: Proceeding of the 24th ACM Symposium on Principles of Programming Languages (Paris), pp. 80–93 (1997)

    Google Scholar 

  20. Hanus, M.: Declarative processing of semistructured web data. In: Technical Communications of the 27th International Conference on Logic Programming, vol. 11, pp. 198–208. Leibniz International Proceedings in Informatics (LIPIcs) (2011)

    Google Scholar 

  21. Hanus, M.: Functional logic programming: from theory to Curry. In: Voronkov, A., Weidenbach, C. (eds.) Programming Logics. LNCS, vol. 7797, pp. 123–168. Springer, Heidelberg (2013). doi:10.1007/978-3-642-37651-1_6

    Chapter  Google Scholar 

  22. Hanus, M., Antoy, S., Braßel, B., Engelke, M., Höppner, K., Koj, J., Niederau, P., Sadre, R., Steiner, F.: PAKCS: The Portland Aachen Kiel Curry System (2016). http://www.informatik.uni-kiel.de/pakcs/

  23. M. Hanus (ed.). Curry: An Integrated Functional Logic Language (vers. 0.9.0) (2016). http://www.curry-language.org

  24. Hermenegildo, M.: A documentation generator for (C)LP systems. In: Lloyd, J., Dahl, V., Furbach, U., Kerber, M., Lau, K.-K., Palamidessi, C., Pereira, L.M., Sagiv, Y., Stuckey, P.J. (eds.) CL 2000. LNCS, vol. 1861, pp. 1345–1361. Springer, Heidelberg (2000). doi:10.1007/3-540-44957-4_90

    Chapter  Google Scholar 

  25. Johansson, M., Rosén, D., Smallbone, N., Claessen, K.: Hipster: integrating theory exploration in a proof assistant. In: Watt, S.M., Davenport, J.H., Sexton, A.P., Sojka, P., Urban, J. (eds.) CICM 2014. LNCS (LNAI), vol. 8543, pp. 108–122. Springer, Cham (2014). doi:10.1007/978-3-319-08434-3_9

    Chapter  Google Scholar 

  26. Koopman, P., Alimarine, A., Tretmans, J., Plasmeijer, R.: Gast: generic automated software testing. In: Peña, R., Arts, T. (eds.) IFL 2002. LNCS, vol. 2670, pp. 84–100. Springer, Heidelberg (2003). doi:10.1007/3-540-44854-3_6

    Chapter  Google Scholar 

  27. Kuraj, I., Kuncak, V., Jackson, D.: Programming with enumerable sets of structures. In: Proceeding of the 2015 ACM SIGPLAN International Conference on Object-Oriented Programming, Systems, Languages, and Applications (OOPSLA 2015), pp. 37–56. ACM (2015)

    Google Scholar 

  28. Norell, U.: Dependently typed programming in Agda. In: Koopman, P., Plasmeijer, R., Swierstra, D. (eds.) AFP 2008. LNCS, vol. 5832, pp. 230–266. Springer, Heidelberg (2009). doi:10.1007/978-3-642-04652-0_5

    Chapter  Google Scholar 

  29. Oberschweiber, J.: A package manager for Curry. Master’s thesis, University of Kiel (2016)

    Google Scholar 

  30. Papadakis, M., Sagonas, K.: A PropEr integration of types and function specifications with property-based testing. In: Proceeding of the 10th ACM SIGPLAN Workshop on Erlang, pp. 39–50 (2011)

    Google Scholar 

  31. Reddy, U.S.: Narrowing as the operational semantics of functional languages. In: Proceeding of IEEE International Symposium on Logic Programming, pp. 138–151, Boston (1985)

    Google Scholar 

  32. Runciman, C., Naylor, M., Lindblad, F.: SmallCheck and Lazy SmallCheck: automatic exhaustive testing for small values. In: Proceeding of the 1st ACM SIGPLAN Symposium on Haskell, pp. 37–48. ACM Press (2008)

    Google Scholar 

  33. Stulova, N., Morales, J.F., Hermenegildo, M.: Reducing the overhead of assertion run-time checks via static analysis. In: Proceeding 18th International Symposium on Principles and Practice of Declarative Programming (PPDP 2016), pp. 90–103. ACM Press (2016)

    Google Scholar 

  34. Stump, A.: Verified Functional Programming in Agda. ACM and Morgan & Claypool, New York (2016)

    Book  Google Scholar 

  35. Wadler, P.: How to declare an imperative. ACM Comput. Surv. 29(3), 240–263 (1997)

    Article  Google Scholar 

Download references

Acknowledgements

The author is grateful to Jan-Patrick Baye for implementing an initial version of CurryCheck and to the anonymous reviewers for their suggestions to improve this paper.

Author information

Authors and Affiliations

  1. Institut Für Informatik, CAU Kiel, 24098, Kiel, Germany

    Michael Hanus

Authors
  1. Michael Hanus
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Michael Hanus .

Editor information

Editors and Affiliations

  1. IMDEA Software Institute and Universidad Politécnica de Madrid, Madrid, Spain

    Manuel V Hermenegildo

  2. IMDEA Software Institute and CSIC, Madrid, Spain

    Pedro Lopez-Garcia

Rights and permissions

Reprints and permissions

Copyright information

© 2017 Springer International Publishing AG

About this paper

Cite this paper

Hanus, M. (2017). CurryCheck: Checking Properties of Curry Programs. In: Hermenegildo, M., Lopez-Garcia, P. (eds) Logic-Based Program Synthesis and Transformation. LOPSTR 2016. Lecture Notes in Computer Science(), vol 10184. Springer, Cham. https://doi.org/10.1007/978-3-319-63139-4_13

Download citation

  • DOI: https://doi.org/10.1007/978-3-319-63139-4_13

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-319-63138-7

  • Online ISBN: 978-3-319-63139-4

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation