Centro
de Informática
Universidade Federal de Pernambuco
Lines - Languages and Software
Engineering Group
Centro
de Informática
|
|
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.