Abstract
We introduce an expressive yet semantically clean core Java-like language, Java JR, and provide it with a formal operational semantics based on traces of observable actions which represent interaction across package boundaries. A detailed example based on the Observer Pattern is used to demonstrate the intuitive character of the semantic model. We also show that our semantic trace equivalence is fully-abstract with respect to a natural notion of testing equivalence for object systems. This is the first such result for a full class-based OO-language with inheritance.
Chapter PDF
Similar content being viewed by others
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
Abadi, M., Cardelli, L.: A Theory of Objects. Springer, Heidelberg (1996)
Abramsky, S., Ong, L.: Full abstraction in the lazy lambda calculus. Information and Computation 105, 159–267 (1993)
Alves-Foss, J. (ed.): Formal Syntax and Semantics of Java. LNCS, vol. 1523. Springer, Heidelberg (1999)
Attali, I., Caromel, D., Russo, M.: A formal executable semantics for Java. In: Proc. Formal Underpinnings of Java (1998)
Banerjee, A., Naumann, D.A.: Stack-based access control and secure information flow. J. Functional Programming (2005) (to appear)
Bierman, G.M., Parkinson, M.J., Pitts, A.M.: An imperative core calculus for Java and Java with effects. Technical Report 563, University of Cambridge Computer Laboratory (2003)
Brookes, S.D., Hoare, C.A.R., Roscoe, A.W.: A theory of communicating sequential processes. Journal of the ACM 31(3), 560–599 (1984)
Cardelli, L., Gordon, A.: Mobile ambients. In: Proc. Foundations of Software Science and Computation Structures. LNCS. Springer, Heidelberg (1998)
Drossopoulou, S., Eisenbach, S.: Towards an operational semantics and proof of type soundness for Java. In: Alves-Foss, J. (ed.) Formal Syntax and Semantics of Java. LNCS, vol. 1523. Springer, Heidelberg (1999)
Fiore, M.P., Moggi, E., Sangiorgi, D.: A fully-abstract model for the pi-calculus. In: Proc. IEEE Logic in Computer Science, p. 43. IEEE Computer Society, Los Alamitos (1996)
Flatt, M., Krishnamurthi, S., Felleisen, M.: Classes and mixins. In: Proc. ACM Principles of Programming Languages, pp. 171–183 (1998)
Gamma, E., Helm, R., Johnson, R., Vlissides, J.: Design Patterns: Elements of Reusable Object-Oriented Software. Addison-Wesley, Reading (1995)
Gordon, M.J.C.: Experimental Programming Reports. PhD thesis, School of AI, University of Edinburgh (1973)
Gosling, J., Joy, B., Steele, G., Bracha, G.: Java Language Specification, 2nd edn. The Java Series. Addison-Wesley, Reading (2000)
Hennessy, M.: Algebraic Theory of Processes. MIT Press, Cambridge (1988)
Igarashi, A., Pierce, B.C., Wadler, P.: Featherweight Java: a minimal core calculus for Java and GJ. ACM Trans. Program. Lang. Syst. 23(3), 396–450 (2001)
Jeffrey, A.S.A., Rathke, J.: A fully abstract testing semantics for concurrent objects. In: Proc. IEEE Logic in Computer Science, pp. 101–112. IEEE Computer Society Press, Los Alamitos (2002)
Landin, P.J.: A correspondence between ALGOL 60 and Church’s lambda-notation: Part I. Communications of the ACM 8(2), 89–101 (1965)
McCarthey, J.: Towards a mathematical science of computation. In: Popplewell, C.M. (ed.) Information Processing 1962, pp. 21–28 (1963)
McCarthy, J.: A formal description of a subset of algol. In: Proc. IFIP WG Formal Language Description Languages for Computer Programming, pp. 1–12. North-Holland, Amsterdam (1966)
Milner, R.: A Calculus of Communication Systems. LNCS, vol. 92. Springer, Heidelberg (1980)
Milner, R.: Communication and mobile systems: the π-calculus. Cambridge University Press, Cambridge (1999)
Morris, J.H.: Lambda-calculus models of programming languages. PhD thesis, MIT (1968)
Nipkow, T.: Jinja: Towards a comprehensive formal semantics for a Java-like language. In: Proc. Marktobderdorf Summer School. IOS Press, Amsterdam (2003) (to appear)
Plotkin, G.D.: LCF considered as a programming language. Theoretical Computer Science 5, 223–255 (1977)
Plotkin, G.D.: A structural approach to operational semantics. Report DAIMI FN-19, Computer Science Department, Aarhus University (1981)
Tofte, M., Milner, R., Harper, R.: The Definition of Standard ML. MIT Press, Cambridge (1990)
Reppy, J.: Higher-Order Concurrency. PhD thesis, Cornell University, Technical Report TR 92-1285 (1992)
Sangiorgi, D., Walker, D.: The pi-calculus: A Theory of mobile processes. Cambridge University Press, Cambridge (2001)
Steel, T.B.: A formalization of semantics for programming language description. In: Proc. IFIP WG Formal Language Description Languages for Computer Programming, pp. 25–36 (1969)
Sussman, G.J., Steele Jr., G.L.: Scheme:an interpreter for extended lambda-calculus. Technical Report Memo 349, MIT AI Lab (1975)
Wright, A.K., Felleisen, M.: A syntactic approach to type soundness. Information and Computation 115(1), 38–94 (1994)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2005 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Jeffrey, A., Rathke, J. (2005). Java JR: Fully Abstract Trace Semantics for a Core Java Language. In: Sagiv, M. (eds) Programming Languages and Systems. ESOP 2005. Lecture Notes in Computer Science, vol 3444. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-31987-0_29
Download citation
DOI: https://doi.org/10.1007/978-3-540-31987-0_29
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-25435-5
Online ISBN: 978-3-540-31987-0
eBook Packages: Computer ScienceComputer Science (R0)