Program Repair as Sound Optimization of Broken Programs
(0) We present a new, semantics-based approach to me chanical program repair where the intended meaning of broken programs (i.e., programs that may abort under a given, error-admitting language semantics) can be defined by a special, error-compensating semantics. Program re pair can then become a compile-time, mechanical program transformation based on a program analysis. It turns a given program into one whose evaluations under the error admitting semantics agree with those of the given program under the error-compensating semantics. We present the analysis and transformation as a type system with a trans formation component, following the type-systematic ap proach to program optimization from our earlier work. The type-systematic method allows for simple soundness proofs of the repairs, based on a relational interpretation of the type system, as well as mechanical transformability of program correctness proofs between the Hoare logics for the error-compensating and error-admitting semantics. We first demonstrate our approach on the repair of file handling programs with missing or superfluous open and close statements. Our framework shows that this repair is strikingly similar to partial redundancy elimination op timization commonly used by compilers. In a second ex ample, we demonstrate the repair of programs operating a queue that can over-and underflow, including mechanical transformation of program correctness proofs.
program repair type systems similarity relations program optimization soundness program logics mechanical transformation of program correctness proofs
Bernd Fischer Ando Saabas Tarmo Uustalu
School of Electronics and Computer Science University of Southampton Southampton, SO17 1BJ, United K Institute of Cybernetics Tallinn University of Technology Akadeemia tee 21, EE- 12618 Tallinn, Eston
国际会议
天津
英文
165-173
2009-07-29（万方平台首次上网日期，不代表论文的发表时间）