zbMATH — the first resource for mathematics

A formal framework for Java separate compilation. (English) Zbl 1049.68746
Magnusson, Boris (ed.), ECOOP 2002 - object-oriented programming. 16th European conference, Málaga, Spain, June 10–14, 2002. Proceedings. Berlin: Springer (ISBN 3-540-43759-2). Lect. Notes Comput. Sci. 2374, 609-635 (2002).
Summary: We define a formal notion, called compilation schema, suitable for specifying different possibilities for performing the overall process of Java compilation, which includes typechecking of source fragments with generation of corresponding binary code, typechecking of binary fragments, extraction of type information from fragments and definition of dependencies among them. We consider three compilation schemata of interest for Java, that is, minimal, SDK and safe, which correspond to a minimal set of checks, the checks performed by the SDK implementation, and all the checks needed to prevent run-time linkage errors, respectively. In order to demonstrate our approach, we define a kernel model for Java separate compilation and execution, consisting in a small Java subset, and a simple corresponding binary language for which we provide an operational semantics including run-time verification. We define a safe compilation schema for this language and formally prove type safety.
For the entire collection see [Zbl 0997.68676].

68U99 Computing methodologies and applications
68N19 Other programming paradigms (object-oriented, sequential, concurrent, automatic, etc.)
68N15 Theory of programming languages
68N30 Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.)
Full Text: Link