Publications
147 results found
Ancona D, Zucca E, Drossopoulou S, 2000, Overloading and Inheritance in Java, 2nd ECOOP Workshop on Formal techniques for Java Programs, ECOOP2000, Cannes
Drossopoulou S, 2000, Towards an abstract model of Java dynamic linking and verification, ACM Sigplan Workshop, Montreal
Drossopoulou S, Eisenbach S, Khurshid S, 1999, Is the Java Type System is Sound, Theory and Practice of Object Systems, Vol: 5, Pages: 3-24
A proof of the soundness of the Java type system is a first, necessary step towards demonstrating which Java programs won't compromise computer security. We consider a subset of Java describing primitive types, classes, inheritance, instance variables and methods, interfaces, shadowing, dynamic method binding, object creation, null, arrays and exception throwing and handling. We argue that for this subset the type system is sound, by proving that program execution preserves the types, up to subclasses/subinterfaces.
Drossopoulou S, Eisenbach S, Wragg D, 1999, A Fragment Calculus towards a model of Separate Compilation, Linking and Binary Compatibility, LICS'99 Fourteenth Annual IEEE Symposium on Logic in Computer Science, Trento
Drossopoulou S, Eisenbach S, Khurshid S, 1999, Is the Java type system sound?, THEORY AND PRACTICE OF OBJECT SYSTEMS, Vol: 5, Pages: 3-24, ISSN: 1074-3227
- Author Web Link
- Cite
- Citations: 27
Drossopoulou S, Eisenbach S, 1999, Describing the Semantics of Java and Proving Type Soundness, Publisher: Springer Berlin Heidelberg, Pages: 41-80, ISSN: 0302-9743
Drossopoulou S, Eisenbach S, 1999, Towards an Operational Semantics and Proof of Type Soundness for Java, Formal Syntax and Semantics of Java, Publisher: Springer-Verlag
We give an operational semantics for a large subset of Java describing primitive types, classes, inheritance, instance variables and methods, interfaces, shadowing, dynamic method binding, object creation, null, arrays and exception throwing and handling. We build a model that is simple and near the programmer's intuition. We distinguish between three languages: Javas is the original language. Javase is an enriched version of Javas containing compile time information necessary for execution. Javar is an extended version of Javase allowing for runtime constructs such as addresses.\r\n\r\nWe give a type system for Javas, Javase and Javar. The two latter are slight modifications of the former. We prove that well-typed Javas terms retain their type when the corresponding Javase or Javar term is considered. The operational semantics describes the execution of Javar terms for given Javase programs. We prove a subject reduction theorem, which states that execution of Javar preserves types, up to subclasses/subinterfaces\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, Yang D, 1998, Permco – a permissive approach to covariant overriding of subclass members, Departmental Technical Report: 98/4, Publisher: Department of Computing, Imperial College London
We describe Permco, a permissive approach which allows covariant overriding of instance variables and any overriding of instance methods.Subclasses are considered subtypes. Instance method access is treated by considering the types of all methods defined for the class of the receiver and all its possible subclasses. Instance variable access is treated by considering the types of the instance variable in all possible subclasses. Thus, Permco is permissive at the point of redefinition and restrictive at the point of call or access. Closed types describe values which may belong to a class but not to its subclasses, and allow a more precise description of types. Result types may depend on receiver or argument types.This paper introduces Permco in terms of an example and compares with related approaches. It then demonstrates its soundness through a subject reduction theorem.
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, 1996, The knife change minimization problem. definition, properties, heuristics, Departmental Technical Report: 96/7, Publisher: Department of Computing, Imperial College London
We define formally the Knife Change Minimization Problem, we prove some properties which reduce the search space, and then describe some heuristsics.At one of the last stages of the paper construction process customer widths have to be cut out of jumbo reels. For example, the widths 50,40,60,40, 30,50,50,50 and 60,40,40,40 may have to be cut out of three jumbo reels of width 200. The collections of indivdidual widths (e.g. 50-40-60-40) are called patterns.The order in which to consider the patterns (i.e. the route) can be arbitrary, and the order in which to cut each pattern is arbitrary as well. Each different solution involves a different number of knife changes, e.g. the solution from above involves 12 knife changes, whereas the solution 50-40-40-60, 5-4-4-4 and 50-50-50-30 involves only 7 knife changes. The objective is to find the solution with the minimal number of knife changes, or, because the search space is immense, to approximate such a solution.We first give some auxiliary definitions describing operations on sequences, bags and sets. We then define formally the problem, the solution space and the cost function in terms of the above. We prove some properties which reduce the search space, and then we describe heuristics.
Drossopoulou S, Karathanos S, Yang D, 1996, Type Checking Smalltalk, Journal of Object Oriented Programming, Vol: 8
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
Spinellis D, Eisenbach S, Drossopoulou S, 1994, Language and Architecture Paradigms as Object Classes: A Unified Approach Towards Multiparadigm Programming, \tProgramming Languages and System Architectures, Publisher: Springer-Verlag, Pages: 191-207
Computer language paradigms offer linguistic abstractions and proof theories for expressing program implementations. Similarly, system architectures offer the hardware abstractions and quantitative theories applicable to the execution of compiled programs. Although the two entities are usually treated independently, object-oriented technology can be used to obtain a unifying framework. Specifically, inheritance can be used to model both programming languages as extensions to the assembly language executed by the target architecture, and system architectures as the root class of those paradigms. We describe how these principles can be used to model, structure and implement real multiparadigm systems in a portable and extendable way.
Spinellis D, Drossopoulou S, Eisenbach S, 1994, An Object Model for Multiparadigm Programming, OOPSLA Workshop on Multi-Language Object Models
Spinellis D, Drossopoulou S, Eisenbach S, 1994, Multiparadigm Programming through Paradigm Classes, International Conference on Programming Languages and System Architectures Zurich, Publisher: Springer Verlag
FINKELSTEIN A, KRAMER J, ABRAMSKY S, et al., 1993, AN INTEGRATED ENGINEERING STUDY SCHEME IN COMPUTING, COMPUTER JOURNAL, Vol: 36, Pages: 320-334, ISSN: 0010-4620
- Author Web Link
- Cite
- Citations: 2
Drossopoulou S, Paterson R, Eisenbach S, 1991, Parameterized Interfaces are Interfaces - AIAS., Publisher: Springer, Pages: 133-147
Drossopoulou S, Uhl J, Persch G, et al., 1982, An attribute grammar for Ada, Symposium on Compiler Construction, Publisher: ACM
We describe the development of a formal specification of the static semantics of Ada in form of an attribute grammar. This specification is complete, and was tested extensively with automatically generated equivalent Pascal programs. From this specification we systematically developed the semantic analysis part of our Ada Compiler Front End. We outline the general proceeding when specifying semantic analysis with attribute grammars and then discuss to some extent examples about declaration elaboration and overloading resolution.
Uhl J, Persch G, Drossopoulou S, et al., 1982, An Attribute Grammar for the Semantic Analysis of Ada, ISBN: 0387115714
Persch G, Dausmann M, Winterstein G, et al., 1981, A Separate Compilation System for Ada, Werkzeuge der Programmiertechnik, GI-Arbeitstagung, Karlsruhe, 16.-17. Mõrz 1981, Pages: 197-213
Drossopoulou S, Winterstein G, Dausmann M, et al., 1981, The Tasking Facility of Ada, Implementierungssprachen fuer nichtsequentielle Programmsysteme,\r\n-- Tagung I/1981 des German Chapter of the ACM, Kaiserslautern, Publisher: Teubner, Pages: 95-118
Cameron N, Ernst E, Drossopoulou S, Towards an Existential Types Model for Java Wildcards, Formal techniques for Java-like languages
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.