Formal Semantics for Java-like Languages and Research Opportunities

Samuel da Silva Feitosa, Rodrigo Geraldo Ribeiro, Andre Rauber Du Bois

Abstract


The objective of this paper is twofold: first, we discuss the state of art on Java-like semantics, focusing on those that provide formal specification using operational semantics (big-step or small-step), studying in detail the most cited projects and presenting some derivative works that extend the originals aggregating useful features. Also, we filter our research for those that provide some insights in type-safety proofs. Furthermore, we provide a comparison between the most used projects in order to show which functionalities are covered in such projects. Second, our effort is focused towards the research opportunities in this area, showing some important works that can be applied to the previously presented projects to study features of object-oriented languages, and pointing for some possibilities to explore in future researches.

Keywords


Java Semantics; Operational Semantics; Type Systems; Type Safety

Full Text:

PDF

References


TIOBE.COM. TIOBE Index. 2017. Disponivel em: https://www.tiobe.com/tiobe-index/.

LANGPOP.COM. Programming Language Popularity Index. 2013. Disponıvel em: http://langpop.corger.nl/.

ORACLE.COM. The Java Language Specification. 2015. Disponıvel em: ⟨http://docs.oracle.com/javase/specs/ jls/se8/html/.

DEBBABI, M.; FOURATI, M. A formal type system for Java. J. Object Technol., v. 6, n. 8, p. 117–184, 2007.

FILARETTI, D.; MAFFEIS, S. An executable formal semantics of PHP. In: Proceedings of the 28th European Conference on ECOOP 2014 — Object-Oriented Programming. New York, NY, USA: Springer-Verlag New York, Inc., 2014. v. 8586.

BOGDANAS, D.; ROSU, G. K-Java: A complete semantics of Java. SIGPLAN Not., v. 50, n. 1, p. 445–456, 2015.

MILNER, R. The definition of standard ML: revised. 1. ed. Cambridge, USA: MIT press, 1997.

FLATT, M.; KRISHNAMURTHI, S.; FELLEISEN, M. Classes and mixins. In: Proceedings of the 25th

ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages. New York, NY, USA: ACM, 1998. (POPL, ’98).

DROSSOPOULOU, S.; EISENBACH, S. Describing the semantics of java and proving type soundness. In: Formal Syntax and Semantics of Java. London, UK: Springer-Verlag, 1999. v. 1.

IGARASHI, A.; PIERCE, B. C.; WADLER, P. Featherweight java: A minimal core calculus for java and gj. ACM Trans. Program. Lang. Syst., v. 23, n. 3, p. 396–450, 2001.

KLEIN, G.; NIPKOW, T. A machine-checked model for a java-like language, virtual machine, and compiler. ACM Trans. Program. Lang. Syst., v. 28, n. 4, p. 619–695, 2006.

GOOGLE. Google Scholar. 2018. Disponıvel em: https://scholar.google.com.br/.

ORACLE.COM. The Java Language Specification. 2018. Disponıvel em: https://docs.oracle.com/javase/specs/ jls/se10/html.

CIANCARINI, S. C. C. L. P. A reduction semantics for java. Citeseerx, v. 1, n. 1, p. 1–17, 1998.

FARZAN, A.; CHEN, F.; MESEGUER, J. Formal analysis of java programs in javafan. In: ALUR, R.; PELED, D. A. (Ed.). In Proceedings of CAV. Berlin, Germany: Springer, 2004. (LNCS, v. 3314).

STARK, R. F.; BORGER, E.; SCHMID, J. Java and the Java Virtual Machine: Definition, Verification, Validation with Cdrom. 2001. ed. Secaucus, NJ, USA: Springer-Verlag New York, Inc., 2001. v. 1.

PIERCE, B. C. Types and Programming Languages. 1st. ed. Cambridge, Usa: The MIT Press, 2002. v. 1.

BIERMAN, G. M.; PARKINSON, M.; PITTS, A. MJ: An imperative core calculus for Java and Java with effects. Cambridge, UK, 2003.

O STLUND,J.; WRIGSTAD,T. Welterweightjava. In: VITEK, J. (Ed.). Proceedings of the 48th International Conference on Objects, Models, Components, Patterns. Berlin, Heidelberg: Springer-Verlag, 2010. (TOOLS, ’10).

BELLIA, M.; OCCHIUTO, M. E. Properties of java simple closures. Fundam. Inf., v. 109, n. 3, p. 237–253, 2011.

