Advertisement

Combining Static and Dynamic Contract Checking for Curry

  • Michael Hanus
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 10855)

Abstract

Static type systems are usually not sufficient to express all requirements on function calls. Hence, contracts with pre- and postconditions can be used to express more complex constraints on operations. Contracts can be checked at run time to ensure that operations are only invoked with reasonable arguments and return intended results. Although such dynamic contract checking provides more reliable program execution, it requires execution time and could lead to program crashes that might be detected with more advanced methods at compile time. To improve this situation for declarative languages, we present an approach to combine static and dynamic contract checking for the functional logic language Curry. Based on a formal model of contract checking for functional logic programming, we propose an automatic method to verify contracts at compile time. If a contract is successfully verified, dynamic checking of it can be omitted. This method decreases execution time without degrading reliable program execution. In the best case, when all contracts are statically verified, it provides trust in the software since crashes due to contract violations cannot occur during program execution.

Notes

Acknowledgments

The author is grateful to John Gallagher, Grigore Rosu, and the anonymous reviewers for their helpful comments to improve the paper.

References

  1. 1.
    Albert, E., Hanus, M., Huch, F., Oliver, J., Vidal, G.: Operational semantics for declarative multi-paradigm languages. J. Symb. Comput. 40(1), 795–829 (2005)MathSciNetCrossRefGoogle Scholar
  2. 2.
    Antoy, S., Echahed, R., Hanus, M.: A needed narrowing strategy. J. ACM 47(4), 776–822 (2000)MathSciNetCrossRefGoogle Scholar
  3. 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).  https://doi.org/10.1007/11680093_2CrossRefzbMATHGoogle Scholar
  4. 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).  https://doi.org/10.1007/11799573_9CrossRefzbMATHGoogle Scholar
  5. 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. 6.
    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).  https://doi.org/10.1007/978-3-642-27694-1_4CrossRefGoogle Scholar
  7. 7.
    Antoy, S., Hanus, M.: Default rules for Curry. Theory Pract. Log. Program. 17(2), 121–147 (2017)MathSciNetCrossRefGoogle Scholar
  8. 8.
    Braßel, B.: Implementing functional logic programs by translation into purely functional programs. Ph.D. thesis, Christian-Albrechts-Universität zu Kiel (2011)Google Scholar
  9. 9.
    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).  https://doi.org/10.1007/978-3-642-22531-4_1CrossRefGoogle Scholar
  10. 10.
    Chitil, O., McNeill, D., Runciman, C.: Lazy assertions. In: Trinder, P., Michaelson, G.J., Peña, R. (eds.) IFL 2003. LNCS, vol. 3145, pp. 1–19. Springer, Heidelberg (2004).  https://doi.org/10.1007/978-3-540-27861-0_1CrossRefGoogle Scholar
  11. 11.
    de Dios Castro, J., López-Fraguas, F.J.: Extra variables can be eliminated from functional logic programs. Electron. Notes Theor. Comput. Sci. 188, 3–19 (2007)CrossRefGoogle Scholar
  12. 12.
    de Moura, L., Bjørner, N.: Z3: an efficient SMT solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 337–340. Springer, Heidelberg (2008).  https://doi.org/10.1007/978-3-540-78800-3_24CrossRefGoogle Scholar
  13. 13.
    Dimoulas, C., Pucella, R., Felleisen, M.: Future contracts. In: Proceedings of the 11th ACM SIGPLAN International Conference on Principles and Practice of Declarative Programming (PPDP 2009), pp. 195–206. ACM Press (2009)Google Scholar
  14. 14.
    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).  https://doi.org/10.1007/978-3-642-18070-5_2CrossRefGoogle Scholar
  15. 15.
    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. Log. Program. 40, 47–87 (1999)MathSciNetCrossRefGoogle Scholar
  16. 16.
    Hanus, M.: Improving lazy non-deterministic computations by demand analysis. In: Technical Communications of the 28th International Conference on Logic Programming. Leibniz International Proceedings in Informatics (LIPIcs), vol. 17, pp. 130–143 (2012)Google Scholar
  17. 17.
    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).  https://doi.org/10.1007/978-3-642-37651-1_6CrossRefGoogle Scholar
  18. 18.
    Hanus, M.: CurryCheck: checking properties of Curry programs. In: Hermenegildo, M.V., Lopez-Garcia, P. (eds.) LOPSTR 2016. LNCS, vol. 10184, pp. 222–239. Springer, Cham (2017).  https://doi.org/10.1007/978-3-319-63139-4_13CrossRefGoogle Scholar
  19. 19.
    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/
  20. 20.
    Hanus, M., Skrlac, F.: A modular and generic analysis server system for functional logic programs. In: Proceedings of the ACM SIGPLAN 2014 Workshop on Partial Evaluation and Program Manipulation (PEPM 2014), pp. 181–188. ACM Press (2014)Google Scholar
  21. 21.
    Hanus, M. (ed.): Curry: an integrated functional logic language (vers. 0.9.0) (2016). http://www.curry-language.org
  22. 22.
    Launchbury, J.: A natural semantics for lazy evaluation. In: Proceedings of the 20th ACM Symposium on Principles of Programming Languages (POPL 1993), pp. 144–154. ACM Press (1993)Google Scholar
  23. 23.
    Milner, R.: A theory of type polymorphism in programming. J. Comput. Syst. Sci. 17, 348–375 (1978)MathSciNetCrossRefGoogle Scholar
  24. 24.
    Nguyen, P.C., Tobin-Hochstadt, S., Van Horn, D.: Soft contract verification. In: Proceedings of the 19th ACM SIGPLAN International Conference on Functional Programming (ICFP 2014), pp. 139–152. ACM Press (2014)Google Scholar
  25. 25.
    Peyton Jones, S. (ed.): Haskell 98 Language and Libraries—The Revised Report. Cambridge University Press, Cambridge (2003)zbMATHGoogle Scholar
  26. 26.
    Serrano, A., López-García, P., Bueno, F., Hermenegildo, M.V.: Sized type analysis for logic programs. Theory Pract. Log. Program. 13(4–5–Online–Supplement), 1–15 (2013)MathSciNetGoogle Scholar
  27. 27.
    Stulova, N., Morales, J.F., Hermenegildo, M.: Reducing the overhead of assertion run-time checks via static analysis. In: Proceedings of the 18th International Symposium on Principles and Practice of Declarative Programming (PPDP 2016), pp. 90–103. ACM Press (2016)Google Scholar
  28. 28.
    Stump, A.: Verified Functional Programming in Agda. ACM and Morgan & Claypool, New York (2016)CrossRefGoogle Scholar
  29. 29.
    Vazou, N., Seidel, E.L., Jhala, R.: LiquidHaskell: experience with refinement types in the real world. In: Proceedings of the 2014 ACM SIGPLAN Symposium on Haskell, pp. 39–51. ACM Press (2014)Google Scholar
  30. 30.
    Vazou, N., Seidel, E.L., Jhala, R., Peyton Jones, S.: Refinement types for Haskell. In: Proceedings of the 19th ACM SIGPLAN International Conference on Functional Programming (ICFP), pp. 269–282. ACM Press (2014)Google Scholar
  31. 31.
    Wadler, P.: How to declare an imperative. ACM Comput. Surv. 29(3), 240–263 (1997)CrossRefGoogle Scholar
  32. 32.
    Xu, D.N., Peyton Jones, S.L., Claessen, K.: Static contract checking for Haskell. In: Proceedings of the 36th ACM Symposium on Principles of Programming Languages (POPL 2009), pp. 41–52 (2009)Google Scholar

Copyright information

© Springer International Publishing AG, part of Springer Nature 2018

Authors and Affiliations

  1. 1.Institut für InformatikCAU KielKielGermany

Personalised recommendations