Publications
134 results found
Drossopoulou S, Eisenbach S, 1999, Towards an Operational Semantics of Java and Proof of Soundness of its Type System, Formal Syntax and Semantics of Java, Editors: Foss, Publisher: Springer Verlag
Eisenbach S, Sadler C, 1999, Ephemeral Java Source Code, IEEE Workshop on Future Trends in Distributed Computing Systems, Cape Town
Drossopoulou S, Wragg D, Eisenbach S, 1998, What is Java Binary Compatibility?, OOPSLA 1998, Pages: 341-361
Separate compilation enables decomposition of programs into units that may be compiled separately, and linked into an executable. Traditionally, separate compilation was equivalent to the compilation of all units together, and modification and re-compilation of one unit required re-compilation of all importing units.\r\n\r\nJava suggests a more flexible framework, in which the linker checks the integrity of the binaries to be combined. Certain source code modifications, such as addition of methods to classes, are defined as binary compatible. The language description guarantees that binaries of types (i.e. classes or interfaces) which were modified in binary compatible ways may be re-compiled and linked with the binaries of types that imported and were compiled using the earlier versions of the modified types.\r\n\r\nHowever, this is not always the case: some of the changes considered by Java as binary compatible do not guarantee successful linking and execution. In this paper we study the concepts around binary compatibility. We suggest a formalization of the requirement of safe linking and execution without re-compilation, we investigate alternatives, we demonstrate several of its properties, and we propose a more restricted definition of binary compatible changes. Finally, we prove for a substantial subset of Java, that this restricted definition guarantees safe linking and execution.\r\n
Drossopoulou S, Wragg D, Eisenbach S, 1998, What is Java binary compatibility?, ACM SIGPLAN NOTICES, Vol: 33, Pages: 341-361, ISSN: 0362-1340
Separate compilation allows the decomposition of programs into units that may be compiled separately, and linked into an executable. Traditionally, separate compilation was equivalent to the compilation of all units together, and modification and re-compilation of one unit required re-compilation of all importing units.Java suggests a more flexible framework, in which the linker checks the integrity of the binaries to be combined. Certain source code modifications, such as addition of methods to classes, are defined as binary compatible. The language description guarantees that binaries of types (i.e. classes or interfaces) modified in binary compatible ways may be re-compiled and linked with the binaries of types that imported and were compiled using the earlier versions of the modified types.However, this is not always the case: some of the changes considered by Java as binary compatible do not guarantee successful linking and execution. In this paper we study the concepts around binary compatibility. We suggest a formalization of the requirement of safe linking and execution without re-compilation, investigate alternatives, demonstrate several of its properties, and propose a more restricted definition of binary compatible changes. Finally, we prove for a substantial subset of Java, that this restricted definition guarantees error-free linking and execution.
Wragg D, Drossopoulou S, Eisenbach S, 1998, Java binary computability is almost correct version 2∝, Departmental Technical Report: 98/3, Publisher: Department of Computing, Imperial College London
The Java language description is unusual in that it defines the effect of interleaving separate compilation and source code modifications. In Java, certain source code modifications, such as adding a method to a class, are defined as binary compatible. The Java language description does not require the re-compilation of programs importing classes or interfaces which were modified in binary compatible ways, and it claims that successful linking and execution of the altered program is guaranteed. In this paper we show that Java binary compatibility does not actually guarantee successful linking and execution. We then suggest a framework in which we formalize the requirement of safe linking and execution without re-compilation and we propose a more modest definition of binary compatibility. We prove for a substantial subset of Java, that our definition guarantees safe linking and execution.
Drossopoulou S, Eisenbach S, 1998, What is java binary compatibility?, Departmental Technical Report: 98/5, Publisher: Department of Computing, Imperial College London
Separate compilation allows the decomposition of programs into units that may be compiled separately, and linked into an executable. Traditionally, separate compilation was equivalent to the compilation of all units together, and modification and re-compilation of one unit required re-compilation of all importing units.Java suggests a more flexible framework, in which the linker checks the integrity of the binaries to be combined. Certain source code modifications, such as addition of methods to classes, are defined as binary compatible. The language description guarantees that binaries of types (i.e. classes or interfaces) modified in binary compatible ways may be re-compiled and linked with the binaries of types that imported and were compiled using the earlier versions of the modified types.However, this is not always the case: some of the changes considered by Java as binary compatible do not guarantee successful linking and execution. In this paper we study the concepts around binary compatibility. We suggest a formalization of the requirement of safe linking and execution without re-compilation, investigate alternatives, demonstrate several of its properties, and propose a more restricted definition of binary compatible changes. Finally, we prove for a substantial subset of Java, that this restricted definition guarantees error-free linking and execution.
Drossopoulou S, Eisenbach S, Wragg D, 1998, What can java binary compatibility mean?, Departmental Technical Report: 98/13, Publisher: Department of Computing, Imperial College London
Java binary compatibility prescribes conditions under which modification and re-compilation of classes does not necessitate re-compilation of further classes importing the modified classes. Binary compatibility is a novel concept for language design.We argue that the description of the term binary compatibility in the Java language specification allows for many possible interpretations. We discuss the various interpretations and their ramifications, and suggest one interpretation, which is best in our view.
Drossopoulou S, Eisenbach S, 1998, Towards an Operational Semantics and Proof of Type Soundness in Java, Formal Syntax and Semantics of Java, Editors: ves-Foss, Publisher: Springer
Radestock M, Eisenbach S, 1998, Component coordination in middleware systems, IFIP International Conference on Distributed Systems Platforms and Open Distributed Processing (Middleware 98), Publisher: SPRINGER-VERLAG LONDON LTD, Pages: 225-240
- Author Web Link
- Cite
- Citations: 12
Drossopoulou S, Eisenbach S, 1997, Java is type safe - Probably, 11th European Conference on Object-Oriented Programming (ECOOP 97), Publisher: SPRINGER-VERLAG BERLIN, Pages: 389-418, ISSN: 0302-9743
- Author Web Link
- Cite
- Citations: 26
Drossopoulou S, Eisenbach S, 1997, Is the Java Type System Sound?, FOOL 4( Foundations of Object Oriented Languages), Paris
Drossopoulou S, Eisenbach S, 1997, The Java Type System is Sound - Probably, European Conference of Object Oriented programming, Jyvaskyla, Finland, Publisher: Springer
Radestock M, Eisenbach S, 1996, An Object Model for Distributed and Concurrent Programming Based on Decomposition, Object Orientation with Parallelism and Persistence, Publisher: Kluwer Academic Publishers
Broda KB, Eisenbach S, 1996, Tool Support for Informal Deduction, ACSE'96, Sydney, Australia
Broda KB, Eisenbach S, Kamara L, 1996, Tool Support for Natural Deduction, Proceedings of ACSE96, CACM
Radestock M, Eisenbach S, 1996, Coordination in Evolving Systems, International Workshop on Trends in Distributed Systems
Radestock M, Eisenbach S, 1996, Formalizing System Structure, IWSSD-8, Publisher: IEEE Computer Society Press, Paderborn Germany
Radestock M, Eisenbach S, 1996, Agent-based Configuration Management, 7th IFIP/IEEE International Workshop on Distributed Systems: Operation and Management
Radestock M, Eisenbach S, 1996, Semantics of a Higher-Order Coordination Language, COORDINATION'96 Cesena, Italy, Pages: 339-356
Kramer J, Magee J, Eisenbach S, 1995, Modelling Darwin in pi-Calculus, Theory and Practice in Distributed Systems, Publisher: Springer-Verlag, Pages: 133-152
SPINELLIS D, DROSSOPOULOU S, EISENBACH S, 1995, OBJECT-ORIENTED TECHNOLOGY IN MULTIPARADIGM LANGUAGE IMPLEMENTATION, JOURNAL OF OBJECT-ORIENTED PROGRAMMING, Vol: 8, Pages: 33-38, ISSN: 0896-8438
- Author Web Link
- Cite
- Citations: 1
Magee JN, Dulay N, Eisenbach S, et al., 1995, Specifying Distributed Software Architectures, Fifth European Software Engineering Conference, ESEC '95 , Barcelona
Magee JN, Dulay N, Eisenbach S, et al., 1995, Specifying Distributed Software Architectures, Fifth European Software Engineering Conference, ESEC '95 , Barcelona
Magee J, Kramer J, Eisenbach S, 1995, System Structuring: A Convergence of Theory and Practice?, Dagstuhl International Workshop on Theory and Practice in Distributed Systems
Darwin is a general purpose structuring tool of use in building complex distributed systems from diverse components and diverse component interaction mechanisms. It is in essence a declarative binding language which can be used to define hierarchic compositions of interconnected components. Distribution is dealt with orthogonally to system structuring. The language allows the specification of both static structures and dynamic structures which evolve during execution. The central abstractions managed by Darwin are components and services. Bindings are formed by manipulating references to services. \r\n\r\nThe paper describes the operational semantics of Darwin in terms of the pi-calculus, MilnerÆs calculus of mobile processes. The correspondence between the treatment of names in the pi-calculus and the management of service references in Darwin leads to an elegant and concise pi-calculus model of DarwinÆs operational semantics. The model has proved useful in arguing the correctness of Darwin implementations and in designing\r\nextensions to Darwin and reasoning about their behaviour. The paper discusses the reasons why other formalisms fail to capture elegantly the system structuring concepts on which Darwin is based.
Radestock M, Eisenbach S, 1994, What do you get from a p-calculus semantics?, PARLE, Athens
Magee JN, Eisenbach S, Kramer J, 1994, Modelling Darwin in the Pi-calculus, International Workshop on Theory and Practice in Distributed Systems, Publisher: Springer-Verlag
Radestock M, Eisenbach S, 1994, Towards a Minimal Object-Oriented Language for Distributed and Concurrent Programming, PODC, Los Angeles
Spinellis D, Drossopoulou S, Eisenbach S, 1994, An Object Model for Multiparadigm Programming, OOPSLA Workshop on Multi-Language Object Models
Eisenbach S, Kramer J, Magee J, 1994, Specifying the Concurrent Programming System\r\nRegis in the Pi-Calculus\r\n, Proceedings IEEE 2nd Int. Workshop on Configurable Distributed Systems (IWCDS-2), Pages: 1-4
This data is extracted from the Web of Science and reproduced under a licence from Thomson Reuters. You may not copy or re-distribute this data in whole or in part without the written consent of the Science business of Thomson Reuters.