Collaborative Research: Formal Methods for Behavioral Subclassing and Callbacks

Project Details


Proposals 0429894/Naumann 0429567/Leavens

Collaborative Research:

Formal Methods for Behavioral Subclassing and Callbacks

David A. Naumann and Gary T. Leavens

For evolvability, scalability, and productivity, software systems must be composed of extensible components. Features of object-oriented programming languages such as inheritance and dynamic dispatch, and

techniques like callbacks and downcalls, are crucial but they invert the usual layering of abstractions. Aliasing among objects is crucial for efficiency but can breach encapsulation boundaries. Yet abstraction

and encapsulation are necessary to separately validate individual components.

This project will advance the theory of specification, development, and verification for object-oriented software, focusing on behavioral subclassing, alias confinement, and callbacks. Core features of the

Java Modeling Language (JML) for behavioral interface specification will be studied, using a confinement discipline to control aliasing and model programs to specify callbacks. The ideas will be presented

in a cogent, simple, and robust theory, to facilitate applications by tools, comparison between alternative proposals for specification notations and proof rules, and teaching. The theory will be encoded

in a theorem prover and key results machine-checked.

This project will provide theoretical guidance for the designers of programming and specification languages. The results will also help clarify and improve techniques used in practice.

Direct application is expected in projects based on JML and in work by our Brazilian collaborators.

Effective start/end date9/1/045/31/08


  • National Science Foundation: $161,995.00


Explore the research topics touched on by this project. These labels are generated based on the underlying awards/grants. Together they form a unique fingerprint.