Document Open Access Logo

Pure Methods for roDOT

Authors Vlastimil Dort , Yufeng Li, Ondřej Lhoták , Pavel Parízek

PDF
Thumbnail PDF

File

LIPIcs.ECOOP.2024.13.pdf
  • Filesize: 0.96 MB
  • 29 pages

Document Identifiers

Author Details

Vlastimil Dort
  • Charles University, Prague, Czech Republic
Yufeng Li
  • University of Cambridge, UK
Ondřej Lhoták
  • University of Waterloo, Canada
Pavel Parízek
  • Charles University, Prague, Czech Republic

Funding

This work was supported by the Czech Science Foundation project 23-06506S, and by the Czech Ministry of Education, Youth and Sports project LL2325 of the ERC.CZ programme. This research was also supported by the Natural Sciences and Engineering Research Council of Canada.

Cite AsGet BibTex

Vlastimil Dort, Yufeng Li, Ondřej Lhoták, and Pavel Parízek. Pure Methods for roDOT. In 38th European Conference on Object-Oriented Programming (ECOOP 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 313, pp. 13:1-13:29, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)
https://doi.org/10.4230/LIPIcs.ECOOP.2024.13

Abstract

Object-oriented programming languages typically allow mutation of objects, but pure methods are common too. There is great interest in recognizing which methods are pure, because it eases analysis of program behavior and allows modifying the program without changing its behavior. The roDOT calculus is a formal calculus extending DOT with reference mutability. In this paper, we explore purity conditions in roDOT and pose a SEF guarantee, by which the type system guarantees that methods of certain types are side-effect free. We use the idea from ReIm to detect pure methods by argument types. Applying this idea to roDOT required just a few changes to the type system, but necessitated re-working a significant part of the soundness proof. In addition, we state a transformation guarantee, which states that in a roDOT program, calls to SEF methods can be safely reordered without changing the outcome of the program. We proved type soundness of the updated roDOT calculus, using multiple layers of typing judgments. We proved the SEF guarantee by applying the Immutability guarantee, and the transformation guarantee by applying the SEF guarantee within a framework for reasoning about safe transformations of roDOT programs. All proofs are mechanized in Coq.

Subject Classification

ACM Subject Classification
  • Software and its engineering → Formal language definitions
  • Software and its engineering → Object oriented languages
Keywords
  • type systems
  • DOT calculus
  • pure methods

Metrics

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

Related Versions

Supplementary Materials

