Logic in Computer Science (LICS 1999)

Paper: A Fragment Calculus — Towards a Model of Separate Compilation, Linking and Binary Compatibility (at LICS 1999)

Authors: Sophia Drossopoulou Susan Eisenbach David Wragg

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.

BibTeX

  @InProceedings{DrossopoulouEisenba-AFragmentCalculusTo,
    author = 	 {Sophia Drossopoulou and Susan Eisenbach and David Wragg},
    title = 	 {A Fragment Calculus — Towards a Model of Separate Compilation, Linking and Binary Compatibility},
    booktitle =  {Proceedings of the Fourteenth Annual IEEE Symp. on Logic in Computer Science, {LICS} 1999},
    year =	 1999,
    editor =	 {Giuseppe Longo},
    month =	 {July}, 
    pages =      {147--156},
    location =   {Trento, Italy}, 
    publisher =	 {IEEE Computer Society Press}
  }