True separate compilation of Java classes

ABSTRACT

We define a type system modeling true separate compilation for a small but significant Java subset, in the sense that a single class declaration can be intra-checked (following the Cardelli's terminology) and compiled providing a minimal set of type requirements on missing classes. These requirements are specified by a local type environment associated with each single class, while in the existing formal definitions of the Java type system classes are typed in a global type environment containing all the type information on a closed program. We also provide formal rules for static inter-checking and relate our approach with compilation of closed programs, by proving that we get the same results.

REFERENCES

• 1: D. Ancona and G. Lagorio. Supporting true separate compilation in Java: A modular approach. Technical report, Dipartimento di Informatica e Scienze dell'Informazione, Università di Genova, 2002. Submitted for publication.
• 2: Davide Ancona , Giovanni Lagorio , Elena Zucca, A Formal Framework for Java Separate Compilation, Proceedings of the 16th European Conference on Object-Oriented Programming, p.609-636, June 10-14, 2002
• 3: Luca Cardelli, Program fragments, linking, and modularization, Proceedings of the 24th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.266-277, January 15-17, 1997, Paris, France [doi>10.1145/263699.263735]
• 4: Sophia Drossopoulou , Susan Eisenbach, Describing the Semantics of Java and Proving Type Soundness, Formal Syntax and Semantics of Java, p.41-82, January 1999
• 5: S. Drossopoulou, T. Valkevych, and S. Eisenbach. Java type soundness revisited. Technical report, Dept. of Computing - Imperial College of Science, Technology and Medicine, September 2000.
• 6: James Gosling , Bill Joy , Guy Steele , Gilad Bracha, Java Language Specification, Second Edition: The Java Series, Addison-Wesley Longman Publishing Co., Inc., Boston, MA, 2000
• 7: Pieter H. Hartel , Luc Moreau, Formalizing the safety of Java, the Java virtual machine, and Java card, ACM Computing Surveys (CSUR), v.33 n.4, p.517-558, December 2001 [doi>10.1145/503112.503115]
• 8: Tim Lindholm , Frank Yellin, Java Virtual Machine Specification, Addison-Wesley Longman Publishing Co., Inc., Boston, MA, 1999
• 9: Sean McDirmid , Matthew Flatt , Wilson C. Hsieh, Jiazzi: new-age components for old-fasioned Java, Proceedings of the 16th ACM SIGPLAN conference on Object oriented programming, systems, languages, and applications, p.211-222, October 14-18, 2001, Tampa Bay, FL, USA
• 10: Zhong Shao , Andrew W. Appel, Smartest recompilation, Proceedings of the 20th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.439-450, March 1993, Charleston, South Carolina, United States [doi>10.1145/158511.158702]

INDEX TERMS

Primary Classification:
  F. Theory of Computation
  F.3 LOGICS AND MEANINGS OF PROGRAMS
      F.3.3 Studies of Program Constructs

General Terms:
Languages, Theory

Keywords:
object-oriented programming, separate compilation, types