FEITOSA SAMUEL DA SILVAAND VIZZOTTO, J. K. P. E. K. D. B. A. R. A monadic semantics for quantum computing in featherweight java. In: . Proceedings of the 20th Brazilian Symposium on Progamming Languages, SBLP 2016. 1. ed. Maringa, Brazil: Springer International Publishing, 2016. v. 1, p. 31–45.

DELAWARE, B.; COOK, W.; BATORY, D. Product lines of theorems. In: ACM SIGPLAN Notices. New York, USA: ACM, 2011. v. 46.

KUCI, E. et al. A co-contextual type checker for featherweight java (incl. proofs). arXiv preprint arXiv:1705.05828, v. 1, n. 1, p. 1–54, 2017.

FLATT, M.; KRISHNAMURTHI, S.; FELLEISEN, M. A programmer’s reduction semantics for classes and mixins.

In: ALVES-FOSS, J. (Ed.). Formal Syntax and Semantics of Java. London, UK: Springer-Verlag, 1999. v. 1.

POTTIER, F. Hindley-milner elaboration in applicative style: Functional pearl. In: JEURING, J.; CHAKRAVARTY, M. M. (Ed.). Proceedings of the 19th ACM SIGPLAN International Conference on Functional Programming. New York, USA: ACM, 2014. (ICFP, ’14).

FLANAGAN, C.; FREUND, S. N. Type-based race detection for java. SIGPLAN Not., v. 35, n. 5, p. 219–232, 2000.

BOYAPATI, C.; LEE, R.; RINARD, M. A type system for preventing data races and deadlocks in java programs. In: Proceedings of the ACM Conference on Object-Oriented Programming, Systems, Languages and Applications. Cambridge, USA: MIT Press, 2002. v. 1.

WELC, A.; HOSKING, A. L.; JAGANNATHAN, S. Transparently reconciling transactions with locking for java synchronization. In: THOMAS, D. (Ed.). Proceedings of the 20th European Conference on Object-Oriented Programming. Berlin, Heidelberg: Springer-Verlag, 2006.

FINDLER, R. B.; FELLEISEN, M. Contract soundness for object-oriented languages. SIGPLAN Not., v. 36, n. 11, p. 1–15, 2001.

BOYAPATI, C.; LISKOV, B.; SHRIRA, L. Ownership types for object encapsulation. In: AIKEN, A.; MORRISETT, G. (Ed.). ACM SIGPLAN Notices. New York, USA: ACM press, 2003. v. 38.

HAMLEN, K. W.; JONES, M. M.; SRIDHAR,

M. Aspect-oriented runtime monitor certification. In: FLANAGAN, C.; Ko ̈NIG, B. (Ed.). Proceedings of the 18th International Conference on Tools and Algorithms for the Construction and Analysis of Systems. Berlin, Heidelberg: Springer-Verlag, 2012. v. 1.

MOLDEREZ, T.; JANSSENS, D. Modular reasoning in aspect-oriented languages from a substitution perspective. In:CHIBA,S.;TANTERE ́ric;HIRSCHFELD,E.E. andRobert (Ed.). Transactions on Aspect-Oriented Software Development XII. Berlin, Germany: Springer, 2015. v. 8989, p. 3–59.

SYME, D. Proving java type soundness. In: ALVES-FOSS, J. (Ed.). Formal Syntax and Semantics of Java. London, UK: Springer-Verlag, 1999. v. 1.

DROSSOPOULOU, S.; EISENBACH, S. Java is type safe - probably. In: AKS ̧ IT, M.; MATSUOKA, S. (Ed.). In European Conference On Object Oriented Programming. Berlin, Germany: Springer-Verlag, 1997. (LNCS, v. 1241), p. 389–418.

DROSSOPOULOU, S.; EISENBACH, S.; KHURSHID, S. Is the java type system sound? Theor. Pract. Object Syst., John Wiley & Sons, Inc., New York, NY, USA, v. 5, n. 1, p. 3–24, 1999.

NIPKOW, T.; OHEIMB, D. von. Javalight is type-safe—definitely. In: Proceedings of the 25th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages. New York, USA: ACM, 1998. (POPL, ’98).

MYERS, A. C. Mostly-static decentralized information flow control. Tese (Doutorado) — Massachusetts Institute of Technology, Cambridge, USA, 1999.

BODIN, M. a. A trusted mechanised javascript specification. In: JAGANNATHAN, S.; SEWELL, P. (Ed.). ACM SIGPLAN Notices. New York, USA: ACM, 2014. v. 49.

