DARE-COOP – Development and Applications of a Refinement Calculus for Object-Oriented Programming | Concluded in 2005

The main goal of this project is to consolidate a refinement calculus for object-oriented languages such as Java, taking into account previous works, such as Morgan’s refinement calculus.

The proposed calculus should include basic algebraic rules for program transformation, as well as high-level rules that systematise the state-of-the-practice of object-oriented designs. The rules should be proved considering the semantics (based on weakest precondition) of the given language. Some case studies and a compiler (based on rewriting rules) are going to be developed as an exercise of the application of the rules. In a previous project (CO-OP) the emphasis was on a language with copy semantics. Differently, in this project, we consider reference semantics, besides supporting more elaborate constructions such as abstract classes, interfaces and packages.