Type Checker for VDM++

Thesis Title : Extending the VDM++ formal specification language with type inference and generic classes

Abstract

This thesis is divided into three phases. In the first phase, we convert a VDM-SL specification of a VDM++ static semantics checker to VDM++. Apart from the translation, we introduce a new architecture for the static semantics checker based on automatically generated AST visitors. The second phase is an study of the feasibility of extending OML with two new language feature, implicitly-typed functions and Java-style generic classes. Finally in the third phase, we provide a proof of concept of type-inference of implicitly-typed functions for a small subset of OML and a partial implementation of Generic classes.

Goals

• Phase 1 - Convert a subset of the original specification, written in VDM-SL, to an equivalent specification, written in VDM++.
• Phase 2 - Investigate, for a suitable subset of the VDM++ language the possibilities of adding two new language features to OML, Implicitly typed functions (with no function type annotations) and Parameterized classes in the style of Java Generics.
• Phase 3 - Implement an extended statics semantics checker for a subset of VDM++ as a proof of concept of Phase 2.

Results

Phase 1 - Conversion

The existing module-based architecture was re-designed to make use of the automatically generated AST-visitor classes generated by the Overture parser. A number of the old modules were combined into new structures based on visitors and a number of new visitors were added to support the type-inference experiments in late phases. Approximately 5100 lines of VDM-SL code were hand-converted into VDM++. Approximately 4500 lines of new code was added to support phases 2 and 3.

Phase 2 - Investigation

A theoretical investigation of type-inference and Generic classes pointed to Union types and Type invariants as potentially problematic areas with respect to type-inference.

Phase 3 - Implementation

Two new language features were added to the OML grammar, Generic Classes and Typeless Explicit Functions (TEF). A series of static checks were implemented for Generic classes. For TEF, a simple type-inference engine was implemented for a small subset of the language using a unification-based type-inference algorithm.

Future work

A type-checker for VDM++ / OML has already been specified by Peter Gorm Larsen. The existing type-checker is specified in VDM-SL. I have made a start on translating the VDM-SL specification to a VDM++ specification. An estimated 60% of the original type-checker has been hand-translated into VDM++ and adapted to the new AST visitor architecture.

What needs to be done on the type-checker alone ?

• The remaining 40% of the type-checker needs to be translated and adapted.
• The type-checker needs to be extensively tested using an existing test suite used to test the existing VDMTools type-checker.
• The type-checker needs to be code-generated to Java and integrated into the Overture Eclipse Plug in.

Where can someone pick up from where I have left off ?

The main focus of my thesis was to evaluate type-inference and generic classes as viable extensions to the OML. Of these two extensions, I believe that generic classes could be successfully implemented. Perhaps a new flavour of OML could be created that implemented this feature fully (Generic-OML) ? Type-inference could also be fun for someone to continue working with. In my thesis, I identified some areas of OML that might present some obstacles to adding full type-inference to OML. This does not mean that it could not work for a subset of the language. A topic for further investigation could be, defining this subset and any language restrictions necessary to allow type-inference.

Downloads

• ss_checker_code.zip: VDMTools Project files and VDM++ source files
• Thomas_Christensen_thesis.pdf: The thesis describing the project

Contact

If you have any questions regarding the project or source code, please feel free to contact ThomasChristensen.

-- ThomasChristensen - 30 Dec 2007