Centro de Informática
Universidade Federal de Pernambuco       
Lines - Languages and Software Engineering Group

logodi.gif (5809 bytes)


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 internals. 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.