BODIN, M. Certified semantics and analysis of JavaScript. Tese (Doutorado) — Universite ́ Rennes 1, 2016.

FILARETTI, D. An executable formal semantics of PHP with applications to program analysis. Tese (Doutorado) — Imperial College London, London, UK, 2015.

NIPKOW, T. Jinja: Towards a comprehensive formal semantics for a java-like language. In: NIPKOW, T. et al. (Ed.). IN PROCEEDINGS OF THE MARKTOBERDORF SUMMER SCHOOL. NATO SCIENCE SERIES. Munich, Germany: Press, 2003. v. 1.

KLEIN, G.; NIPKOW, T. Jinja is not Java - Archive of Formal Proofs. 2017. Disponıvel em:

https://www.isa-afp.org/entries/Jinja.html.

LOCHBIHLER, A. Type safe nondeterminism - a formal semantics of java threads. In: International Workshop on Foundations of Object-Oriented Languages (FOOL 2008). San Francisco, USA: Karlsruhe Institute of Technology, 2008. v. 1.

WASSERRAB, D. et al. An operational semantics and type safety proof for multiple inheritance in. In: TARR, P. et al. (Ed.). ACM SIGPLAN Notices. New York, USA: ACM, 2006. v. 41.

CHAIEB, A. Proof-producing program analysis.

In: BARKAOUI, K.; CAVALCANTI, A.; CERONE, A. (Ed.). Proceedings of the Third International Conference on Theoretical Aspects of Computing. Berlin, Heidelberg: Springer-Verlag, 2006. (ICTAC, ’06).

PIRKER, M.; SCHAPER, B. M. From Jinja Bytecode to Computation Graphs. Bachelor’s Thesis — University of Innsbruck, 2012.

MOSER, G.; SCHAPER, M. A complexity preserving transformation from jinja bytecode to rewrite systems. arXiv preprint arXiv:1204.1568, v. 1, n. 1, p. 1–36, 2012.

KUSTERS,R.etal.Ahybridapproachforproving noninterference of java programs. In: FOURNET, C.; HICKS, M. (Ed.). Computer Security Foundations Symposium (CSF), 2015 IEEE 28th. Verona, Italy: IEEE, 2015. v. 1.

CLAUDEL, B.; SABAH, Q.; STEFANI, J.-B. Simple isolation for an actor abstract machine. In: International

Conference on Formal Techniques for Distributed Objects, Components, and Systems. Cham, Switzerland: Springer,

Cham, 2015. (LNCS, v. 9039).

MOGGI, E. Computational lambda-calculus and monads. In: Proceedings of the Fourth Annual Symposium on Logic in computer science. Hoboken, New Jersey: IEEE Press, 1989. (LNCS, v. 9039).

CLAESSEN, K.; HUGHES, J. QuickCheck: A lightweight tool for random testing of Haskell programs. In: ODERSKY, M.; WADLER, P. (Ed.). Proceedings of the Fifth ACM SIGPLAN International Conference on Functional Programming. New York, NY, USA: ACM, 2000. (ICFP, ’00).

BLELLOCH, G. E.; HARPER, R. Cache and i/o efficent functional algorithms. In: Proceedings of the 40th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages. New York, USA: ACM, 2013. (POPL, v. 1).

HARPER, R. Yet Another Reason Not To

Be Lazy Or Imperative. 2012. Disponıvel em: https://existentialtype.wordpress.com/2012/08/26/ yet-another-reason-not-to-be-lazy-or-imperative/⟩.

CAMPOS, J.; VASCONCELOS, V. T. Imperative objects with dependent types. In: MONAHAN, R. (Ed.). Proceedings of the 17th Workshop on Formal Techniques for Java-like Programs. New York, NY, USA: ACM, 2015. (FTfJP, ’15).

RONDON, P. M.; KAWAGUCI, M.; JHALA, R. Liquid types. In: Proceedings of the 29th ACM SIGPLAN Conference on Programming Language Design and Implementation. New York, USA: ACM, 2008. (PLDI, ’08).




DOI: https://doi.org/10.22456/2175-2745.80912

Copyright (c) 2018 Samuel da Silva Feitosa, Rodrigo Geraldo Ribeiro, Andre Rauber Du Bois

Creative Commons License
This work is licensed under a Creative Commons Attribution-NonCommercial-NoDerivatives 4.0 International License.