Invited Talks

Oscar Nierstrasz: Object-oriented Reengineering Patterns

ABSTRACT Surprising as it may seem, many of the early adopters of object-oriented languages already face a number of problems typically encountered in large-scale legacy systems. Software engineers are now confronted with millions of lines of industrial source code, developed using object-oriented design methods and languages of the late 80s and early 90s. These systems exhibit a range of problems, effectively preventing them from satisfying the evolving requirements imposed by their customers. This talk will present a survey of various techniques that have been successfully used to re-engineer industrial OO systems. In particular, we will discuss issues like reverse engineering, design extraction, metrics, refactoring and program visualisation.

Oege de Moor: The AspectBench Compiler for AspectJ

ABSTRACT Aspects provide a highly disciplined form of program generation; rather than generating or transforming program syntax, they transform program behaviours by intercepting events. This basis makes aspect-oriented programming less error-prone than general meta-programming.

While the merits of aspects are generally accepted, the design space for aspect-oriented programming languages is not yet well understood. What are the events that can be intercepted? What are appropriate patterns for describing such events? Do aspects admit modular reasoning? What are appropriate features for aspects to add members to existing classes? How are aspects composed? What are the overheads of using aspects? I shall outline a programme of research that begins to address these questions.

As part of that research programme, we have developed abc: an extensible, optimising compiler for AspectJ. abc is intended as a workbench to experiment with answers to the above questions. I will explain how this goal translates into an architecture for abc, and I shall summarise how abc has been used, both by ourselves and by others.

Bernd Fischer: Certifiable Program Generation

ABSTRACT Code generators based on template expansion techniques are easier to build than purely deductive systems but do not guarantee the same level of assurance: instead of providing correctness-by-construction, the correctness of the generated code depends on the correctness of the generator itself. We present an alternative assurance approach, in which the generator is extended to enable Hoare-style safety proofs for each individual generated program. The proofs ensure that the generated code does not go wrong, i.e., does not violate certain conditions during its execution.

The crucial step in this approach is to extend the generator in such way that it produces all required annotations (i.e., pre-/postconditions and loop invariants) without compromising the assurance provided by the subsequent verification phase. This is achieved by embedding annotation templates into the code templates, which are then instantiated in parallel by the generator. This is feasible because the structure of the generated code and the possible safety properties are known when the generator is developed. It does not compromise the provided assurance because the annotations only serve as auxiliary lemmas and errors in the annotation templates ultimately lead to unprovable safety obligations.

We have implemented this approach and integrated it into the AutoBayes and AutoFilter program generators. We have then used it to fully automatically prove that code generated by the two systems satisfies both language-specific properties such as array-bounds safety or proper variable initialization-before-use and domain-specific properties such as vector normalization, matrix symmetry, or correct sensor input usage.