A fragment calculus-towards a model of separate compilation, linking and binary compatibility
- 20 January 2003
- conference paper
- Published by Institute of Electrical and Electronics Engineers (IEEE)
- p. 147-156
- https://doi.org/10.1109/lics.1999.782606
Abstract
We propose a calculus describing compilation and linking in terms of operations on fragments, i.e. compilation units, without reference to their specific contents. We believe this calculus faithfully reflects the situation within modern programming systems. Binary compatibility in Java prescribes conditions under which modification of fragments does not necessitate recompilation of importing fragments. We apply our calculus to formalize binary compatibility, and demonstrate that several interpretations of the language specification are possible, each with different ramifications. We choose a particular interpretation, justify our choice, formulate and prove properties important for language designers and code library developers.Keywords
This publication has 12 references indexed in Scilit:
- Is the Java type system sound?Theory and Practice of Object Systems, 1999
- Proving Java Type SoundnessPublished by Springer Nature ,1999
- Dynamic class loading in the Java virtual machinePublished by Association for Computing Machinery (ACM) ,1998
- What is Java binary compatibility?Published by Association for Computing Machinery (ACM) ,1998
- A type system for Java bytecode subroutinesPublished by Association for Computing Machinery (ACM) ,1998
- The security of static typing with dynamic linkingPublished by Association for Computing Machinery (ACM) ,1997
- Program fragments, linking, and modularizationPublished by Association for Computing Machinery (ACM) ,1997
- Release-to-release binary compatibility in SOMPublished by Association for Computing Machinery (ACM) ,1995
- Programming in Modula-2Published by Springer Nature ,1982
- A Separate Compilation System for AdaPublished by Springer Nature ,1981