Projects for 2001/2002

Richard Paige

Note: I am joining the Department of Computer Science, University of York, in March 2001, though I won't be physically in England on a regular basis until July 2001 (it's complicated, and a little surreal, isn't it?). The best way to contact me between now and July is by email: We can arrange a phone conversation too.

RFP/1 - Extending a BON CASE Tool

(Suitable for CS/MEng PR4)

A CASE tool for drawing, manipulating, and storing object-oriented models in the BON modelling language has been constructed. BON, effectively, is equivalent to an Eiffel profile of UML, and supports modelling of static structure (e.g., via class diagrams that show classes, packages, interfaces, and relationships) and dynamic structure. The tool, implemented in Java/Swing using the GEF framework of the University of Southern California, currently supports static modelling (including interfaces), generates XML and JML code, and implements most of the BON metamodel. A number of projects are possible, related to studying, evaluating, extending, and improving the CASE tool:

A key challenge with these projects is understanding an existing, substantial system. Adding new features and functionality to the CASE tool should not be overly difficult, given the extendible nature of its design.


K. Walden and J.-M. Nerson, Seamless Object-Oriented Software Architecture, Prentice-Hall, 1995.

G. Booch, J. Rumbaugh, I. Jacobsen, The UML Reference Guide, Addison-Wesley, 1999.

The Argo/UML Tool documentation, available from (the BON CASE tool is constructed using the framework of Argo/UML)

G. Leavens et al. Preliminary Design of JML, Iowa State Technical Report, available from

RFP/2 - Object-Oriented Modelling in PVS

(Suitable for CS/MEng PR4)

The PVS system is an industrially applicable theorem prover and type checker based on higher order logic. It is strongly typed and provides semi-automatic support for reasoning. It has been successfully applied to a number of industrial verification tasks, e.g., microprocessor verification, software verification, compiler verification, etc. This project examines the use of the PVS specification language for object-oriented modelling. PVS provides no object-oriented constructs (e.g., classes, associations, objects, etc.) so the project will focus on designing an encoding of object-oriented models in PVS. In particular, the project can take two approaches:

Based on the mapping, a tool could be constructed (perhaps within the BON CASE tool framework discussed in RFP/1, above) to automate the generation of PVS theories from BON or UML models. The main challenge with this project is to devise the mapping from the modelling language into PVS. This is primarily a theoretical exercise; implementing a code generator for the translation should be mechanical. I forsee particular challenges in translating inheritance and method overriding into PVS. Thus, the theoretical aspects of this project offer more challenges than other projects that I offer. I do recommend that you have some experience with logic and functional programming if you choose to take up this project.

Readings: K. Walden and J.-M. Nerson, Seamless Object-Oriented Software Architecture, Prentice-Hall, 1995.

G. Booch, J. Rumbaugh, I. Jacobsen, The UML Reference Guide, Addison-Wesley, 1999.

S. Owre et al., The PVS Specification Language, CSL-SRI Technical Report, September 1999. Available from

RFP/3 - Redesigning a Compiler in Java

(Suitable for CS/MEng PR4)

A compiler (written in C) for a small imperative programming language is to be redesigned and rewritten in Java. The project involves two significant parts:

The compiler consists of several components: a lexical analyzer, a table-driven LL(1) parser, a symbol table, a type checker and scope controller, a code generator, and a small Virtual Machine. Each component may have to be redesigned and will have to be implemented in the chosen language. The C code for the compiler is about 10000 lines. There are a number of degrees of freedom with this project, for example:

I see this project as being of moderate difficulty, given the wealth of compiler-writing tools that are available. The second option, wherein the target language for the compiler is changed, is more challenging and will require experience with Java and an understanding of the Java VM.


- any Java reference book, e.g., the Java Programming Language from Sun.

- Aho, Sethi, Ullman: "Compilers: Principles, Techniques and Tools"

- Fischer and Leblanc: "Crafting a Compiler in C"

- Appel: "Modern Compiler Implementation in Java"

RFP/4 - Performance Analysis of Generics in Java, Eiffel, and C++

(Suitable for CS/MEng PR4)

Generic types (also known as templates) are a language facility that is available in C++ (in the form of templates, as in the STL) and Eiffel (in the form of generic classes), and, soon, Java (as offered by the proposal GJ). This project will involve quantitative comparison of the generic techniques offered in C++, Eiffel, and Java. In particular, the following generic techniques will be quantitatively compared:

Small programs will be written in each of the languages, using the generic techniques offered by the language. Time and space requirements for the programs will be gathered (e.g., using a profiler), and the languages compared, with the intent of discovering how each approach differs. In particular, analysis should look at memory footprint and how use of generics impacts on the time spent in garbage collection in Java and Eiffel (and, for example, in C++ instrumented with a collector like BDW).

A key challenge with this project is in identifying suitable benchmarks and in interpreting the results of the performance analysis.


- standard language references for C++, Eiffel, and Java (e.g., Stroustrup, Meyer, and Gosling)

- R. Jones, Garbage Collection, Wiley, 1996.

- web references for STL and Generic Java (see above and

RFP/5 - Expressing OCL in PVS

(Suitable for CS/MEng PR4)

The Object Constraint Language is part of standard UML. It is used for writing constraints that can be applied to models, for example:

Tool support is need for manipulating and reasoning about OCL constraints. This project will study the feasibility of using the PVS language for specifying OCL, and using the PVS theorem prover for reasoning about OCL constraints. The project will involve:

I expect this to be a challenging project. The semantics of OCL are unclear in many places, and there are likely many pitfalls in mapping it to a well-founded language like PVS. However, the potential for making a contribution to the UML development and to our understanding of OCL is great (this may lead to publishable work). I think the main challenge in this project will be in considering the alternatives for mapping OCL to PVS, and weighing the pros and cons of each.


J. Warmer and A. Kleppe, The Object Constraint Language, Addison-Wesley, 1999.

S. Owre et al, The PVS Specification Language, CSL SRI Technical Report, Sept 1999, available from

E.C.R. Hehner, A Practical Theory of Programming, Springer-Verlag, 1993.