Document Open Access Logo

On Improving Run-time Checking in Dynamic Languages

Author Nataliia Stulova

PDF
Thumbnail PDF

File

OASIcs.ICLP.2017.15.pdf
  • Filesize: 0.52 MB
  • 10 pages

Document Identifiers

Author Details

Nataliia Stulova

Cite AsGet BibTex

Nataliia Stulova. On Improving Run-time Checking in Dynamic Languages. In Technical Communications of the 33rd International Conference on Logic Programming (ICLP 2017). Open Access Series in Informatics (OASIcs), Volume 58, pp. 15:1-15:10, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)
https://doi.org/10.4230/OASIcs.ICLP.2017.15

Abstract

In order to detect incorrect program behaviors, a number of approaches have been proposed, which include a combination of language-level constructs (procedure-level annotations such as assertions/contracts, gradual types, etc.) and associated tools (such as static code analyzers and run-time verification frameworks). However, it is often the case that these constructs and tools are not used to their full extent in practice due to a number of limitations such as excessive run-time overhead and/or limited expressiveness. The issue is especially prominent in the context of dynamic languages without an underlying strong type system, such as Prolog. In our work we propose several practical solutions for minimizing the run-time overhead associated with assertion-based verification while keeping the correctness guarantees provided by run-time checks. We present the solutions in the context of the Ciao system, where a combination of an abstract interpretation-based static analyzer and run-time verification framework is available, although our proposals can be straightforwardly adapted to any other similar system.
Keywords
  • Runtime Verification
  • Assertions
  • Prolog
  • Logic Programming

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

