Publications
147 results found
Drossopoulou S, Eisenbach S, 2004, Flexible, source level, dynamic linking and re-linking, Formal techniques for Java-like languages, 2003
Drossopoulou S, Damiani F, Giannini P, 2003, Refined Effects for Unanticipated Object Re-classification: Fickle3 (Extended Abstract), Theoretical Computer Science: 8th Italian Conference (ICTCS'03}, Publisher: Springer-Verlag, Pages: 97-110
In previous work with Dezani, on the language Fickle, and its extension, FickleII, we introduced language features for object re-classification for imperative, typed, class-based, object-oriented languages.\r\n\r\nIn this paper we present the language Fickle3, which on one side refines FickleII with more expressive effect annotations, and on the other eliminates the need to declare explicitly which are the classes of the objects that may be re-classified. Therefore, Fickle3 allows to correctly type meaningful programs which FickleII rejects. Moreover, re-classification may be decided by the client of a class, allowing "unanticipated object re-classification". As for FickleII, also the type and effect system for Fickle3 guarantees that, even though objects may be re-classified across classes with different members, they will never attempt to access non existing members.\r\n\r\nThe type and effect system of Fickle3 has some significant differences from the one of FickleII. In particular, besides the fact that intra-class type checking has to track the more refined effects, when a class is combined with other classes some additional inter-class checking is introduced.\r\n
Anderson C, Drossopoulou S, 2003, BabyJ: From object based to class based programming via types, Electronic Notes in Theoretical Computer Science, Vol: 82, Pages: 53-81, ISSN: 1571-0661
Object oriented programming can be classified into the object based, and the class based paradigm. Object based languages typically are weakly typed and interpreted, allow member addition and removal, and thus they support flexibility and prototyping. Class based languages are usually strongly typed and compiled, require a rigid class structure and class membership, and thus they support more robust, type safe programs. The two paradigms therefore address the needs of different stages in the programming lifecycle: object based programming better fits the earlier, exploratory phases, whereas class based better fits the latter, consolidation and maintenance phases. Because the transition from one paradigm to the other is not straightforward, programs tend to be developed in one of the two paradigms, thus foregoing the advantages of the other. We suggest that this need not be so, and that the benefits of the two paradigms can be combined: The earlier, exploratory, programming phases should take place in an object based setting. Then, the program should be incrementally annotated with types. Once fully typed, the program can be mapped onto an equivalent class based program. We demonstrate these ideas through the introduction of BabtJ, a formalization of Javascript. We define BabyJ T, a typed extension of BabyJ. A permissive type in BabyJ allows the typing process to be incremental. We then define a meaning preserving transformation of BabyJT programs to Java programs. ©2003 Published by Elsevier Science B.V.
Smith M, Drossopoulou S, 2003, Inner classes visit Aliasing, Formal techniques for Java-like languages, 2003
Anderson C, Drossopoulou S, 2003, BabyJ: from object based to class based programming via types, Electronic Notes in Theoretical Computer Science, Vol: 82, Pages: 1-29, ISSN: 1571-0661
Anderson C, Barbanera F, Dezani-Ciancaglini M, et al., 2003, Can addresses be types? A case study: objects with delegation, Electronic Notes in Theoretical Computer Science, Vol: 82, Pages: 108-129, ISSN: 1571-0661
Clarke D, Drossopoulou S, Noble J, 2003, Aliasing, confinement, and ownership in object-oriented programming, 17th European Conference on Object-Oriented Programming (ECOOP 2003), Publisher: SPRINGER-VERLAG BERLIN, Pages: 197-207, ISSN: 0302-9743
- Author Web Link
- Cite
- Citations: 3
Anderson C, Drossopoulou S, Dezani-Ciancaglini M, et al., 2003, Can Addresses be Types? (a case study: objects with delegation), Electronic Notes in Theoretical Computer Science, Vol: 82, Pages: 1-22, ISSN: 1571-0661
We adapt the aliasing constraints approach for designing a flexible typing of evolving \r\nobjects. Types are singleton types (addresses of objects, as a matter of fact) whose relevance \r\nis mainly due to the sort of safety property they guarantee. In particular we provide a type \r\nsystem for an imperative object based calculus with delegation and which supports method \r\nand delegate overriding, addition, and removing.
Drossopoulou S, Lagorio G, Eisenbach S, 2003, Flexible models for dynamic linking, Berlin, Joint European conference on theory and practice of software (ETAPS 2003), Warsaw, Poland, Publisher: Springer-Verlag, Pages: 38-53
Damiani F, Drossopoulou S, Giannini P, 2003, Refined effects for unanticipated object re-classification: Fickle(3), Berlin, 8th Italian conference on theoretical computer science (ICTCS 2003), Bertinoro, Italy, Publisher: Springer-Verlag, Pages: 97-110
Smith M, Drossopoulou S, 2003, Cheaper reasoning with ownership types, IWACO 2003
Clarke D, Drossopoulou S, 2002, Ownership, Encapsulation and the Disjointness of Types and Effects, 17th ACM SIGPLAN conference on Object-oriented programming, systems, languages, and applications (OOPSLA'02), Pages: 292-310
Ancona D, Anderson CL, Damiani F, et al., 2002, A type preserving translation of Fickle into Java
Drossopoulou S, Eisenbach S, 2002, Manifestations of Dynamic Linking, The First Workshop on Unanticipated Software Evolution (USE 2002), Mßlaga, Spain
Through dynamic linking, Java supports a novel paradigm for code deployment, which ensures fast program start-up and linking with the most recent version of code. Thus Java dynamic linking, gives support for software evolution, by supporting a piece of code A which uses a piece of code B, to link at run-time with a version of code B which was created after A was created.\r\n\r\nDynamic linking involves loading, verification, resolution and preparation of code. Programmers are normally not aware of the dynamic linking process. Nevertheless, in some situations, dynamic linking does manifest itself, and affects program execution and the integrity of the virtual machine. Therefore, there is a need for a description of dynamic linking at the level of the Java source language.\r\n\r\nWe provide such a description, and demonstrate the process in terms of a sequence of source language examples, in which the effects if dynamic linking are explicit.\r\n
Drossopoulou S, Damiani F, Dezani-Ciancaglini M, et al., 2002, More dynamic object re-classification: FickleII, ACM Transactions On Programming Languages and Systems, Vol: 24, Pages: 153-191, ISSN: 0164-0925
Drossopoulou S, Eisenbach S, Leavens GT, et al., 2002, Formal techniques for java-like programs, Pages: 203-210, ISSN: 0302-9743
This report gives an overview of the fourth ECOOP Workshop on Formal Techniques for Java-like Programs. It explains the motivation for such a workshop and summarizes the presentations and discussions.
Leavens G, Poetzsch-Heffter A, Eisenbach S, et al., 2002, Formal techniques for Java programs, Pages: 30-40
Anderson C, Drossopoulou S, 2002, Delta an object based calculus for delegation, USE workshop for at ECOOP 2002, June 2002, Malaga
Anderson C, Drossopoulou S, 2002, delta an imperative object based calculus, USE 2002
Object based, imperative languages with delegation (eg SELF) support exploratory programming: composition of objects, sharing of attributes and modification of objects' behaviour at run-time are easily expressible. Delegation allows objects to delegate execution of methods to other objects and to adapt delegated behaviour by overriding of method definitions. These features allow for creation of very flexible programs that can accommodate requirement changes at a very late stage.\r\n\r\n\r\nProgramming language design and understanding has generally benefited from formal models of programming languages. Such models, of course, tend to focus on the essential features of the particular language, making it possible to highlighting design alternatives and compare them. Models for object based languages have already been developed in the 90's, but these models do not directly express imperative delegation.\r\n\r\nWe argue that no calculi so far developed fully express the essence of such languages. We give a simple intuitive calculus for imperative object based delegation. We start with delta-, an imperative object based calculus, and demonstrate its use through examples. delta- is similar to the first order imperative Abadi Cardelli calculus, though simpler in some sense. We prove a correspondence theorem. We then present delta, which extends delta- through explicit delegation; delta allows an object to specify explicitly to which objects it wants to delegate. We show key features of delta through examples.
Leavens GT, Drossopoulou S, Eisenbach S, et al., 2002, Formal techniques for Java programs, Berlin, ECOOP 2001 workshop, Budapest, Hungary, 2001, Publisher: Springer-Verlag, Pages: 30-40
Ancona D, Anderson C, Damiani F, et al., 2001, An Effective Translation of Fickle into Java, 7th Italian Conference on Theoretical Computer Science, ICTCS 2001, Torino, Italy, October 4-6, 2001, Publisher: Springer, Pages: 215-234
We present a translation from Fickle (a Java-like language allowing dynamic object re-classification, that is, objects that can change their class at run-time) into plain Java. The translation is proved to preserve static and dynamic semantics; moreover, it is shown to be effective, in the sense that the translation of a Fickle class does not depend on the implementation of used classes, hence can be done in a separate way, that is, without having their sources, exactly as it happens for Java compilation. The aim is to demonstrate that an extension of Java supporting dynamic object re-classification could be fully compatible with the existing Java environment.
Drossopoulou S, 2001, An abstract model of Java dynamic linking and loading, Publisher: Springer, ISBN: 9783540421962
Drossopoulou S, Damiani F, zani-Ciancaglini M, et al., 2001, Fickle: dynamic object re-classification, Berlin, 15th European conference; object-oriented programming, ECOOP 2001, Publisher: Springer, Pages: 130-149
Ancona D, Drossopoulou S, 2001, Overloading and inheritance, Foundations of object oriented languages 8, London, January 2001
Drossopoulou S, Damiani F, zani-Ciancaglini M, et al., 2001, Dynamic object reclassification, Foundations of object oriented languages 8, London, January 2001
Ancona D, Anderson C, Damiani F, et al., 2001, An effective translation of Fickle into Java (Extended abstract), Berlin, 7th conference on theoretical computer science, Publisher: Springer c2001, Pages: 215-234
Drossopoulou S, 2001, An abstract model of Java dynamic linking and loading, New York, 3rd international workshop on types in compilation, 2001, Publisher: Springer, Pages: 53-84
Drossopoulou S, Eisenbach S, Valkevych T, 2000, Java Type Soundness Revisited, Publisher: Imperial College London, Department of Computing
We present an operational semantics, type system, and a proof of type soundness for a substantial subset of Java. The subset includes interfaces, classes, inheritance, field hiding, method overloading and overriding, arrays with associated dynamic checks, and exception handling.\r\n\r\nWe distinguish between normal execution, where no exception is thrown - or, more precisely, any exception thrown is handled - and abnormal execution, where an exception is thrown and not handled. The type system distinguishes normal types which describe the possible outcomes of normal execution, and abnormal types which describe the possible outcomes of abnormal execution. The type of a term consists of its normal type and its abnormal type.\r\n\r\nWith this set-up we prove subject reduction. Thus, the meaning of our subject reduction theorem is stronger than usual: it guarantees that normal execution returns a value of a type compatible with the normal type of the term, and that normal execution throws an exception compatible with the abnormal type of the term.\r\n\r\nWe also give a formalization of separate compilation and linking. We distinguish between Javas, Javab and Javar, which stand for the source language, the binary language and the run-time language. Javas closely reflects the Java syntax. Javab is a version of Java where field access and method call are enriched with type information; we consider Javab a high-level version of the byte code. Javar is an extension of Javab where we allow for addresses. Compilation maps Javas onto Javab and uses type information from Javab for the imported classes. The linker checks are reflected as well-formedness checks for Javab.\r\n\r\nFinally, we show that Javas and Javab can be viewed as a fragment system - an abstract model of separate compilation and linking which was introduced to investigate possible meanings of binary compatibility.\r\n
Drossopoulou S, Valkevych T, 2000, Java Exceptions Throw No Surprises, Publisher: Imperial College London, Department of Computing
We present a summary of our formalization of the static and dynamic semantics of Java related to exceptions. We distinguish between normal execution, where no exception is thrown - or, more precisely, any exception thrown is handled - and abnormal execution, where an exception is thrown and not handled. The type system distinguishes normal types which describe the possible outcomes of normal execution, and abnormal types which describe the possible outcomes of abnormal execution. The type of a term consists of its normal type and its abnormal type.\r\n\r\nThe meaning of our subject reduction theorem we prove with this set-up is stronger than usual: it guarantees that normal execution returns a value of a type compatible with the normal type of the term, and that abnormal execution throws an exception compatible with the abnormal type of the term.\r\n
Drossopoulou S, Eisenbach S, Jacobs B, et al., 2000, Formal Techniques for Java Programs., Publisher: Springer, Pages: 41-54
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.