Formal Methods for Extensible Object-Oriented Software

Iowa State University, Ames IA

Investigators

Abstract

This project advances the theory and practice of extensible object-oriented (OO) software by investigating how to support careful design, specification, and reasoning. Enhancing theoretical understanding for specifying and verifying extensible OO software forms the first subproblem. The project investigates several avenues: the soundness of proof techniques for behavioral subtyping among abstract data types with mutable objects, whose operations may have nondeterministic specifications; the extent to which the use of multimethods affects one's ability to prove behavioral subtyping; and the soundness of a specification and verification technique that allows the implementation of a subclass from a superclass's specification, without seeing the superclass's code. The second subproblem comprises enhancing Java and a specification language for Java to better support extensible OO frameworks and libraries. The project implements and refines MultiJava, an extension to Java that supports both open classes and multimethods. The former allow one to extend existing classes with new methods, while the latter allow one to easily extend both a set of data types and the methods that work on them. The project also extends and refines JML, which is a behavioral interface specification language tailored to Java.