Specification, Implementation and Verification of Refactorings

Add to your list(s) Download to your calendar using vCal

• Max Schaefer (Oxford Computing Lab)
• Thursday 20 January 2011, 15:15-16:15
• GS15, Computer Laboratory.

If you have a question about this talk, please contact Dominic Orchard.

Note: Thursday not Friday.

Refactoring is the process of restructuring programs by means of behaviour-preserving program transformations, themselves called refactorings. Most modern development environments come with built-in support for automated refactorings that the user can perform at the push of a button. Implementing refactorings is notoriously complex, however, and even state-of-the-art implementations have very low standards of correctness.

We give an overview of our recent work on developing concepts and techniques that make it possible to give concise and modular specifications of refactorings. Our approach is based on static semantic dependencies, which express program properties to be preserved by the refactoring; decomposition of large refactorings into smaller microrefactorings, which can be developed and reused independently; and language restrictions and extensions, which abstract from the complexities of the object language.

The specifications we obtain are precise enough to cover all details of the object language, and thus give rise to full featured, high-quality refactoring implementations. Their modularity, on the other hand, makes them amenable to formal proof, and hence opens the door to the rigorous verification of refactorings.

This talk is part of the Computer Laboratory Programming Research Group Seminar series.

This talk is included in these lists:

• All Talks (aka the CURE list)
• Cambridge talks
• Computer Laboratory Programming Research Group Seminar
• Department of Computer Science and Technology talks and seminars
• GS15, Computer Laboratory
• Interested Talks
• School of Technology
• Trust & Technology Initiative - interesting events
• bld31

Note that ex-directory lists are not shown.