References

  1. Martín Abadi and Luca Cardelli. A Theory of Objects. Monographs in Computer Science. Springer, 1996. URL: https://doi.org/10.1007/978-1-4419-8598-9.
  2. Nada Amin, Samuel Grütter, Martin Odersky, Tiark Rompf, and Sandro Stucki. The essence of dependent object types. In Sam Lindley, Conor McBride, Philip W. Trinder, and Donald Sannella, editors, A List of Successes That Can Change the World - Essays Dedicated to Philip Wadler on the Occasion of His 60th Birthday, volume 9600 of Lecture Notes in Computer Science, pages 249-272. Springer, 2016. URL: https://doi.org/10.1007/978-3-319-30936-1_14.
  3. Nada Amin, Tiark Rompf, and Martin Odersky. Foundations of path-dependent types. In Andrew P. Black and Todd D. Millstein, editors, Proceedings of the 2014 ACM International Conference on Object Oriented Programming Systems Languages & Applications, OOPSLA 2014, part of SPLASH 2014, Portland, OR, USA, October 20-24, 2014, OOPSLA '14, pages 233-249. ACM, 2014. URL: https://doi.org/10.1145/2660193.2660216.
  4. Yuyan Bao, Guannan Wei, Oliver Bračevac, Yuxuan Jiang, Qiyang He, and Tiark Rompf. Reachability types: Tracking aliasing and separation in higher-order functional programs. Proc. ACM Program. Lang., 5(OOPSLA), October 2021. URL: https://doi.org/10.1145/3485516.
  5. Mike Barnett, David A Naumann, Wolfram Schulte, and Qi Sun. 99.44% pure: Useful abstractions in specifications. In ECOOP workshop on formal techniques for Java-like programs (FTfJP), 2004. Google Scholar
  6. William C. Benton and Charles N. Fischer. Mostly-functional behavior in Java programs. In Neil D. Jones and Markus Müller-Olm, editors, Verification, Model Checking, and Abstract Interpretation, 10th International Conference, VMCAI 2009, Savannah, GA, USA, January 18-20, 2009. Proceedings, volume 5403 of Lecture Notes in Computer Science, pages 29-43. Springer, 2009. URL: https://doi.org/10.1007/978-3-540-93900-9_7.
  7. Aleksander Boruch-Gruszecki, Martin Odersky, Edward Lee, Ondřej Lhoták, and Jonathan Brachthäuser. Capturing types. ACM Trans. Program. Lang. Syst., 45(4), November 2023. URL: https://doi.org/10.1145/3618003.
  8. Oliver Bračevac, Guannan Wei, Songlin Jia, Supun Abeysinghe, Yuxuan Jiang, Yuyan Bao, and Tiark Rompf. Graph IRs for impure higher-order languages: Making aggressive optimizations affordable with precise effect dependencies. Proc. ACM Program. Lang., 7(OOPSLA2), October 2023. URL: https://doi.org/10.1145/3622813.
  9. The Checker Framework Manual: Custom pluggable types for Java. URL: https://checkerframework.org/manual/#initialization-checker, 2022.
  10. The Checker Framework Manual: Custom pluggable types for Java. URL: https://checkerframework.org/manual/#purity-checker, 2022.
  11. Lars Ræder Clausen. A Java bytecode optimizer using side-effect analysis. Concurrency: Practice and Experience, 9(11):1031-1045, 1997. URL: https://doi.org/10.1002/(SICI)1096-9128(199711)9:11<1031::AID-CPE354>3.0.CO;2-O.
  12. Vlastimil Dort and Ondřej Lhoták. Reference mutability for DOT. In Robert Hirschfeld and Tobias Pape, editors, 34th European Conference on Object-Oriented Programming, ECOOP 2020, November 15-17, 2020, Berlin, Germany (Virtual Conference), volume 166 of LIPIcs, pages 18:1-18:28. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2020. URL: https://doi.org/10.4230/LIPIcs.ECOOP.2020.18.
  13. Vlastimil Dort, Yufeng Li, Ondřej Lhoták, and Pavel Parízek. Pure methods for roDOT (an extended version). Technical Report D3S-TR-2024-01, Dep. of Distributed and Dependable Systems, Charles University, 2024. URL: https://d3s.mff.cuni.cz/files/publications/dort_pure_report_2024.pdf.
  14. Michael D. Ernst. Annotation type Pure. https://checkerframework.org/api/org/checkerframework/dataflow/qual/Pure.html, 2022.
  15. Manuel Fähndrich, Michael Barnett, and Francesco Logozzo. Embedded contract languages. In Sung Y. Shin, Sascha Ossowski, Michael Schumacher, Mathew J. Palakal, and Chih-Cheng Hung, editors, Proceedings of the 2010 ACM Symposium on Applied Computing (SAC), Sierre, Switzerland, March 22-26, 2010, pages 2103-2110. ACM, 2010. URL: https://doi.org/10.1145/1774088.1774531.
  16. Matthew Finifter, Adrian Mettler, Naveen Sastry, and David A. Wagner. Verifiable functional purity in Java. In Peng Ning, Paul F. Syverson, and Somesh Jha, editors, Proceedings of the 2008 ACM Conference on Computer and Communications Security, CCS 2008, Alexandria, Virginia, USA, October 27-31, 2008, pages 161-174. ACM, 2008. URL: https://doi.org/10.1145/1455770.1455793.
  17. Paolo G. Giarrusso, Léo Stefanesco, Amin Timany, Lars Birkedal, and Robbert Krebbers. Scala step-by-step: soundness for DOT with step-indexed logical relations in Iris. Proc. ACM Program. Lang., 4(ICFP):114:1-114:29, 2020. URL: https://doi.org/10.1145/3408996.
  18. James Gosling, Bill Joy, Guy Steele, Gilad Bracha, and Alex Buckley. The Java® language specification, Java SE 8 edition. https://docs.oracle.com/javase/specs/jls/se8/html/jls-8.html#jls-8.4.1, 2022.
  19. Wei Huang, Ana Milanova, Werner Dietl, and Michael D. Ernst. ReIm & ReImInfer: checking and inference of reference immutability and method purity. In Proceedings of the 27th Annual ACM SIGPLAN Conference on Object-Oriented Programming, Systems, Languages, and Applications, OOPSLA 2012, part of SPLASH 2012, Tucson, AZ, USA, October 21-25, 2012, OOPSLA '12, pages 879-896. Association for Computing Machinery, 2012. URL: https://doi.org/10.1145/2384616.2384680.
  20. JML reference manual: Class and interface member declarations. https://www.cs.ucf.edu/~leavens/JML/jmlrefman/jmlrefman_7.html#SEC60, 2022.
  21. Ifaz Kabir. themaplelab / dot-public: A simpler syntactic soundness proof for dependent object types. URL: https://github.com/themaplelab/dot-public/tree/master/dot-simpler.
  22. Ifaz Kabir and Ondřej Lhoták. κDOT: scaling DOT with mutation and constructors. In Proceedings of the 9th ACM SIGPLAN International Symposium on Scala, SCALA@ICFP 2018, St. Louis, MO, USA, September 28, 2018, pages 40-50, 2018. URL: https://doi.org/10.1145/3241653.3241659.
  23. Ifaz Kabir, Yufeng Li, and Ondrej Lhoták. ιDOT: a DOT calculus with object initialization. Proc. ACM Program. Lang., 4(OOPSLA):208:1-208:28, 2020. URL: https://doi.org/10.1145/3428276.
  24. Darya Melicher, Anlun Xu, Valerie Zhao, Alex Potanin, and Jonathan Aldrich. Bounded abstract effects. ACM Trans. Program. Lang. Syst., 44(1), January 2022. URL: https://doi.org/10.1145/3492427.
  25. David A. Naumann. Observational purity and encapsulation. In Maura Cerioli, editor, Fundamental Approaches to Software Engineering, 8th International Conference, FASE 2005, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2005, Edinburgh, UK, April 4-8, 2005, Proceedings, volume 3442 of Lecture Notes in Computer Science, pages 190-204. Springer, 2005. URL: https://doi.org/10.1007/978-3-540-31984-9_15.
  26. Jens Nicolay, Quentin Stiévenart, Wolfgang De Meuter, and Coen De Roover. Purity analysis for JavaScript through abstract interpretation. Journal of Software: Evolution and Process, 29(12), 2017. URL: https://doi.org/10.1002/smr.1889.
  27. Martin Odersky, Aleksander Boruch-Gruszecki, Jonathan Immanuel Brachthäuser, Edward Lee, and Ondřej Lhoták. Safer exceptions for Scala. In Proceedings of the 12th ACM SIGPLAN International Symposium on Scala, SCALA 2021, pages 1-11, New York, NY, USA, 2021. Association for Computing Machinery. URL: https://doi.org/10.1145/3486610.3486893.
  28. Martin Odersky, Aleksander Boruch-Gruszecki, Edward Lee, Jonathan Brachthäuser, and Ondřej Lhoták. Scoped capabilities for polymorphic effects, 2022. URL: https://arxiv.org/abs/2207.03402.
  29. David J. Pearce. JPure: A modular purity system for Java. In Jens Knoop, editor, Compiler Construction - 20th International Conference, CC 2011, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2011, Saarbrücken, Germany, March 26-April 3, 2011. Proceedings, volume 6601 of Lecture Notes in Computer Science, pages 104-123. Springer, 2011. URL: https://doi.org/10.1007/978-3-642-19861-8_7.
  30. Marianna Rapoport, Ifaz Kabir, Paul He, and Ondřej Lhoták. A simple soundness proof for dependent object types. Proc. ACM Program. Lang., 1(OOPSLA):46:1-46:27, 2017. URL: https://doi.org/10.1145/3133870.
  31. Marianna Rapoport and Ondrej Lhoták. A path to DOT: formalizing fully path-dependent types. Proc. ACM Program. Lang., 3(OOPSLA):145:1-145:29, 2019. URL: https://doi.org/10.1145/3360571.
  32. Marianna Rapoport and Ondřej Lhoták. Mutable WadlerFest DOT. In Proceedings of the 19th Workshop on Formal Techniques for Java-like Programs, Barcelona , Spain, June 20, 2017, pages 7:1-7:6. ACM Press, 2017. URL: https://doi.org/10.1145/3103111.3104036.
  33. Tiark Rompf and Nada Amin. Type soundness for dependent object types (DOT). In Eelco Visser and Yannis Smaragdakis, editors, Proceedings of the 2016 ACM SIGPLAN International Conference on Object-Oriented Programming, Systems, Languages, and Applications, OOPSLA 2016, part of SPLASH 2016, Amsterdam, The Netherlands, October 30 - November 4, 2016, OOPSLA '16, pages 624-641. ACM, 2016. URL: https://doi.org/10.1145/2983990.2984008.
  34. Atanas Rountev. Precise identification of side-effect-free methods in Java. In 20th International Conference on Software Maintenance (ICSM 2004), 11-17 September 2004, Chicago, IL, USA, pages 82-91. IEEE Computer Society, 2004. URL: https://doi.org/10.1109/ICSM.2004.1357793.
  35. Lukas Rytz, Nada Amin, and Martin Odersky. A flow-insensitive, modular effect system for purity. In Werner Dietl, editor, Proceedings of the 15th Workshop on Formal Techniques for Java-like Programs, FTfJP 2013, Montpellier, France, July 1, 2013, FTfJP '13, pages 4:1-4:7. ACM, 2013. URL: https://doi.org/10.1145/2489804.2489808.
  36. Amr Sabry and Matthias Felleisen. Reasoning about programs in continuation-passing style. In Proceedings of the 1992 ACM Conference on LISP and Functional Programming, LFP '92, pages 288-298, New York, NY, USA, 1992. Association for Computing Machinery. URL: https://doi.org/10.1145/141471.141563.
  37. Alexandru Salcianu and Martin Rinard. A combined pointer and purity analysis for Java programs. Technical report, Massachusetts Institute of Technology Computer Science and Artificial Intelligence Laboratory, 2004. URL: https://dspace.mit.edu/handle/1721.1/30470.
  38. Alexandru Salcianu and Martin C. Rinard. Purity and side effect analysis for Java programs. In Radhia Cousot, editor, Verification, Model Checking, and Abstract Interpretation, 6th International Conference, VMCAI 2005, Paris, France, January 17-19, 2005, Proceedings, volume 3385 of Lecture Notes in Computer Science, pages 199-215. Springer, 2005. URL: https://doi.org/10.1007/978-3-540-30579-8_14.
  39. Guannan Wei, Oliver Bračevac, Songlin Jia, Yuyan Bao, and Tiark Rompf. Polymorphic reachability types: Tracking freshness, aliasing, and separation in higher-order generic programs. Proc. ACM Program. Lang., 8(POPL), January 2024. URL: https://doi.org/10.1145/3632856.
  40. Haiying Xu, Christopher J. F. Pickett, and Clark Verbrugge. Dynamic purity analysis for Java programs. In Manuvir Das and Dan Grossman, editors, Proceedings of the 7th ACM SIGPLAN-SIGSOFT Workshop on Program Analysis for Software Tools and Engineering, PASTE'07, San Diego, California, USA, June 13-14, 2007, pages 75-82. ACM, 2007. URL: https://doi.org/10.1145/1251535.1251548.
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