Document Open Access Logo

Behavioural Up/down Casting For Statically Typed Languages

Authors Lorenzo Bacchiani , Mario Bravetti , Marco Giunti , João Mota , António Ravara

PDF
Thumbnail PDF

File

LIPIcs.ECOOP.2024.5.pdf
  • Filesize: 1.23 MB
  • 28 pages

Document Identifiers

Author Details

Lorenzo Bacchiani
  • University of Bologna, Italy
Mario Bravetti
  • University of Bologna, Italy
Marco Giunti
  • University of Oxford, UK
João Mota
  • NOVA LINCS, Nova University Lisbon, Portugal
  • NOVA School of Science and Technology, Caparica, Portugal
António Ravara
  • NOVA LINCS, Nova University Lisbon, Portugal
  • NOVA School of Science and Technology, Caparica, Portugal

Funding

This work was partially supported by the EU H2020 RISE programme under the Marie Skłodowska-Curie grant agreement No. 778233 (BehAPI).
  • Giunti, Marco: EPSRC (EP/T006544/2).
  • Mota, João: NOVA LINCS (UIDB/04516/2020) via the Portuguese Fundação para a Ciência e a Tecnologia (doi: 10.54499/2021.05297.BD).

Cite AsGet BibTex

Lorenzo Bacchiani, Mario Bravetti, Marco Giunti, João Mota, and António Ravara. Behavioural Up/down Casting For Statically Typed Languages. In 38th European Conference on Object-Oriented Programming (ECOOP 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 313, pp. 5:1-5:28, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)
https://doi.org/10.4230/LIPIcs.ECOOP.2024.5

Abstract

We provide support for polymorphism in static typestate analysis for object-oriented languages with upcasts and downcasts. Recent work has shown how typestate analysis can be embedded in the development of Java programs to obtain safer behaviour at runtime, e.g., absence of null pointer errors and protocol completion. In that approach, inheritance is supported at the price of limiting casts in source code, thus only allowing those at the beginning of the protocol, i.e., immediately after objects creation, or at the end, and in turn seriously affecting the applicability of the analysis. In this paper, we provide a solution to this open problem in typestate analysis by introducing a theory based on a richer data structure, named typestate tree, which supports upcast and downcast operations at any point of the protocol by leveraging union and intersection types. The soundness of the typestate tree-based approach has been mechanised in Coq. The theory can be applied to most object-oriented languages statically analysable through typestates, thus opening new scenarios for acceptance of programs exploiting inheritance and casting. To defend this thesis, we show an application of the theory, by embedding the typestate tree mechanism in a Java-like object-oriented language, and proving its soundness.

Subject Classification

ACM Subject Classification
  • Theory of computation → Type theory
  • Theory of computation → Object oriented constructs
  • Theory of computation → Program verification
Keywords
  • Behavioural types
  • object-oriented programming
  • subtyping
  • cast
  • typestates

Metrics

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

Supplementary Materials

References

  1. Frances E Allen. Control flow analysis. ACM Sigplan Notices, 5(7):1-19, 1970. URL: https://doi.org/10.1145/390013.808479.
  2. Davide Ancona, Viviana Bono, Mario Bravetti, Joana Campos, Giuseppe Castagna, Pierre-Malo Deniélou, Simon J. Gay, Nils Gesbert, Elena Giachino, Raymond Hu, Einar Broch Johnsen, Francisco Martins, Viviana Mascardi, Fabrizio Montesi, Rumyana Neykova, Nicholas Ng, Luca Padovani, Vasco T. Vasconcelos, and Nobuko Yoshida. Behavioral Types in Programming Languages. Found. Trends Program. Lang., 3(2-3):95-230, 2016. URL: https://doi.org/10.1561/2500000031.
  3. Lorenzo Bacchiani, Mario Bravetti, Marco Giunti, João Mota, and António Ravara. A Java typestate checker supporting inheritance. Science of Computer Programming, 221:102844, 2022. URL: https://doi.org/10.1016/j.scico.2022.102844.
  4. Lorenzo Bacchiani, Mario Bravetti, Julien Lange, and Gianluigi Zavattaro. A Session Subtyping Tool. In Proc. of Coordination Models and Languages (COORDINATION), volume 12717 of Lecture Notes in Computer Science, pages 90-105. Springer, 2021. URL: https://doi.org/10.1007/978-3-030-78142-2_6.
  5. Franco Barbanera, Mariangiola Dezani-Ciancaglini, and Ugo de'Liguoro. Intersection and Union Types: Syntax and Semantics. Information and Computation, 119:202-230, 1995. Google Scholar
  6. Nels E Beckman, Duri Kim, and Jonathan Aldrich. An Empirical Study of Object Protocols in the Wild. In Proc. of European Conference on Object-Oriented Programming (ECOOP), pages 2-26. Springer, 2011. URL: https://doi.org/10.1007/978-3-642-22655-7_2.
  7. Kevin Bierhoff and Jonathan Aldrich. Lightweight object specification with typestates. In Proceedings of the 10th European Software Engineering Conference held jointly with 13th ACM SIGSOFT International Symposium on Foundations of Software Engineering, 2005, pages 217-226. ACM, 2005. URL: https://doi.org/10.1145/1081706.1081741.
  8. Kevin Bierhoff and Jonathan Aldrich. Modular typestate checking of aliased objects. In Proceedings of the 22nd Annual ACM SIGPLAN Conference on Object-Oriented Programming, Systems, Languages, and Applications, OOPSLA 2007, pages 301-320. ACM, 2007. URL: https://doi.org/10.1145/1297027.1297050.
  9. Stefan Blom and Marieke Huisman. The VerCors Tool for Verification of Concurrent Programs. In Cliff B. Jones, Pekka Pihlajasaari, and Jun Sun, editors, FM 2014: Formal Methods - 19th International Symposium. Proceedings, volume 8442 of Lecture Notes in Computer Science, pages 127-131. Springer, 2014. URL: https://doi.org/10.1007/978-3-319-06410-9_9.
  10. Jelle Bouma, Stijn de Gouw, and Sung-Shik Jongmans. Multiparty Session Typing in Java, Deductively. In Sriram Sankaranarayanan and Natasha Sharygina, editors, Tools and Algorithms for the Construction and Analysis of Systems - 29th International Conference, TACAS 2023, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2022, Proceedings, Part II, volume 13994 of Lecture Notes in Computer Science, pages 19-27. Springer, 2023. URL: https://doi.org/10.1007/978-3-031-30820-8_3.
  11. Mario Bravetti, Adrian Francalanza, Iaroslav Golovanov, Hans Hüttel, Mathias Jakobsen, Mikkel Kettunen, and António Ravara. Behavioural Types for Memory and Method Safety in a Core Object-Oriented Language. In Asian Symposium on Programming Languages and Systems, volume 12470 of Lecture Notes in Computer Science, pages 105-124. Springer, 2020. URL: https://doi.org/10.1007/978-3-030-64437-6_6.
  12. Michael J. Coblenz, Reed Oei, Tyler Etzel, Paulette Koronkevich, Miles Baker, Yannick Bloem, Brad A. Myers, Joshua Sunshine, and Jonathan Aldrich. Obsidian: Typestate and Assets for Safer Blockchain Programming. ACM Trans. Program. Lang. Syst., 42(3):14:1-14:82, 2020. URL: https://doi.org/10.1145/3417516.
  13. Robert DeLine and Manuel Fähndrich. Typestates for Objects. In Martin Odersky, editor, ECOOP 2004 - Object-Oriented Programming, 18th European Conference, Proceedings, volume 3086 of Lecture Notes in Computer Science, pages 465-490. Springer, 2004. URL: https://doi.org/10.1007/978-3-540-24851-4_21.
  14. Edsger W. Dijkstra. The humble programmer, 1972. ACM Turing Award acceptance speech. URL: https://doi.org/10.1145/355604.361591.
  15. Ronald Garcia, Éric Tanter, Roger Wolff, and Jonathan Aldrich. Foundations of Typestate-Oriented Programming. ACM Transactions on Programming Languages and Systems, 36(4):12, 2014. URL: https://doi.org/10.1145/2629609.
  16. Simon J. Gay and Malcolm Hole. Types and Subtypes for Client-Server Interactions. In Proc. of Programming Languages and Systems (ESOP), volume 1576 of Lecture Notes in Computer Science, pages 74-90. Springer, 1999. URL: https://doi.org/10.1007/3-540-49099-X_6.
  17. Simon J. Gay and Malcolm Hole. Subtyping for session types in the pi-calculus. Acta Informatica, 42(2-3):191-225, 2005. URL: https://doi.org/10.1007/s00236-005-0177-z.
  18. Simon J. Gay, Vasco Thudichum Vasconcelos, António Ravara, Nils Gesbert, and Alexandre Z. Caldeira. Modular session types for distributed object-oriented programming. In Proceedings of the 37th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2010, pages 299-312. ACM, 2010. URL: https://doi.org/10.1145/1706299.1706335.
  19. Tony Hoare. Null References: The Billion Dollar Mistake, 2009. Presentation at QCon London. URL: https://tinyurl.com/eyipowm4.
  20. Kohei Honda, Nobuko Yoshida, and Marco Carbone. Multiparty Asynchronous Session Type. J. ACM, 63(1):9:1-9:67, 2016. URL: https://doi.org/10.1145/2827695.
  21. Jez Humble and David Farley. Continuous Delivery: Reliable Software Releases Through Build, Test, and Deployment Automation. Addison-Wesley Professional, 2010. Google Scholar
  22. Hans Hüttel, Ivan Lanese, Vasco T. Vasconcelos, Luís Caires, Marco Carbone, Pierre-Malo Deniélou, Dimitris Mostrous, Luca Padovani, António Ravara, Emilio Tuosto, Hugo Torres Vieira, and Gianluigi Zavattaro. Foundations of Session Types and Behavioural Contracts. ACM Comput. Surv., 49(1):3:1-3:36, 2016. URL: https://doi.org/10.1145/2873052.
  23. Mathias Jakobsen, Alice Ravier, and Ornela Dardha. Papaya: Global Typestate Analysis of Aliased Objects. In Proceedings of the 23rd International Symposium on Principles and Practice of Declarative Programming (PPDP'21), pages 19:1-19:13. ACM, 2021. URL: https://doi.org/10.1145/3479394.3479414.
  24. Dimitrios Kouzapas, Ornela Dardha, Roly Perera, and Simon J Gay. Typechecking protocols with Mungo and StMungo. In Proc. of Principles and Practice of Declarative Programming (PPDP), pages 146-159. ACM, 2016. URL: https://doi.org/10.1145/2967973.2968595.
  25. Luis Mastrangelo, Matthias Hauswirth, and Nathaniel Nystrom. Casting about in the dark: an empirical study of cast operations in Java programs. Proc. ACM Program. Lang., 3(OOPSLA):158:1-158:31, 2019. URL: https://doi.org/10.1145/3360584.
  26. João Mota, Marco Giunti, and António Ravara. On Using VeriFast, VerCors, Plural, and KeY to Check Object Usage (Experience Paper). In 37th European Conference on Object-Oriented Programming, ECOOP 2023, July 17-21, 2023, Seattle, Washington, United States, volume 263 of LIPIcs, pages 40:1-40:29. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2023. URL: https://doi.org/10.4230/LIPICS.ECOOP.2023.40.
  27. Fabian Muehlboeck and Ross Tate. Empowering union and intersection types with integrated subtyping. Proc. ACM Program. Lang., 2(OOPSLA):112:1-112:29, 2018. URL: https://doi.org/10.1145/3276482.
  28. Rumyana Neykova and Nobuko Yoshida. Featherweight Scribble. In Michele Boreale, Flavio Corradini, Michele Loreti, and Rosario Pugliese, editors, Models, Languages, and Tools for Concurrent and Distributed Programming - Essays Dedicated to Rocco De Nicola on the Occasion of His 65th Birthday, volume 11665 of Lecture Notes in Computer Science, pages 236-259. Springer, 2019. URL: https://doi.org/10.1007/978-3-030-21485-2_14.
  29. Jens Palsberg and Pavlopoulou Chirstina. From Polyvariant flow information to intersection and union types. Journal of Functional Programming, 11(3):263-317, 2001. URL: https://doi.org/10.1017/S095679680100394X.
  30. Matthew M Papi, Mahmood Ali, Telmo Luis Correa Jr, Jeff H Perkins, and Michael D Ernst. Practical pluggable types for Java. In Proc. of Software Testing and Analysis (ISSTA), pages 201-212. ACM, 2008. URL: https://doi.org/10.1145/1390630.1390656.
  31. R. E. Strom and S. Yemini. Typestate: A programming language concept for enhancing software reliability. IEEE Transactions on Software Engineering, SE-12(1):157-171, 1986. URL: https://doi.org/10.1109/TSE.1986.6312929.
  32. Vasco T. Vasconcelos. Sessions, from Types to Programming Languages. Bull. EATCS, 103:53-73, 2011. URL: http://eatcs.org/beatcs/index.php/beatcs/article/view/136.
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