Imperial College London
SLURP
Sound Languages Underpin Reliable Programming

Publications

ESOP 2006 Invited Talk

Language Design

Compilation and Dynamic Linking

Ownership Types

Software Engineering

Fickle: Dynamic Object Reclassification

Java Semantics

Process Calculi

Miscellaneous

Earlier Work

Multiple Ownership

Back to top

Nicholas Cameron, Sophia Drossopoulou, James Noble, Matthew Smith .PDF

@INPROCEEDINGS{ pubsdoc:multiple-ownership,
  booktitle = {OOPSLA 07},
  title = {{Multiple Ownership}},
  author = {Cameron, Nicholas and Drossopoulou, Sophia and Noble, James and Smith, Matthew},
  month = {October},
  year = {2007},
  url = {http://pubs.doc.ic.ac.uk/multiple-ownership/}
}

Existing ownership type systems require objects to have precisely one primary owner, organizing the heap into an ownership tree. Unfortunately, a tree structure is too restrictive for many programs, and prevents many common design patterns where multiple objects interact.

Multiple Ownership is an ownership type system where objects can have more than one owner, and the resulting ownership structure forms a DAG. We give a straightforward model for multiple ownership, focusing in particular on how multiple ownership can support a powerful effect system that determines when two computations interfere - in spite of the DAG structure.

We present a core programming language MOJO, Multiple Ownership for Java-like Objects, including a type and effects system, and soundness proof. In comparison to other systems, MOJO imposes absolutely no restrictions on pointers, modifications or programs' structure, but in spite of this, MOJO's effects can be used to reason about or describe programs' behaviour.

Towards an Existential Types Model for Java Wildcards

Back to top

Nicholas Cameron, Erik Ernst, Sophia Drossopoulou .PDF

@INPROCEEDINGS{ pubsdoc:towards-existential-wildcards,
  booktitle = {Formal Techniques for Java-like Programs (FTfJP) 2007},
  title = {{Towards an Existential Types Model for Java Wildcards}},
  author = {Cameron, Nicholas and Ernst, Erik and Drossopoulou, Sophia},
  month = {July},
  year = {2007},
  url = {http://pubs.doc.ic.ac.uk/towards-existential-wildcards/}
}

Wildcards extend Java generics by softening the mismatch between subtype and parametric polymorphism. Although they are a key part of the Java 5.0 programming language, a type system including wildcards has never been proven type sound. Wildcards have previously been formalised as existential types. In this paper we extend FGJ, a featherweight formalisation of Java with generics, with existential types. We prove that this calculus, ExistsJ, is type sound, and illustrate how it models wildcards in the Java Programming Language. ExistsJ is not a full model for Java wildcards, because it does not support lower bounds for wildcards. We discuss why ExistsJ can not be easily extended with lower bounds, and how full Java wildcards could be modelled in a type sound way.

Tribe: A Simple Virtual Class Calculus

Back to top

Dave Clarke, Sophia Drossopoulou, James Noble and Tobias Wrigstad
.PDF

@inproceedings{Tribe,
 author    = {Dave Clarke and Sophia Drossopoulou and James Noble and Tobias Wrigstad},
 title     = {Tribe: A Simple Virtual Class Calculus},
 booktitle = {Sixth International Conference on Aspect-Oriented Software Development (AOSD 2007)},
 year      = {2007},
 month     = {March},
 address   = {Vancouver, British Columbia, Canada}
}

Beginning with Beta, a range of programming language mechanisms such as virtual classes (class-valued attributes of objects) have been developed to allow inheritance in the presence of mutually dependent classes. This paper presents Tribe, a type system which generalises and simplifies other formalisms of such mechanisms, by treating issues which are inessential for soundness, such as the precise details of dispatch and field initialisation, as orthogonal to the core formalism. Tribe can support path types dependent simultaneously on both classes and objects, which is useful for writing library code, and ubiquitous access to an object's family, which offers family polymorphism without the need to drag around family arguments. Languages based on Tribe will be both simpler and more expressive than existing designs, while having a simpler type system, serving as a useful basis for future language designs.

A state abstraction for coordination in Java-like languages

Back to top

Ferruccio Damiani, Elena Giachino, Paola Giannini, Nick Cameron, Sophia Drossopoulou
.PDF

@inproceedings{ stateabstraction-ftfjp06,
 author    = {Ferruccio Damiani and Elena Giachino and Paola Giannini and Nick Cameron and Sophia Drossopoulou},
 title     = {A state abstraction for coordination in Java-like languages},
 booktitle = {ECOOP Workshop on Formal Techniques for Java Programs (FTfJP 2006)},
 year      = {2006},
 month     = {July},
 address   = {Nantes, France}
}

Objects’ state, intended as some abstraction over the value of fields, is always in the mind of a COOL (Concurrent Object-Oriented Language) programmer. In fact, as the state of an object changes so does its coordination behaviour.

We introduce a language feature for expressing the notion of state in Java-like languages. The proposed feature takes the form of state class, a new kind of class, equipped with a static type and effect system guaranteeing that during the execution of a method on a receiver o: (1) Even though the state of o may vary through states with different parameters, no attempt will be made to access non-existing parameters, and (2) No method invoked on a receiver different from this may cause (through method calls on o) a change in the state of o.

Session Types for Object-Oriented Languages

Back to top

Mariangiola Dezani-Ciancaglini, Dimitris Mostrous, Nobuko Yoshida and Sophia Drossopoulou
.PDF

@unpublished{ sessiontypesforoolanguages,
 author    = {Mariangiola Dezani-Ciancaglini and Dimitris Mostrous and Nobuko Yoshida and Sophia Drossopoulou},
 title     = {Session Types for Object-Oriented Languages},
 year      = {2005},
 month     = {December}
}

A session takes place between two parties; after establishing a connection, each party interleaves local computations with communications (sending or receiving) with the other party. Session types characterise such sessions in terms of the types of values communicated and the shape of protocols, and have been developed for the pi-calculus, CORBA interfaces, and functional languages. We study the incorporation of session types into object-oriented languages through the language Moose, a multi-threaded language with session types, thread spawning, iterative and higher-order sessions. Our design aims to consistently integrate the object-oriented programming style and sessions, and to treat various case studies from the literature. We describe the design of Moose, its syntax, operational semantics and type system, and develop a type inference system. After proving subject reduction, we establish the progress property: once a communication has been established, well-typed programs will never starve at communication points.

Tribe: More Types for Virtual Classes

Back to top

Dave Clarke, Sophia Drossopoulou, James Noble and Tobias Wrigstad
.PDF

@unpublished{ tribe,
 author    = {Dave Clarke and Sophia Drossopoulou and James Noble and Tobias Wrigstad},
 title     = {Tribe: More Types for Virtual Classes},
 year      = {2005},
 month     = {December}
}

Note that this work has been superceded by Tribe: A Simple Virtual Class Calculus

Beginning with Beta, a range of programming language mechanisms have been developed to allow inheritance in the presence of mutually dependent classes. This paper presents Tribe, a type system which generalises and simplifies other formalisms of such mechanisms, by treating issues which are inessential for soundness, such as the precise details of dispatch and path initialisation, as orthogonal to the core formalism. Tribe can support path types dependent simultaneously on both classes and objects, which is useful for writing library code, and ubiquitous access to an object's family (= owner), which offers family polymorphism without the need to drag around family arguments. Languages based on Tribe will be both simpler and more expressive than existing designs, while having a simpler type system, serving as a useful basis for future language designs.

A Concurrency Model of Chorded Languages

Back to top

Sophia Drossopoulou, Susan Eisenbach and Alexis Petrounias
Mini-site

@unpublished{ concurrencymodelofchordedlanguages,
 author    = {Sophia Drossopoulou and Susan Eisenbach and Alexis Petrounias},
 title     = {A Concurrency Model of Chorded Languages},
 year      = {2005},
 month     = {December}
}

Chords are a concurrency mechanism of object-oriented language inspired by the join of the Join-calculus. We present a formal model of chorded languages, namely the Small Chorded Object-Oriented Language (SCHOOL), a minimal language which aims to capture the essence of the concurrent behaviours of chords. Furthermore we study the interaction of chords with fields, a standard feature of many object-oriented language. We achieve this by extending SCHOOL to include fields, resulting in fdSCHOOL. Fields can be encoded using only chords; hence fields are a macro-expansion of chords and do not increase the expressive power of SCHOOL. We show this by means of a translation between the two languages and proof of equivalence.

Towards Type Inference for JavaScript

Back to top

Christopher Anderson, Paola Giannini and Sophia Drossopoulou
.PDF

@inproceedings{ typeinferenceforjavascript-ecoop05,
 author    = {Christopher Anderson and Paola Giannini and Sophia Drossopoulou},
 title     = {Type Inference for Scripting Languages},
 booktitle = {19th European Conference on Object-Oriented Programming (ECOOP 2005)},
 year      = {2005},
 month     = {July},
 address   = {Glasgow, Scotland}
}

Object-oriented scripting languages like JavaScript and Python are popular partly because of their dynamic features. These include the runtime modification of objects and classes through addition of fields or updating of methods. These features make static typing difficult and so usually dynamic typing is used. Consequently, errors such as access to non-existent members are not detected until runtime.

We first develop a formalism for an object based language, JS0, with features from JavaScript, including dynamic addition of fields and updating of methods. We give an operational semantics and static type system for JS0 using structural types. Our types allow objects to evolve in a controlled manner by classifying members as definite or potential.

We define a type inference algorithm for JS0 that is sound with respect to the type system. If the type inference algorithm succeeds, then the program is typeable. Therefore, programmers can benefit from the safety offered by the type system, without the need to write explicitly types in their programs.

Chai: Traits for Java-like Languages

Back to top

Charles Smith and Sophia Drossopoulou
.PDF

@inproceedings{ chaitraits-ecoop05,
 author    = {Charles Smith and Sophia Drossopoulou},
 title     = {Chai: Typed Traits in Java},
 booktitle = {19th European Conference on Object-Oriented Programming (ECOOP 2005)},
 year      = {2005},
 month     = {July},
 address   = {Glasgow, Scotland}
}

Traits support the factoring out of common behaviour, and its integration into classes in a manner that coexists smoothly with inheritance-based structuring mechanisms.

We designed the language Chai, which incorporates statically typed traits into a simple Java-like base language, and we discuss three versions of the language: Chai1, where traits are only a mechanism for the creation of classes; Chai2, where traits are a mechanism for the creation of classes, and can also introduce types, and Chai3 where traits play a role at runtime, and can be applied to objects, and change the objects’ behaviour. We give formal models for these languages, outline the proof of soundness, and our prototype implementation.

A Distributed Object-Oriented language with Session types

Back to top

Mariangiola Dezani-Ciancaglini, Nobuko Yoshida, Alexander Ahern and Sophia Drossopoulou
.PDF

@inproceedings{ distributedoowithsessiontypes-tgc05,
 author    = {Mariangiola Dezani-Ciancaglini and Nobuko Yoshida and Alexander Ahern and Sophia Drossopoulou},
 title     = {A Distributed Object-Oriented language with Session types},
 booktitle = {ETAPS International Symposium on Trustworthy Global Computing (TGC 2005)},
 year      = {2005},
 month     = {April},
 address   = {Edinburgh, Scotland}
}

In the age of the world-wide web and mobile computing, programming communication-centric software is essential. Thus, programmers and program designers are exposed to new levels of complexity, such as ensuring the correct composition of communication behaviours and guaranteeing deadlock-freedom of their protocols.

This paper proposes the language Ldoos, a simple distributed object-oriented language augmented with session communication primitives and types. Ldoos provides a flexible object-oriented programming style for structural interaction protocols by prescribing channel usages within signatures of distributed classes.

We develop a typing system for Ldoos and prove its soundness with respect to the operational semantics. We also show that in a well-typed Ldoos program, there will never be a connection error, a communication error, nor an incorrect completion between server-client interactions. These results demonstrate that a consistent integration of object-oriented language features and session types offers a compositional method to statically check safety of communication protocols.

SCHOOL: a Small Chorded Object-Oriented Language

Back to top

Sophia Drossopoulou, Alexis Petrounias, Alex Buckley and Susan Eisenbach
.PDF (Long, Unpublished) .PDF (Short, Published at DCM'05)

@unpublished{ school-long,
 author    = {Sophia Drossopoulou and Alexis Petrounias and Alex Buckley and Susan Eisenbach},
 title     = {SCHOOL: a Small Chorded Object-Oriented Language},
 year      = {2005},
 month     = {March}
}
@inproceedings{ school-dcm,
 author    = {Sophia Drossopoulou and Alexis Petrounias and Alex Buckley and Susan Eisenbach},
 title     = {SCHOOL: a Small Chorded Object-Oriented Language},
 booktitle = {ICALP International Workshop on Developments in Computational Models (DCM 2005)},
 year      = {2005},
 month     = {July},
 address   = {Lisbon, Portugal}
}

Chords are a declarative synchronisation construct based on the Join calculus, available in C-Omega. Compared with synchronisation constructs in most imperative languages, chords promise development of programs that are more succinct, easier to read, and easier to reason about. However, to our knowledge, chords have no formal model in an object-oriented setting.

In this paper we suggest SCHOOL, a formal model for an object-oriented language with chords. We give an operational semantics and type system, and prove soundness of the type system.

SCHOOL is minimal, supporting only classes, inheritance and chords. To prove that SCHOOL is sufficient, we define SCHOOL+F, an extension of SCHOOL with fields. We develop an encoding of SCHOOL+F into SCHOOL, and prove soundness and completness of the encoding with respect to the type system and the operational semantics.

SCHOOL proofs are available.

Please compare with newer work A Concurrency Model of Chorded Languages

Simple Dependent Types: Concord

Back to top

Paul Jolly, Sophia Drossopoulou, Christopher Anderson and Klaus Ostermann
.PDF

@inproceedings{ concord-ftfjp04,
 author    = {Paul Jolly and Sophia Drossopoulou and Christopher Anderson and Klaus Ostermann},
 title     = {Simple Dependent Types: Concord},
 booktitle = {ECOOP Workshop on Formal Techniques for Java Programs (FTfJP 2004)},
 year      = {2004},
 month     = {June},
 address   = {Oslo, Norway},
 url       = {http://myitcv.org.uk/papers/concord04.html}
}

We suggest a simple model for a restricted form of dependent types in object oriented languages, whereby classes belong to groups and dependency is introduced via intra-group references using the MyGrp keyword. We show how our approach can code well-known examples from the literature, present the formal model and outline soundness of the type system.

Flexible Dynamic Linking for .NET

Back to top

Anders Aaltonen, Alex Buckley and Susan Eisenbach
.PDF

@article{ flexibledynamiclinkingfordotnet,
 author  = {Anders Aaltonen and Alex Buckley and Susan Eisenbach},
 title   = {Flexible Dynamic Linking for .NET},
 journal = {Journal of .NET Technologies},
 year    = {2006},
 month   = {June},
 volume  = {4},
 note    = {Presented at .NET Technologies 2006, Plzen, Czech Republic},
 url     = {http://dotnet.zcu.cz/NET_2006/NET_2006.htm}
}

A modern object-oriented application is a set of components developed or reused by programmers, and tested together for correctness and performance. Each component’s dependencies on other components are type-checked at compile-time and embedded into the executable image, from where they guide the dynamic linking process.

We propose that an application can potentially consist of multiple sets of components, all known to the application’s programmers. Each set implements the application’s functionality in some special way, e.g. using only patent-free algorithms or being optimised for 64-bit processors. Depending on the components available on a user’s machine, the dynamic linking process will select a suitable set and load components from it.

We describe our approach for writing programs that use a "default" set of components and carry nominal and structural specifications about permissible sets of alternative components. We modified the linking infrastructure of Rotor, a .NET VM, to effciently and safely find components on the user’s machine that satisfy the programmer’s specifications. Specifications can be applied to individual classes and methods, so only code that might want to use alternative code needs to undergo the modified linking process.

A Model of Dynamic Binding in .NET

Back to top

Alex Buckley
.PDF (FTfJP 2005) .PDF (Component Deployment 2005)

@inproceedings{ dynamicbindingindotnet,
 author    = {Alex Buckley},
 title     = {A Model of Dynamic Binding in .NET},
 booktitle = {ECOOP Workshop on Formal Techniques for Java Programs (FTfJP 2005)},
 year      = {2005},
 month     = {July},
 address   = {Glasgow, Scotland}
}

Millions of programmers use ECMA CLI-compliant languages like VB.NET and C#. The resulting bytecode can be executed on several CLI implementations, such as those from Microsoft and the open-source Mono organisation. While assemblies are the standard unit of deployment, no standard exists for the process of finding and loading assemblies at run-time. The process is typically complex, and varies between CLI implementations. Unlike other linking stages, such as verification, it is visible to programmers and can be a source of confusion.

We offer a framework that describes how assemblies are resolved, loaded and used in CLI implementations. We strive for implementation-independence and note how implementations from different organisations vary in behaviour. We describe the reflection features available for dynamic loading, and give C# examples that exercise the features modelled in the framework.

Flexible Bytecode for Linking in .NET

Back to top

Alex Buckley, Michelle Murray, Susan Eisenbach and Sophia Drossopoulou
.PDF

@inproceedings{ flexiblebytecodefordotnet-bytecode05,
 author    = {Alex Buckley and Michelle Murray and Susan Eisenbach and Sophia Drossopoulou},
 title     = {Flexible Bytecode for Linking in .NET},
 booktitle = {ETAPS Workshop on Bytecode Semantics, Verification, Analysis and Transformation (BYTECODE 2005)},
 year      = {2005},
 month     = {April},
 address   = {Edinburgh, Scotland},
 url       = {http://profs.sci.univr.it/~spoto/Bytecode05/}
}

Dynamic linking in modern execution environments like .NET is considerably more sophisticated than in the days of C shared libraries on UNIX. One aspect of this sophistication is that .NET assemblies embed type information about dynamically linked resources.

This type information implicitly represents compile-time assumptions about the resources available at run-time. However, at run-time, different resources may actually be available. For example, the execution environment on a mobile phone might provide fewer, simpler classes than on a desktop PC.

We have designed and implemented a "flexible" dynamic linking scheme that supports the run-time selection of .NET assemblies and classes. This enables a regime of "compile once, run anywhere". We describe the scheme's integration with the .NET linking infrastructure, review important design decisions and report on experiences with the "Rotor" shared source version of .NET.

Polymorphic Bytecode: Compositional Compilation for Java-like Languages

Back to top

Davide Ancona, Ferruccio Damiani, Sophia Drossopoulou and Elena Zucca
.PDF

@inproceedings{ polymorphicbytecode-popl05,
 author    = {Davide Ancona and Ferruccio Damiani and Sophia Drossopoulou and Elena Zucca},
 title     = {Polymorphic Bytecode: Compositional Compilation for Java-like Languages},
 booktitle = {Proceedings of the 32nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL 2005)},
 year      = {2005},
 month     = {January},
 address   = {Long Beach, CA, USA}
}

We define compositional compilation to be the ability to typecheck source code fragments in isolation, generate corresponding binaries, and link together fragments whose mutual assumptions are satisfied, without reinspecting the code. Even though compositional compilation is a highly desirable feature, in Java-like languages it can hardly be achieved. This is due to the fact that the bytecode generated for a fragment (say, a class) is not uniquely determined by its source code, but depends on the compilation context.

In this paper, we propose a way to obtain compositional compilation for Java, by introducing a polymorphic form of bytecode containing type variables (ranging over class names) and equipped with a set of constraints involving type variables. Thus, polymorphic bytecode provides a representation for all the (standard Java) bytecode that can be obtained by replacing type variables with class names satisfying the associated constraints.

We illustrate our proposal by developing a type inference and a linking algorithm for a small subset of Java. The type inference algorithm compiles a class in isolation generating the corresponding polymorphic bytecode fragment with the needed constraints on the classes it depends on. The linking algorithm takes a collection of polymorphic bytecode fragments, checks their mutual consistency, and possibly simplifies and specializes them. In particular, when a self-contained collection of fragments is taken, linking either fails, or produces standard Java bytecode (which is the same as the one which would have been produced by standard Java compilation of all fragments together).

Safety in Flexible Dynamic Linking

Back to top

Alex Buckley and Sophia Drossopoulou
.PDF

@unpublished{ safetyinflexibledynamiclinking,
 author    = {Alex Buckley and Sophia Drossopoulou},
 title     = {Safety in Flexible Dynamic Linking},
 year      = {2004},
 month     = {October}
}

Dynamic linking lets programs use the most recent versions of classes without re-compilation. In Java and .NET, bytecode specifies which classes should be dynamically linked. This information represents the compiler's knowledge of the compilation environment, but the execution environment might be different. For example, the execution environment on a mobile phone might provide fewer, simpler classes than on a desktop PC. As bytecode cannot adapt to its execution environment, component reuse is restricted and development costs are increased.

We suggest flexible dynamic linking that binds bytecode as late as possible to the classes available in an execution environment. Rather than specifying classes, bytecode contains type variables that are substituted by classes as late as execution. We present a non-deterministic model that treats substitution as a linking step, and interleaves linking with execution. We examine how linking builds a well-formed program and prove soundness for the laziest substitution strategy, representing the most general execution.

Flexible Dynamic Linking

Back to top

Alex Buckley and Sophia Drossopoulou
.PDF

@inproceedings{ flexibledynamiclinking-ftfjp04,
 author    = {Alex Buckley and Sophia Drossopoulou},
 title     = {Flexible Dynamic Linking},
 booktitle = {ECOOP Workshop on Formal Techniques for Java Programs (FTfJP 2004)},
 year      = {2004},
 month     = {June},
 address   = {Oslo, Norway},
 url       = {http://www.cs.kun.nl/~erikpoll/ftfjp/2004.html}
}

Dynamic linking, as in Java and C#, allows users to execute the most recent versions of software without re-compilation or re-linking. Dynamic linking is guided by type names stored in the bytecode.

In current dynamic linking schemes, these type names are hard-coded into the bytecode. Thus, the bytecode reflects the compilation environment that produced it. However, the compilation environment need not be the same as the execution environment: a class may be replaced by one that offers the "same" services but has a different name. Such changes are not supported by current linking schemes.

We suggest a more flexible approach to dynamic linking, where bytecode contains type variables rather than types, and where these type variables are substituted during execution. We develop a non-deterministic system that allows type variable substitution at many different points, and sketch a proof of soundness.

Even More Principal Typings for Java-like Languages

Back to top

Davide Ancona, Ferruccio Damiani, Sophia Drossopoulou and Elena Zucca
.PDF

@inproceedings{ evenmore-ftfjp04,
 author    = {Davide Ancona and Ferruccio Damiani and Sophia Drossopoulou and Elena Zucca},
 title     = {Even More Principal Typings for Java-like Languages},
 booktitle = {ECOOP Workshop on Formal Techniques for Java Programs (FTfJP 2004)},
 year      = {2004},
 month     = {June},
 address   = {Oslo, Norway}
}

We propose a new type system for Java-like languages which allows compilation of a class in isolation, that is, in a context where no information is available on other classes. Indeed, by this type system it is possible to infer the assumptions guaranteeing type correctness of a class c, and generate (abstract) bytecode for c, by just inspecting the source code of c. Then, a collection of classes can be safely linked together without further inspection of the classes' code, provided that each class has been typechecked in isolation (intra-checking), and that the mutual class assumptions are satisfied (inter-checking). In other words, the type system supports compositional analysis, as formally guaranteed by the fact that it has principal typings. We also develop an algorithm for inter-checking, and prove it correct.

Flexible, source level dynamic linking and re-linking

Back to top

Sophia Drossopoulou and Susan Eisenbach
.PDF

@inproceedings{ flexiblelinking-ftfjp03,
 author    = {Sophia Drossopoulou and Susan Eisenbach},
 title     = {Flexible, {S}ource level {D}ynamic {L}inking and re-linking},
 booktitle = {ECOOP Workshop on Formal Techniques for Java Programs (FTfJP 2003)},
 year      = {2003},
 month     = {July},
 address   = {Darmstadt, Germany},
 url       = {http://www.cs.kun.nl/~erikpoll/ftfjp/2003.html}
}

We give a formal semantics for dynamic linking and re-linking of code. The semantics is at source language level, and allows linking at a finer grain than current Java or C# implementations: Besides supporting the loading and verification of classes interleaved with program execution, it also allows type-safe removal and replacement of classes, fields and methods. Such extended features support unanticipated software evolution.

Flexible Models for Dynamic Linking

Back to top

Sophia Drossopoulou, Giovanni Lagorio and Susan Eisenbach
.PDF .PS (Extended version)

@inproceedings{ flexiblemodels-esop03,
 author    = {Sophia Drossopoulou and Giovanni Lagorio and Susan Eisenbach},
 title     = {Flexible {M}odels for {D}ynamic {L}inking},
 booktitle = {12th European Symposium on Programming (ESOP 2003)},
 year      = {2003},
 month     = {April},
 series    = {LNCS},
 volume    = {2618},
 pages     = {38--53},
 publisher = {Springer-Verlag},
 editor    = {Pierpaolo Degano}
}

Dynamic linking supports flexible code deployment: partially linked code links further code on the fly, as needed; and thus, end-users receive updates automatically. On the down side, each program run may link different versions of the same code, possibly causing subtle errors which mystify end-users.

Dynamic linking in Java and C# are similar: The same linking phases are involved, soundness is based on similar ideas, and executions which do not throw linking errors give the same result. They are, however, not identical: the linking phases are combined differently, and take place in different order. Thus, linking errors may be detected at different times in Java and C#.

We develop a non-deterministic model, which includes the behaviour of Java and C#. The non-determinism allows us to describe the design space, to distill the similarities between the two languages, and to use one proof of soundness for both. We also prove that all execution strategies are equivalent in the sense that all terminating executions which do not involve a link error, give the same result.

Manifestations of Dynamic Linking

Back to top

Sophia Drossopoulou and Susan Eisenbach
.PDF

@inproceedings{ manifestations-use02,
 author    = {S. Drossopoulou and S. Eisenbach},
 title     = {Manifestations of {D}ynamic {L}inking},
 booktitle = {The First Workshop on Unanticipated Software Evolution (USE 2002)},
 year      = {2002},
 month     = {June},
 address   = {Málaga, Spain},
 publisher = {http://joint.org/use2002/proceedings.html}
}

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.

Dynamic 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.

We 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.

An abstract model of Java dynamic linking and loading

Back to top

Sophia Drossopoulou
.PS

@inproceedings{ abstractmodel-tic00,
 title     = {An abstract model of Java dynamic linking and loading},
 author    = {Sophia Drossopoulou},
 booktitle = {Third International Workshop, Types in Compilation (TIC 2000)}
 year      = {2000},
 series    = {LNCS},
 volume    = {2071},
 pages     = {53--84},
 editor    = {Robert Harper},
 publisher = {Springer-Verlag}
}

We suggest a model for dynamic linking and verification as in Java. We distinguish five components in a Java implementation: evaluation, resolution, loading, verification, and preparation - with their associated checks. We demonstrate how these five together guarantee type soundness. We concentrate on giving a comprehensive description of the role of the five components and their dependencies, rather than a faithful model of each in isolation, and do not yet consider multiple loaders.

We take an abstract view, and base our model on a language nearer to Java source than to bytecode. We consider the following features of Java: classes, subclasses, fields and hiding, methods, overloading and inheritance, interfaces and subinterfaces. We chose these features because the corresponding checks for each for these is guaranteed by different components.

The main difference between the current and previous, informally distributed versions of this work is the study of interfaces, and the more faithful description of the timing of possible loading.

Cheaper Reasoning with Ownership Types

Back to top

Matthew Smith and Sophia Drossopoulou
.PDF

@inproceedings{cheaperreasoning-iwaco03,
 author    = {Matthew Smith and Sophia Drossopoulou},
 title     = {Cheaper {R}easoning with {O}wnership {T}ypes},
 booktitle = {ECOOP International Workshop on Aliasing, Confinement and Ownership (IWACO 2003)},
 year      = {2003},
 url       = {http://www.cs.uu.nl/~dave/iwaco/}
}

We use ownership types to facilitate program verification. An assertion that has been established for a part of the heap which is unaffected by some execution will still be hold after this execution. We use ownership and effects, and extend them to assertions to be able to make judgements as to which executions do not affect which assertions. We describe our ideas in terms of an example, and outline the formal system.

Ownership, Encapsulation and the Disjointness of Types and Effects

Back to top

Dæv Clarke and Sophia Drossopoulou
.PS

@inproceedings{ ownershipdisjointness-oopsla02,
 author    = {Dæv Clarke and Sophia Drossopoulou},
 title     = {Ownership, {E}ncapsulation and the {D}isjointness of {T}ypes and {E}ffects},
 booktitle = {Proceedings of the 17th ACM SIGPLAN conference on Object-oriented programming, systems, languages, and applications (OOPSLA'02)},
 year      = {2002},
 month     = {November},
 address   = {Seattle, Washington, USA},
 pages     = {292--310},
 publisher = {ACM Press}
}

Ownership types provide a statically enforceable notion of object-level encapsulation. We extend ownership types with computational effects to support reasoning about object-oriented programs. The ensuing system provides both access control and effects reporting. Based on this types system, we codify two formal systems for reasoning ebout aliasing and the disjointness of computational effects. The first can be used to prove that evaluation of two expressions will never lead to aliases, while the latter can be used to show the non-interference of two expressions.

Ownership Types Restrict Aliasing

Back to top

Alex Buckley
.PDF

@mastersthesis{ restrictaliasing-meng00,
 author = {Alex Buckley},
 title  = {Ownership {T}ypes {R}estrict {A}liasing},
 school = {Department of Computing, Imperial College London},
 year   = {2000}
}

Object-oriented programming languages allow references to create multiple aliases to the same object. This permits object sharing, and gives programmers the ability to model real-world phenomena through networks of interacting objects. However, the possibility that an object's internal state may be modified through an alias to it adds complexity and makes reasoning and optimisation of the code more difficult.

Ownership types embed the notion of object ownership into the type system. Every object has an owner that strongly encapsulates the objects that it owns. Aliasing may only occur where the programmer uses ownership types that permit it.

This thesis presents an implementation of ownership types for Java, and extends it with new notions of ownership. It also presents a scheme for dynamic validation of a program's ownership model.

Keeping Control of Reusable Components

Back to top

Susan Eisenbach, Dilek Kayhan and Chris Sadler
.PDF

@inproceedings{ control-cd04,
 author    = {Susan Eisenbach and Dilek Kayhan and Chris Sadler},
 title     = {Keeping {C}ontrol of {R}eusable {C}omponents},
 booktitle = {Proceedings of Component Deployment (CD 2004)},
 year      = {2004},
 month     = {May},
 address   = {Edinburgh, Scotland}
}

Development and deployment via components offers the possibility of prolific software reuse. However, to achieve this potential in a component-rich environment, it is necessary to recognize that component deployment (and subsequent composition) is closer to a continual process than a one-off operation. This is due to the requirement that newly-evolved components need to replace their ancestors in a timely and efficient manner at the client deployment sites. Modern runtime systems which employ dynamic link-loading mechanisms can permit such dynamic evolution. We review the capabilities of several alternative runtime environments to establish some requirements for dynamic evolution. Then we describe a tool designed to support developers and administrators in the migration of component updates within the Microsoft .NET framework.

MagicBeans: a Platform for Deploying Plugin Components

Back to top

Robert Chatley, Susan Eisenbach and Jeff Magee
.PDF

@inproceedings{ magicbeans-cd04,
 author    = {Robert Chatley and Susan Eisenbach and Jeff Magee},
 title     = {MagicBeans: a {P}latform for {D}eploying {P}lugin {C}omponents},
 booktitle = {Proceedings of Component Deployment (CD 2004)},
 year      = {2004},
 month     = {May},
 address   = {Edinburgh, Scotland}
}

Plugins are optional components which can be used to enable the dynamic construction of flexible and complex systems, passing as much of the configuration management effort as possible to the system rather than the user, allowing graceful upgrading of systems over time without stopping and restarting. Using plugins as a mechanism for evolving applications is appealing, but current implementations have limited functionality. In this paper we present a framework that supports the construction and evolution of applications with a plugin architecture.

Predictable Dynamic Plugin Systems

Back to top

Robert Chatley, Susan Eisenbach and Jeff Magee
.PDF

@inproceedings{ predictable-fase04,
 author    = {Robert Chatley and Susan Eisenbach and Jeff Magee},
 title     = {Predictable {D}ynamic {P}lugin {S}ystems},
 booktitle = {Proceedings of Fundamental Approaches to Software Engineering (FASE 2004)},
 year      = {2004},
 month     = {March},
 address   = {Barcelona, Spain}
}

To be able to build systems by composing a variety of components dynamically, adding and removing as required, is desirable. Unfortunately systems with evolving architectures are prone to behaving in a surprising manner. In this paper we show how it is possible to generate a snapshot of the structure of a running application, and how this can be combined with behavioural specifications for components to check compatibility and adherence to system properties. By modelling both the structure and the behaviour, before altering an existing system, we show how dynamic compositional systems may be put together in a predictable manner.

Managing the Evolution of .NET Programs

Back to top

Susan Eisenbach, Vladimir Jurisic and Chris Sadler
.PDF

@inproceedings{ evolutiondotnet-fmoods03,
 author    = {S. Eisenbach and V. Jurisic and C. Sadler},
 title     = {Managing the {E}volution of .{NET} {P}rograms},
 booktitle = {6th IFIP International Conference on Formal Methods for Open Object-based Distributed Systems (FMOODS 2003)},
 year      = {2003},
 month     = {November},
 address   = {Paris, France},
 series    = {LNCS},
 volume    = {2884},
 pages     = {185--198},
 publisher = {Springer-Verlag}
}

The component-based model of code execution imposes some requirements on the software components themselves, and at the same time lays some constraints on the modern run-time environment. Software components need to store descriptive metadata, and the run-time system must access this 'reflectively' in order to implement dynamic linking. Software components also undergo dynamic evolution whereby a client component experiences the effects of modifications, made to a service component even though these occurred after the client was built.

We wanted to see whether the dynamic linking mechanism implemented in Microsoft's .NET environment could be utilized to maintain multiple versions of components. A formal model was developed to assist in understanding the .NET mechanism and in describing our way of dealing with multiple versions. This showed that .NET incorporates all the features necessary to implement such a scheme and we constructed a tool to do so.

Modelling a Framework for Plugins

Back to top

Robert Chatley, Susan Eisenbach and Jeff Magee
.PDF

@inproceedings{ plugins-savcbs03,
 author    = {R. Chatley and S. Eisenbach and J. Magee},
 title     = {Modelling a {F}ramework for {P}lugins},
 booktitle = {Specification and Verification of Component-Based Systems},
 year      = {2003},
 month     = {September},
 publisher = {http://www.cs.iastate.edu/~leavens/SAVCBS/2003/papers/}
}

Using plugins as a mechanism for extending applications to provide extra functionality is appealing, but current implementations are limited in scope. We have designed a framework to allow the construction of flexible and complex systems from plugin components. In this paper we describe how the use of modelling techniques helped in the exploration of design issues and refine our ideas before implementing them. We present both an informal model and a formal specification produced using Alloy. Alloy's associated tools allowed us to analyse the plugin system's behaviour statically.

Safe Upgrading without Restarting

Back to top

Miles Barr and Susan Eisenbach
.PDF

@inproceedings{ upgrading-icsm03,
 author    = {M. Barr and S. Eisenbach},
 title     = {Safe {U}pgrading without {R}estarting},
 booktitle = {IEEE Conference on Software Maintenance (ICSM 2003)},
 year      = {2003},
 month     = {Sept},
 publisher = {IEEE}
}

The distributed development and maintenance paradigm for component delivery is fraught with problems. One wants a relationship between developers and clients that is autonomous and anonymous. Yet components written in languages such as C++ require the recompilation of all dependent subsystems when a new version of a component is released. The design of Java's binary format has side-stepped this constraint, removing the need for total recompilation with each change. But the potential is not fulfilled if programs have to be stopped to swap in each new component.

This paper describes a framework that allows Java programs to be dynamically upgraded. Its key purpose is to allow libraries that are safe to replace existing libraries without adversely affecting running programs. The framework provides developers with a mechanism to release their libraries and provides clients with the surety of only upgrading when it is safe to do so.

Feeling the way through DLL Hell

Back to top

Susan Eisenbach, Vladimir Jurisic and Chris Sadler
.PDF

@inproceedings{ dllhell-use02,
 author    = {S. Eisenbach and V. Jurisic and C. Sadler},
 title     = {Feeling the way through {DLL} {H}ell},
 booktitle = {The First Workshop on Unanticipated Software Evolution (USE 2002)},
 year      = {2002},
 month     = {June},
 place     = {Málaga, Spain},
 publisher = {http://joint.org/use2002/}
}

Dynamic linking provides a way to share code components across applications and across the network. But managing these relationships as new code versions are developed gives rise to a range of problems well recognized by system support personnel. Operating system and language designers attempt to design solutions to these problems into the latest versions of their products. In this paper we report on some troublesome features that crop up in the runtime systems of object-oriented languages designed for distributed code-sharing.

Evolution of Distributed Java Programs

Back to top

Susan Eisenbach, Chris Sadler and Shakil Shaikh
.PDF .PDF (Short version)

@inproceedings{ evolutionjava-cocd02,
 author    = {S. Eisenbach, C. Sadler and S. Shaikh},
 title     = {Evolution of {D}istributed {J}ava {P}rograms},
 booktitle = {IFIP/ACM Working Conference on Component Deployment (COCD 2002)},
 year      = {2002},
 month     = {June},
 series    = {LNCS},
 volume    = {2370},
 publisher = {Springer-Verlag}
}

A major challenge of maintaining object-oriented programs is to find a means of evolving software that already has a distributed client base. This should be easier for Java developers than for most, because dynamic linking has been designed into the runtime system. It turns out however that things are not so straightforward as they seem, since a given modification can leave a remote client in one of a number of states, not all of which are tolerable, let alone desirable. In this paper we attempt to delineate these states, and to consider ways of avoiding the worst of them. We describe our utility, which gives library developers a transparent version control system, ensuring that their remote clients won't break their applications.

Changing Java Programs

Back to top

Susan Eisenbach and Chris Sadler
.PDF

@inproceedings{ changingjava-icsm01,
 author    = {S. Eisenbach and C. Sadler},
 title     = {Changing {J}ava {P}rograms},
 booktitle = {IEEE Conference in Software Maintenance (ICSM 2001)},
 year      = {2001},
 month     = {November},
 address   = {Florence, Italy},
 url       = {http://www.dsi.unifi.it/icsm2001/}
}

The promises of object-orientation and distributed computing could be delivered if the software we needed were written in stone. But it isn't, it changes. The challenge of distributed object-oriented maintenance is to find a means of evolving software, which already has a distributed client base.

Working within this scenario, we observe how certain object-oriented language systems seek to support differing client requirements and service obligations. In particular, we examine how the Java Language Specification (JLS) facilitates the concept of binary compatibility, a useful property, but one that may introduce a class of clients who dare not re-compile! Following a suggestion in the new draft JLS, we describe our tool to manage distributed version control and we formulate some proposals for future developments.

Ephemeral Java Source Code

Back to top

Susan Eisenbach and Chris Sadler
.PDF .PS

@inproceedings{ ephemeral-ftdcs99,
 author    = {S. Eisenbach and C. Sadler},
 title     = {Ephemeral {J}ava {S}ource {C}ode},
 booktitle = {7th IEEE Workshop on Future Trends in Distributed Computing Systems},
 year      = {1999}
 month     = {December},
 address   = {Cape Town, South Africa}
}

In an object oriented, distributed environment, program maintenance, which has never been the most predictable task, becomes even more uncertain. Java's dynamic loading mechanism was developed to tackle some of the uncertainties. In doing so, it shifts the focus from the state of the sources to that of the binaries. This paper discusses some of the implications of that move.

Refined Effects for Unanticipated Object Re-classification: Fickle3 (Extended Abstract)

Back to top

Ferruccio Damiani, Sophia Drossopoulou and Paola Giannini
.PDF

@inproceedings{fickle3-ictcs03,
 author    = {F. Damiani and S. Drossopoulou and P. Giannini},
 title     = {Refined {E}ffects for {U}nanticipated {O}bject {R}e-classification: {F}ickle3 ({E}xtended {A}bstract)},
 booktitle = {Theoretical Computer Science: 8th Italian Conference (ICTCS'03}},
 year      = {2003},
 month     = {October},
 series    = {LNCS},
 volume    = {2841},
 pages     = {97--110},
 publisher = {Springer-Verlag}
}

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.

In 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.

The 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.

More Dynamic Object Re-classification: FickleII

Back to top

Sophia Drossopoulou, Ferruccio Damiani, Mariangiola Dezani-Ciancaglini and Paola Giannini
.PS

@article{ fickleii-toplas02,
 author    = {S. Drossopoulou and F. Damiani and M. Dezani-Ciancaglini and P. Giannini},
 title     = {More {D}ynamic {O}bject {R}e-classification: {FickleII}},
 journal   = {ACM Transactions On Programming Languages and Systems},
 year      = {2002},
 volume    = {24},
 number    = {2},
 pages     = {153--191}
}

Re-classification changes the class membership of an object at run-time while retaining its identity. We suggest language features for object re-classification,which could extend an imperative, typed, class-based, object-oriented language.

We present our proposal through the language FickleII. The imperative features combined with the requirement for a static and safe type system provided the main challenges. We develop a type and effect system for FickleII and prove its soundness with respect to the operational semantics. In particular, even though objects may be re-classified across classes with different members, they will never attempt to access non-existing members.

A type preserving translation of Fickle into Java

Back to top

Davide Ancona, Christopher Anderson, Ferruccio Damiani, Sophia Drossopoulou, Paola Giannini and Elena Zucca
.PS

@inproceedings{ficklejava-tosca01,
 author    = {D. Ancona and C. Anderson and F. Damiani and S. Drossopoulou and P. Giannini and E. Zucca},
 title     = {A type preserving translation of {F}ickle into {J}ava},
 booktitle = {TOSCA'01},
 year      = {2002},
 series    = {ENTCS},
 volume    = {62},
 editor    = {Marina Lenisa and Marino Miculan},
 publisher = {Elsevier}
}

We present a translation from Fickle (a Java-like language allowing objects that can change their class at run-time) into plain Java. The translation, which maps any Fickle class into a Java class, is driven by an invariant that relates the Fickle object to its Java counterpart. The translation, which is proved to preserve both the static and the dynamic semantics of the language, is an enhanced version of a previous proposal by the same authors.

Fickle: Dynamic object re-classification

Back to top

Sophia Drossopoulou, Ferruccio Damiani, Mariangiola Dezani-Ciancaglini and Paola Giannini
.PS

@inproceedings{ fickle-ecoop01,
 author    = {S. Drossopoulou and F. Damiani and M. Dezani-Ciancaglini and P. Giannini},
 title     = {Fickle: {D}ynamic {O}bject {R}e-classification},
 booktitle = {15 European Conference on Object-Oriented Programming (ECOOP 2001)},
 year      = {2001},
 series    = {LNCS},
 volume    = {2072},
 pages     = {130--149},
 publisher = {Springer-Verlag}
}

Re-classification changes at run-time the class membership of an object while retaining its identity. We suggest language features for object re-classification,which could extend an imperative, typed, class-based, object-oriented language. We present our proposal through the language Fickle. (Fickle is the successor of an earlier proposal, Fickle-99; although both Fickle and Fickle-99 address the same requirement for object re-classification, the approaches are very different).

The imperative features combined with the requirement for a static and safe type system provided the main challenges. We develop a type and effect system for Fickle and prove its soundness with respect to the operational semantics. In particular, even though objects may be re-classified across classes with different members, they will never attempt to access non-existing members.

Inner Classes visit Aliasing

Back to top

Matthew Smith and Sophia Drossopoulou
.PS

@inproceedings{ innerclasses-ftfjp03,
 author    = {Matthew Smith and Sophia Drossopoulou},
 title     = {Inner {C}lasses visit {A}liasing},
 booktitle = {ECOOP Workshop on Formal Techniques for Java Programs (FTfJP 2003)},
 year      = {2003},
 url       = {http://www.cs.kun.nl/~erikpoll/ftfjp/2003.html}
}

Inner classes appear nested withing class definitions, and may access any members of the class ion which they are contained. The interplay between inner classes, aliasing and subclasses can make resolution of such accesses intricate. We offer a succinct model for member classes, in which we highlight these intricacies, and we prove soundness.

Overloading and Inheritance

Back to top

Davide Ancona, Sophia Drossopoulou and Elena Zucca
.PS

@inproceedings{ overloading-fool01,
 author    = {D. Ancona and S. Drossopoulou and E. Zucca},
 title     = {Overloading and {I}nheritance},
 booktitle = {Electronic proceedings of FOOL8 (http://www.cs.williams.edu/~kim/FOOL/)},
 year      = {2001}
}

Overloading allows several function definitions for the same name, distinguished primarily through different argument types; it is typically resolved at compile-time. Inheritance allows subclasses to define more special versions of the same function; it is typically resolved at run-time.

Modern object-oriented languages incorporate both features, usually in a type-safe manner. However, the combination of these features sometimes turns out to have surprising, and even counterintuitive, effects.

We discuss why we consider these effects inappropriate, and suggest alternatives. We explore the design space by isolating the main issues involved and analyzing their interplay and suggest a formal framework describing static overloading resolution and dynamic function selection, in a programming language, and their abstracting from other language features. We believe that our framework clarifies the thought process going on at language design level.

We introduce a notion of soundness and completeness of an overloading resolution policy w.r.t. the underlying dynamic semantics, and a way of comparing the flexibility of different resolution policies. We apply these concepts to some non-trivial issues raised in concrete languages.

We also argue that the semantics of overloading and inheritance is "clean" only if it can be understood through a copy semantics, whereby programs are transformed to equivalent programs without subclasses, and the effect of inheritance is obtained through copying.

Java Exceptions Throw No Surprises

Back to top

Sophia Drossopoulou and Tanya Valkevych
.PS

@misc{ nosurprises-00,
 author = {Sophia Drossopoulou and Tanya Valkevych},
 title  = {Java Exceptions Throw No Surprises},
 year   = {2000},
 month  = {March}
}

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.

The 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.

Java Type Soundness Revisited

Back to top

Sophia Drossopoulou, Tanya Valkevych, Susan Eisenbach
.PS

@misc{ revisited-00,
 author = {Sophia Drossopoulou and Tanya Valkevych and Susan Eisenbach},
 title  = {Java Type Soundness Revisited},
 year   = {2000},
 month  = {September}
}

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.

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.

With 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.

We 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.

Finally, 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.

Is the Java Type System Sound?

Back to top

Sophia Drossopoulou, Susan Eisenbach and Sarfraz Khurshid
.PS

@article{ sound-tapos99,
 author  = {Sophia Drossopoulou and Susan Eisenbach and Sarfraz Khurshid},
 title   = {Is the {J}ava {T}ype {S}ystem {S}ound?},
 journal = {Theory and Practice of Object Systems},
 year    = {1999},
 volume  = {5},
 number  = {1},
 pages   = {3--24},
 url     = {http://tokio.dbis.informatik.uni-frankfurt.de/~taposadm/}
}

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.

A Fragment Calculus - towards a Model of Separate Compilation, Linking and Binary Compatibility

Back to top

Sophia Drossopoulou, Susan Eisenbach and David Wragg
.PS

@inproceedings{ fragment-lics99,
 author    = {Sophia Drossopoulou and Susan Eisenbach and David Wragg},
 title     = {A {F}ragment {C}alculus - towards a {M}odel of {S}eparate {C}ompilation, {L}inking and {B}inary {C}ompatibility},
 booktitle = {14th Symposium on Logic in Computer Science (LICS'99)},
 year      = {1999},
 month     = {July},
 pages     = {147--156},
 publisher = {IEEE}
}

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 re-compilation 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.

A note from Gilad Bracha which influenced the paper (and appears as citation [2]) can be found here.

What is Java Binary Compatibility?

Back to top

Sophia Drossopoulou and David Wragg and Susan Eisenbach
.PS

@inproceedings{ binarycompatibility-oopsla98,
 author    = {Sophia Drossopoulou and David Wragg and Susan Eisenbach},
 title     = {What is {J}ava {B}inary {C}ompatibility?},
 booktitle = {Proceedings of the 13th ACM SIGPLAN conference on Object-oriented programming, systems, languages, and applications (OOPSLA'98)},
 year      = {1998},
 pages     = {341--361},
 publisher = {ACM Press}
}

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.

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) 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.

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, 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.

Towards an Operational Semantics and Proof of Type Soundness for Java

Back to top

Sophia Drossopoulou and Susan Eisenbach
.PS

@inbook{ towards-98,
 author    = {S. Drossopoulou and S. Eisenbach},
 title     = {Towards an {O}perational {S}emantics and {P}roof of {T}ype {S}oundness for {J}ava},
 year      = {1998},
 month     = {March},
 publisher = {Springer-Verlag},
 url       = {citeseer.nj.nec.com/drossopoulou98towards.html}
}

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.

We 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

Java is Type Safe - Probably

Back to top

Sophia Drossopoulou and Susan Eisenbach
.PS

@inproceedings{ probably-ecoop97,
 author    = {Sophia Drossopoulou and Susan Eisenbach},
 title     = {Java is {T}ype {S}afe --- {P}robably},
 booktitle = {11th European Conference on Object Oriented Programming (ECOOP 1997)},
 year      = {1997},
 month     = {June},
 series    = {LNCS},
 volume    = {1241},
 pages     = {389--418},
 publisher = {Springer-Verlag}
}

Amidst rocketing numbers of enthusiastic Java programmers and internet applet users, there is growing concern about the security of executing Java code produced by external, unknown sources. Rather than waiting to find out empirically what damage Java programs do, we aim to examine first the language and then the environment looking for points of weakness. 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 type safe subset of Java describing primitive types, classes, inheritance, instance variables and methods, interfaces, shadowing, dynamic method binding, object creation, null and arrays. We argue that for this subset the type system is sound, by proving that program execution preserves the types, up to subclasses/subinterfaces.

A Distributed Abstract Machine for Boxed Ambient Calculi

Back to top

Andrew Phillips, Nobuko Yoshida and Susan Eisenbach
.PS

@inproceedings{ abstractmachine-esop04,
 author    = {A. Phillips and N. Yoshida and S. Eisenbach},
 title     = {A Distributed Abstract Machine for Boxed Ambient Calculi},
 booktitle = {Proceedings of the European Symposium on Programming (ESOP 2004)},
 year      = {2004},
 month     = {April},
 address   = {Barcelona, Spain},
 series    = {LNCS},
 publisher = {Springer-Verlag}
}

Boxed ambient calculi have been used to model and reason about a wide variety of problems in mobile computing. Recently, several new variants of Boxed Ambients have been proposed, which seek to improve on the original calculus. In spite of these theoretical advances, there has been little research on how such calculi can be correctly implemented in a distributed environment. This paper bridges a gap between theory and implementation by defining a distributed abstract machine for a variant of Boxed Ambients with channels. The abstract machine uses a list semantics, which is close to an implementation language, and a blocking semantics, which leads to an efficient implementation. The machine is proved sound and complete with respect to the underlying calculus. A prototype implementation is also described, together with an application for tracking the location of migrating ambients. The correctness of the machine ensures that the work done in specifying and analysing mobile applications is not lost during their implementation.

From Process Algebra to Java Code

Back to top

Andrew Phillips, Susan Eisenbach and Daniel Lister
.PDF

@inproceedings{ algebra-ftfjp02,
 author    = {A. Phillips and S. Eisenbach and D. Lister},
 title     = {From Process Algebra to Java Code},
 booktitle = {ECOOP Workshop on Formal Techniques for Java-like Programs (FTfJP 2002)},
 year      = {2002},
 month     = {June},
 address   = {Málaga, Spain},
 publisher = {http://www.cs.kun.nl/~erikpoll/ftfjp/2002.html}
}

The delta-pi-calculus, a calculus based on the pi-calculus, is a model for mobile distributed computation. The delta-pi-calculus can be used to specify applications, in order to reason about their security and correctness properties. The delta-pi primitives have been implemented as a Java API. The implementation in Java provides a means of bridging the gap between application specification and implementation.

Formal Models for Aspect-Oriented Software Development

Back to top

Mark Skipper
.PDF

@phdthesis{ skipper-phd03,
 author = {Mark Charles Skipper},
 title  = {Formal Models for Aspect-Oriented Software Development},
 school = {Department of Computing, Imperial College London},
 year   = {2003},
 month  = {December}
}

This thesis is a study of the semantics of the novel features of AspectJ. It presents a formal model of a simple Java-like language with a type system and an operational semantics, then goes on to extend it with the most paradigmatic featutes of AspectJ: Formal definitions of joinpoints, advice and aspects are presented for the first time, in the context of an operational semantics. A formal defintion of weaving is developed. the impact of these features on the type system is investigated. Examples are used to demonstrate their expressiveness. The increments to the semantics of the base language are relatively small for each feature, making the presentation simple to understand. The work is suitable as a base for further investigation of aspect oriented language features using formal techniques.

LEXIS: An Exam Invigilation System

Back to top

Mike Wyer and Susan Eisenbach
.PDF

@inproceedings{ lexis-lisa01,
 author    = {M. Wyer and S. Eisenbach},
 title     = {{LEXIS}: {A}n {E}xam {I}nvigilation {S}ystem},
 booktitle = {LISA 2001 Conference},
 year      = {2001},
 month     = {December},
 address   = {San Diego, California, USA},
 note      = {Best Practical Paper Award}
}

Over recent years, computers have been making their way into the classroom and lecture theatre. Overhead projectors, blackboards, and whiteboards have been joined or even displaced by smartboards and computer based multimedia presentations. Students with laptops are a common sight, and courses have their lecture notes on the web. Students are taking courses in programming, web-site design, computer graphics, and many other digital disciplines. Yet these courses are still being assessed with traditional pen and paper examinations.

The reasons for this are several including inertia, worries about security, and a lack of available tools to administer high-security exams with confidence.

At the request of the Academic Committee of the Imperial College Computing Department, we were asked to develop such a tool so that our students could sit an official examination using the Linux workstations in our teaching laboratories.

We embarked on a project to develop a system to provide necessary resources to candidates, prevent cheating, and securely retrieve and store the work done by the candidates during the exam. Here we describe the technologies, problems, and solutions encountered during the development of software to support exam invigilation.

The result of this work is the Lexis EXam Invigilation System, which was used to administer a first year programming exam on 21st March 2001 which comprised 110 students with access to 160 Linux workstations and lasted for three hours. At the end of which, the labs were restored to general access use. According to the BBC, on the 2nd of April 2001, students sat the first paperless exam in the UK in a pilot scheme in Northern Ireland. In fact, we beat them to it by several weeks.