BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Talks.cam//talks.cam.ac.uk//
X-WR-CALNAME:Talks.cam
BEGIN:VEVENT
SUMMARY:Specification\, Implementation and Verification of Refactorings - 
 Max Schaefer (Oxford Computing Lab)
DTSTART:20110120T151500Z
DTEND:20110120T161500Z
UID:TALK28588@talks.cam.ac.uk
CONTACT:Dominic Orchard
DESCRIPTION:Refactoring is the process of restructuring programs by means 
 of behaviour-preserving program transformations\, themselves called refact
 orings. Most modern development environments come with built-in support fo
 r automated refactorings that the user can perform at the push of a button
 . Implementing refactorings is notoriously complex\, however\, and even st
 ate-of-the-art implementations have very low standards of correctness.\n\n
 We give an overview of our recent work on developing concepts and techniqu
 es that make it possible to give concise and modular specifications of ref
 actorings. Our approach is based on static semantic dependencies\, which e
 xpress program properties to be preserved by the refactoring\; decompositi
 on of large refactorings into smaller microrefactorings\, which can be dev
 eloped and reused independently\; and language restrictions and extensions
 \, which abstract from the complexities of the object language.\n\nThe spe
 cifications we obtain are precise enough to cover all details of the objec
 t language\, and thus give rise to full featured\, high-quality refactorin
 g implementations. Their modularity\, on the other hand\, makes them amena
 ble to formal proof\, and hence opens the door to the rigorous verificatio
 n of refactorings.\n
LOCATION:GS15\, Computer Laboratory
END:VEVENT
END:VCALENDAR