References

  1. C. Beierle, R. Kloos, and G. Meyer. A Pragmatic Type Concept for Prolog Supporting Polymorphism, Subtyping, and Meta-Programming. In Proc. of the ICLP'99 Workshop on Verification of Logic Programs, Las Cruces, Electronic Notes in Theoretical Computer Science, volume 30, issue 1. Elsevier, 2000. URL: http://www.elsevier.nl/locate/entcs/volume30.html.
  2. F. Bueno, P. Deransart, W. Drabent, G. Ferrand, M. Hermenegildo, J. Maluszynski, and G. Puebla. On the Role of Semantic Approximations in Validation and Diagnosis of Constraint Logic Programs. In Proc. of the 3rd. Int'l Workshop on Automated Debugging-AADEBUG'97, pages 155-170, Linköping, Sweden, May 1997. U. of Linköping Press. URL: ftp://cliplab.org/pub/papers/aadebug_discipldeliv.ps.gz.
  3. D. Cabeza and M. Hermenegildo. A New Module System for Prolog. In International Conference on Computational Logic, CL2000, number 1861 in LNAI, pages 131-148. Springer-Verlag, July 2000. Google Scholar
  4. D. Cabeza, M. Hermenegildo, and J. Lipton. Hiord: A Type-Free Higher-Order Logic Programming Language with Predicate Abstraction. In Ninth Asian Computing Science Conference (ASIAN'04), number 3321 in LNCS, pages 93-108. Springer-Verlag, December 2004. Google Scholar
  5. Robert Cartwright and Mike Fagan. Soft Typing. In Programming Language Design and Implementation (PLDI 1991), pages 278-292. SIGPLAN, ACM, 1991. Google Scholar
  6. Cisco Systems. ECLIPSE User Manual, 2006. Google Scholar
  7. P.W. Dart and J. Zobel. Efficient Run-Time Type Checking of Typed Logic Programs. Journal of Logic Programming, 14:31-69, October 1992. Google Scholar
  8. S. Dietrich. Extension Tables for Recursive Query Evaluation. PhD thesis, Departament of Computer Science, State University of New York, 1987. Google Scholar
  9. Christos Dimoulas and Matthias Felleisen. On contract satisfaction in a higher-order world. ACM Trans. Program. Lang. Syst., 33(5):16, 2011. URL: http://dx.doi.org/10.1145/2039346.2039348.
  10. W. Drabent, S. Nadjm-Tehrani, and J. Małuszyński. The Use of Assertions in Algorithmic Debugging. In Proceedings of the Intl. Conf. on Fifth Generation Computer Systems, pages 573-581, 1988. Google Scholar
  11. Manuel Fähndrich and Francesco Logozzo. Static contract checking with abstract interpretation. In Proceedings of the 2010 International Conference on Formal Verification of Object-oriented Software, volume 6528 of Lecture Notes in Computer Science, pages 10-30, Berlin, Heidelberg, 2011. Springer-Verlag. URL: http://dl.acm.org/citation.cfm?id=1949303.1949305.
  12. Robert Bruce Findler and Matthias Felleisen. Contracts for higher-order functions. In Mitchell Wand and Simon L. Peyton Jones, editors, ICFP, pages 48-59. ACM, 2002. URL: http://dx.doi.org/10.1145/581478.581484.
  13. M. Hermenegildo, G. Puebla, and F. Bueno. Using Global Analysis, Partial Specifications, and an Extensible Assertion Language for Program Validation and Debugging. In K. R. Apt, V. Marek, M. Truszczynski, and D. S. Warren, editors, The Logic Programming Paradigm: a 25-Year Perspective, pages 161-192. Springer-Verlag, July 1999. Google Scholar
  14. M. V. Hermenegildo, F. Bueno, M. Carro, P. López, E. Mera, J.F. Morales, and G. Puebla. An Overview of Ciao and its Design Philosophy. Theory and Practice of Logic Programming, 12(1-2):219-252, January 2012. http://arxiv.org/abs/1102.5497. URL: http://dx.doi.org/10.1017/S1471068411000457.
  15. Emmanouil Koukoutos and Viktor Kuncak. Checking Data Structure Properties Orders of Magnitude Faster. In Borzoo Bonakdarpour and Scott A. Smolka, editors, Runtime Verification, volume 8734 of Lecture Notes in Computer Science, pages 263-268. Springer International Publishing, 2014. URL: http://dx.doi.org/10.1007/978-3-319-11164-3_22.
  16. Claude Laï. Assertions with Constraints for CLP Debugging. In Pierre Deransart, Manuel V. Hermenegildo, and Jan Maluszynski, editors, Analysis and Visualization Tools for Constraint Programming, volume 1870 of Lecture Notes in Computer Science, pages 109-120. Springer, 2000. URL: http://dx.doi.org/10.1007/10722311_4.
  17. Leslie Lamport and Lawrence C. Paulson. Should your specification language be typed? ACM Transactions on Programming Languages and Systems, 21(3):502-526, May 1999. Google Scholar
  18. Gary T. Leavens, K. Rustan M. Leino, and Peter Müller. Specification and verification challenges for sequential object-oriented programs. Formal Asp. Comput., 19(2):159-189, 2007. URL: http://dx.doi.org/10.1007/s00165-007-0026-7.
  19. E. Mera, P. López-García, and M. Hermenegildo. Integrating Software Testing and Run-Time Checking in an Assertion Verification Framework. In 25th Int'l. Conference on Logic Programming (ICLP'09), volume 5649 of LNCS, pages 281-295. Springer-Verlag, July 2009. Google Scholar
  20. E. Mera, T. Trigo, P. López-García, and M. Hermenegildo. Profiling for Run-Time Checking of Computational Properties and Performance Debugging. In Practical Aspects of Declarative Languages (PADL'11), volume 6539 of Lecture Notes in Computer Science, pages 38-53. Springer-Verlag, January 2011. Google Scholar
  21. Edison Mera and Jan Wielemaker. Porting and refactoring Prolog programs: the PROSYN case study. TPLP, 13(4-5-Online-Supplement), 2013. Google Scholar
  22. K. Muthukumar and M. Hermenegildo. Compile-time Derivation of Variable Dependency Using Abstract Interpretation. Journal of Logic Programming, 13(2/3):315-347, July 1992. Google Scholar
  23. Gopalan Nadathur and Dale Miller. Higher-Order Logic Programming. In D. Gabbay, C. Hogger, and A. Robinson, editors, Handbook of Logic in Artificial Intelligence and Logic Programming, volume 5. Oxford University Press, 1998. Google Scholar
  24. G. Puebla, F. Bueno, and M. Hermenegildo. Combined Static and Dynamic Assertion-Based Debugging of Constraint Logic Programs. In Logic-based Program Synthesis and Transformation (LOPSTR'99), number 1817 in LNCS, pages 273-292. Springer-Verlag, March 2000. Google Scholar
  25. Vítor Santos Costa, Luís Damas, and Ricardo Rocha. The YAP Prolog System. Theory and Practice of Logic Programming, 2011. http://arxiv.org/abs/1102.3896v1. Google Scholar
  26. N. Stulova, J. F. Morales, and M. V. Hermenegildo. Assertion-based Debugging of Higher-Order (C)LP Programs. In 16th Int'l. ACM SIGPLAN Symposium on Principles and Practice of Declarative Programming (PPDP'14). ACM Press, September 2014. Google Scholar
  27. N. Stulova, J. F. Morales, and M. V. Hermenegildo. Practical Run-time Checking via Unobtrusive Property Caching. Theory and Practice of Logic Programming, 31st Int'l. Conference on Logic Programming (ICLP'15) Special Issue, 15(04-05):726-741, September 2015. URL: http://arxiv.org/abs/1507.05986.
  28. N. Stulova, J. F. Morales, and M. V. Hermenegildo. Reducing the Overhead of Assertion Run-time Checks via static analysis. In 18th Int'l. ACM SIGPLAN Symposium on Principles and Practice of Declarative Programming (PPDP'16), pages 90-103. ACM Press, September 2016. Google Scholar
  29. N. Stulova, J. F. Morales, and M. V. Hermenegildo. Term Hiding and its Impact on Run-time Check Simplification (Extended Abstract). In Proceedings of the Technical Communications of the 33rd International Conference on Logic Programming (ICLP 2017), Melbourne, Australia, August 28 - September 1, 2017. OASIcs, August 2017. Google Scholar
  30. Swedish Institute for Computer Science, PO Box 1263, S-164 28 Kista, Sweden. SICStus Prolog User’s Manual, 4.1.1 edition, December 2009. Available from http://www.sics.se/sicstus/. Google Scholar
  31. Terrance Swift and David Scott Warren. XSB: Extending Prolog with Tabled Logic Programming. TPLP, 12(1-2):157-187, 2012. Google Scholar
  32. Asumu Takikawa, Daniel Feltey, Earl Dean, Matthew Flatt, Robert Bruce Findler, Sam Tobin-Hochstadt, and Matthias Felleisen. Towards practical gradual typing. In John Tang Boyland, editor, 29th European Conference on Object-Oriented Programming, ECOOP 2015, July 5-10, 2015, Prague, Czech Republic, volume 37 of LIPIcs, pages 4-27. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 2015. URL: http://www.dagstuhl.de/dagpub/978-3-939897-86-6, URL: http://dx.doi.org/10.4230/LIPIcs.ECOOP.2015.4.
  33. H. Tamaki and M. Sato. OLD Resolution with Tabulation. In Third International Conference on Logic Programming, pages 84-98, London, 1986. Lecture Notes in Computer Science, Springer-Verlag. Google Scholar
  34. Sam Tobin-Hochstadt and Matthias Felleisen. The Design and Implementation of Typed Scheme. In George C. Necula and Philip Wadler, editors, Proceedings of the 35th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2008, San Francisco, California, USA, January 7-12, 2008, pages 395-406. ACM, 2008. URL: http://dx.doi.org/10.1145/1328438.1328486.
  35. D.H.D. Warren. Higher-order extensions to Prolog: are they needed? In J.E. Hayes, Donald Michie, and Y-H. Pao, editors, Machine Intelligence 10, pages 441-454. Ellis Horwood Ltd., Chicester, England, 1982. Google Scholar
  36. R. Warren, M. Hermenegildo, and S. K. Debray. On the Practicality of Global Flow Analysis of Logic Programs. In Fifth International Conference and Symposium on Logic Programming, pages 684-699. MIT Press, August 1988. Google Scholar
  37. J. Wielemaker. The SWI-Prolog User’s Manual 5.9.9, 2010. Available from http://www.swi-prolog.org. Google Scholar
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact