Program repair as sound optimization of broken programs

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 [12]. 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