This project has received an honorable mention in the evaluation of CNPq (in Portuguese)
Object-oriented programming languages have been widely adopted in
industry because they offer the promise of reusable software components. Languages such as
Java and C++ offer dynamic binding and a flexible system of type-checking, which makes it
possible for a component to be reused in many contexts. In practice, however, the full
potential of reuse is difficult to achieve because dynamic binding allows a component to
have a complicated interaction with the context in which it is used. It is difficult to
gain sufficient understanding of such contexts to reason convincingly about a component in
isolation. It also difficult todesign interfaces so that, in a particular context, a
component's behavior can be understood as a black box, without reference to its
Such modular reasoning is essential for fulfillment ofthe promise of reusability.
Mathematical formalization is an essential foundation for methods of specification and development of software. Practical engineering involves a judicious combination of informal reasoning, rigorous analysis, and automated tools. Formalization explains and justifies informal methods as well as being the basis for rigorous methods and tools. There has been considerable progress in the design of languages and in formalization of specification methods. Nevertheless, for development methods, formalization lags behind both the language features and the informal methods. Formalization of modular reasoning is both important and challenging.
This research project is an effort to devise improved methods for reasoning about programs in widely used languages like Java and C++. Feasible improvements in software development are sought --- ones that fit with conventional practices in requirements specification and reasoning.
The project will produce a calculus for development of object-oriented programs. The calculus will include laws for program derivation and optimization as well as object-oriented class design and class restructuring. A major case study will be formulation of laws for compilation by meansof correctness-preserving transformation.