Top

Published in:

2017 | OriginalPaper | Chapter

CurryCheck: Checking Properties of Curry Programs

Author : Michael Hanus

Published in: Logic-Based Program Synthesis and Transformation

Publisher: Springer International Publishing

Activate our intelligent search to find suitable subject content or patents.

search-config

AI-assisted search

Off

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.

Dont have a licence yet? Then find out more about our products and how to get one now:

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

Mit Springer Professional "Wirtschaft+Technik" erhalten Sie Zugriff auf:

über 102.000 Bücher
über 537 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Finance + Banking
Management + Führung
Marketing + Vertrieb
Maschinenbau + Werkstoffe
Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

inform now

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

über 67.000 Bücher
über 390 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Maschinenbau + Werkstoffe

Jetzt Wissensvorsprung sichern!

inform now

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

über 67.000 Bücher
über 340 Zeitschriften

aus folgenden Fachgebieten:

Bauwesen + Immobilien
Business IT + Informatik
Finance + Banking
Management + Führung
Marketing + Vertrieb
Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

inform now

previous chapter On the Completeness of Selective Unification in Concolic Testing of Logic Programs

next chapter A Hiking Trip Through the Orders of Magnitude: Deriving Efficient Generators for Closed Simply-Typed Lambda Terms and Normal Forms

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.

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.

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

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

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 CrossRef

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

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 CrossRef

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 CrossRef

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)

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

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 CrossRef

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

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 CrossRef

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)

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 CrossRef

12.

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

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 CrossRef

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 CrossRef

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)

16.

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

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 CrossRef

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)MathSciNetCrossRefMATH

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)

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)

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 CrossRef

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 CrossRef

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 CrossRef

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 CrossRef

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)

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 CrossRef

29.

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

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)

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)

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)

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)

34.

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

35.

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

Title: CurryCheck: Checking Properties of Curry Programs
Author: Michael Hanus
Publisher: Springer International Publishing
Book: Logic-Based Program Synthesis and Transformation
Print ISBN: 978-3-319-63138-7

Electronic ISBN: 978-3-319-63139-4

Copyright Year: 2017
DOI: https://doi.org/10.1007/978-3-319-63139-4_13

Springer Professional

Abstract

Please log in to get access to your license.

Dont have a licence yet? Then find out more about our products and how to get one now:

Springer Professional "Wirtschaft+Technik"

Springer Professional "Technik"

Springer Professional "Wirtschaft"

Premium Partner