9803843 This project investigates formal methods for programming object- oriented (OO) software components. The goals are to produce: (a) theoretical foundations to support careful reasoning about such components, and (b) expressive behavioral interface specification languages (BISLs) that are able to substitute for the source code of such components. Foundational issues for goal (a) include the model theory and proof theory of abstract data types with mutable objects, subtyping, aliasing, and message passing. The model theory of our previous work is extended to account for nondeterminism and higher-order procedures. In proof theory, equational reasoning techniques for reasoning about immutable objects are sought. These results are to be connected with verification logics for OO languages with the new feature of multimethods. Goal (b) helps vendors explain OO class libraries and frameworks to customers without giving them source code, which cannot be done with existing BISLs. This project provides: guidance for the design of more expressive OO specification languages, ideas for use in documentation of OO class libraries and frameworks, and expressive notations for specification. Software engineers will also benefit from more expressive BISLs and the ideas about reasoning.***
