Combining Static and Dynamic Contract Checking for Curry

• Autorzy: Hanus Michael

Identyfikatory

DOI

10.3233/FI-2020-1925

• Języki publikacji: EN

Abstrakty

EN

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, it can be omitted from dynamic checking. 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.

Słowa kluczowe

EN

contracts; declarative programming; verification

• Wydawca: IOS Press
• Czasopismo: Fundamenta Informaticae
• Rocznik: 2020
• Tom: Vol. 173, nr 4
• Strony: 285--314
• Opis fizyczny: Bibliogr. 38 poz., rys., tab.

Twórcy

autor

Hanus Michael

• Institut für Informatik, CAU Kiel, Germany

Bibliografia

• [1] Milner R. A Theory of Type Polymorphism in Programming. Journal of Computer and System Sciences, 1978. 17:348-375.
• [2] Stump A. Verified Functional Programming in Agda. ACM and Morgan & Claypool, 2016. doi:10.1145/2841316.
• [3] Antoy S, Hanus M. Contracts and Specifications for Functional Logic Programming. In: Proc. of the 14th International Symposium on Practical Aspects of Declarative Languages (PADL 2012). Springer LNCS 7149, 2012 pp. 33-47. doi:10.1007/978-3-642-27694-1_4.
• [4] de Moura L, Bjørner N. Z3: An Efficient SMT Solver. In: Proc. of the 14th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2008). Springer LNCS 4963, 2008 pp. 337-340. doi:10.1007/978-3-540-78800-3.
• [5] Hanus (ed) M. Curry: An Integrated Functional Logic Language (Vers. 0.9.0). Available at http://www.curry-language.org, 2016.
• [6] Hanus M. Functional Logic Programming: From Theory to Curry. In: Programming Logics - Essays in Memory of Harald Ganzinger. Springer LNCS 7797, 2013 pp. 123-168. doi:10.1007/978-3-642-37651-1\_6.
• [7] Peyton Jones S (ed.). Haskell 98 Language and Libraries — The Revised Report. Cambridge University Press, 2003.
• [8] Antoy S, Echahed R, Hanus M. A Needed Narrowing Strategy. Journal of the ACM, 2000. 47(4):776-822. doi:10.1145/347476.347484.
• [9] González-Moreno J, Hortalá-González M, López-Fraguas F, Rodríguez-Artalejo M. An approach to declarative programming based on a rewriting logic. Journal of Logic Programming, 1999. 40:47-87.
• [10] Antoy S. Constructor-based Conditional Narrowing. In: Proc. of the 3rd International ACM SIGPLAN Conference on Principles and Practice of Declarative Programming (PPDP 2001). ACM Press, 2001 pp.199-206.
• [11] Antoy S, Hanus M. Overlapping Rules and Logic Variables in Functional Logic Programs. In: Proceedings of the 22nd International Conference on Logic Programming (ICLP 2006). Springer LNCS 4079, 2006pp. 87-101.
• [12] de Dios Castro J, López-Fraguas F. Extra variables can be eliminated from functional logic programs. Electronic Notes in Theoretical Computer Science, 2007. 188:3-19.
• [13] Braßel B, Hanus M, Peemöller B, Reck F. KiCS2: A New Compiler from Curry to Haskell. In: Proc. of the 20th International Workshop on Functional and (Constraint) Logic Programming (WFLP 2011). Springer LNCS 6816, 2011 pp. 1-18. doi:10.1007/978-3-642-22531-4\_1.
• [14] Wadler P. How to Declare an Imperative. ACM Computing Surveys, 1997. 29(3):240-263.
• [15] 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’09). ACM Press, 2009 pp. 73-82. doi:10.1145/1599410.1599420.
• [16] Antoy S, Hanus M. Declarative Programming with Function Patterns. In: Proceedings of the International Symposium on Logic-based Program Synthesis and Transformation (LOPSTR’05). Springer LNCS 3901, 2005 pp. 6-22.
• [17] Antoy S, Hanus M. Default Rules for Curry. Theory and Practice of Logic Programming, 2017. 17(2):121-147. doi:10.1017/S1471068416000168.
• [18] Albert E, Hanus M, Huch F, Oliver J, Vidal G. Operational Semantics for Declarative Multi-Paradigm Languages. Journal of Symbolic Computation, 2005. 40(1):795-829.
• [19] Launchbury J. A Natural Semantics for Lazy Evaluation. In: Proc. 20th ACM Symposium on Principles of Programming Languages (POPL’93). ACM Press, 1993 pp. 144-154.
• [20] Braßel B. Implementing Functional Logic Programs by Translation into Purely Functional Programs. Ph.D. thesis, Christian-Albrechts-Universität zu Kiel, 2011.
• [21] Hanus M. CurryCheck: Checking Properties of Curry Programs. In: Proceedings of the 26th International Symposium on Logic-Based Program Synthesis and Transformation (LOPSTR 2016). Springer LNCS 10184, 2017 pp. 222-239. doi:10.1007/978-3-319-63139-4\_13.
• [22] Chitil O, McNeill D, Runciman C. Lazy Assertions. In: Proceedings of the 15th International Workshop on Implementation of Functional Languages (IFL 2003). Springer LNCS 3145, 2004 pp. 1-19.
• [23] Degen M, Thiemann P, Wehr S. True Lies: Lazy Contracts for Lazy Languages (Faithfulness is Better than Laziness). In: 4. Arbeitstagung Programmiersprachen (ATPS’09). Springer LNI 154, 2009 pp. 370; 2946-2259.
• [24] Hanus M. Improving Lazy Non-Deterministic Computations by Demand Analysis. In: Technical Communications of the 28th International Conference on Logic Programming, volume 17. Leibniz International Proceedings in Informatics (LIPIcs), 2012 pp. 130-143. doi:10.4230/LIPIcs.ICLP.2012.130.
• [25] Hanus M, Skrlac F. A Modular and Generic Analysis Server System for Functional Logic Programs. In: Proc. of the ACM SIGPLAN 2014 Workshop on Partial Evaluation and Program Manipulation (PEPM’14). ACM Press, 2014 pp. 181-188. doi:10.1145/2543728.2543744.
• [26] Antoy S, Hanus M, Libby S. Proving Non-Deterministic Computations in Agda. In: Proc. of the 24th International Workshop on Functional and (Constraint) Logic Programming (WFLP 2016), volume 234 of Electronic Proceedings in Theoretical Computer Science. Open Publishing Association, 2017 pp. 180-195. doi:10.4204/EPTCS.234.13.
• [27] Barrett C, Fontaine P, Tinelli C. The SMT-LIB Standard: Version 2.6. Technical report, Department of Computer Science, The University of Iowa, 2017. Available at www.SMT-LIB.org.
• [28] Vazou N, Seidel E, Jhala R, Vytiniotis D, Peyton Jones S. Refinement Types for Haskell. In: Proceedings of the 19th ACM SIGPLAN International Conference on Functional Programming (ICFP). ACM Press, 2014 pp. 269-282. doi:10.1145/2628136.2628161.
• [29] Claessen K, Johansson M, Rosén D, Smallbone N. TIP: Tons of Inductive Problems. In: Int. Conf. on Intelligent Computer Mathematics (CICM 2015). Springer LNCS 9150, 2015 pp. 333-337. doi:10.1007/978-3-319-20615-8\_23.
• [30] Christiansen J, Fischer S. EasyCheck - Test Data for Free. In: Proc. of the 9th International Symposium on Functional and Logic Programming (FLOPS 2008). Springer LNCS 4989, 2008 pp. 322-336.
• [31] Hanus M. Verifying Fail-Free Declarative Programs. In: Proceedings of the 20th International Symposium on Principles and Practice of Declarative Programming(PPDP 2018). ACM Press, 2018 pp. 12:1-12:13. doi:10.1145/3236950.3236957.
• [32] Stulova N, Morales J, Hermenegildo M. Reducing the Overhead of Assertion Run-time Checks via Static Analysis. In: Proc. 18th International Symposium on Principles and Practice of Declarative Programming (PPDP 2016). ACM Press, 2016 pp. 90-103.
• [33] Serrano A, López-García P, Bueno F, Hermenegildo M. Sized Type Analysis for Logic Programs. Theory and Practice of Logic Programming, 2013. 13(4-5-Online-Supplement). doi:http://static.cambridge.org/resource/id/urn:cambridge.org:id:binary:20161018085635834-0697:S1471068413000112:tlp2013011.pdf.
• [34] Xu D, Peyton Jones S, Claessen K. Static contract checking for Haskell. In: Proc. of the 36th ACM Symposium on Principles of Programming Languages (POPL 2009). 2009 pp. 41-52. doi:10.1145/1480881.1480889.
• [35] Nguyen P, Tobin-Hochstadt S, Van Horn D. Soft Contract Verification. In: Proceedings of the 19th ACM SIGPLAN International Conference on Functional Programming (ICFP 2014). ACM Press, 2014 pp. 139-152. doi:10.1145/2628136.2628156.
• [36] Vazou N, Seidel E, Jhala R. LiquidHaskell: Experience with Refinement Types in the Real World. In: Proceedings of the 2014 ACM SIGPLAN Symposium on Haskell. ACM Press, 2014 pp. 39-51. doi:10.1145/2633357.2633366.
• [37] 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’09). ACM Press, 2009 pp. 195-206.
• [38] Fähndrich M, Logozzo F. Static contract checking with Abstract Interpretation. In: Proc. of the Conference on Formal Verification of Object-oriented Software (FoVeOOS 2010). Springer LNCS 6528, 2011 pp. 10-30. doi:10.1007/978-3-642-18070-5\_2.

Uwagi

Opracowanie rekordu ze środków MNiSW, umowa Nr 461252 w ramach programu "Społeczna odpowiedzialność nauki" - moduł: Popularyzacja nauki i promocja sportu (2020).