TY - GEN
T1 - A generic algorithm for program repair
AU - Khaireddine, Besma
AU - Zakharchenko, Aleksandr
AU - Mili, Ali
N1 - Publisher Copyright:
© 2017 IEEE.
PY - 2017/7/3
Y1 - 2017/7/3
N2 - Relative correctness is the property of a program to be more-correct than another with respect to a specification, whereas traditional (absolute) correctness distinguishes between two classes of candidate programs with respect to a specification (correct and incorrect), relative correctness defines a partial ordering between candidate programs, whose maximal elements are the (absolutely) correct programs. In this paper we argue that relative correctness ought to be an integral part of the study of program repair, as it plays for program repair the role that absolute correctness plays for program construction: in the same way that absolute correctness is the criterion by which we judge the process of deriving a program P from a specification R, we argue that relative correctness ought to be the criterion by which we judge the process of repairing a program P to produce a program P' that is more-correct than P with respect to R. In this paper we build on this premise to design a generic program repair algorithm, which proceeds by successive increases of relative correctness until we achieve absolute correctness. We further argue that in the same way that correctness ideas were used, a few decades ago, as a basis for correct-by-design programming, relative correctness ideas may be used, in time, as a basis for more-correct-by-design program repair.
AB - Relative correctness is the property of a program to be more-correct than another with respect to a specification, whereas traditional (absolute) correctness distinguishes between two classes of candidate programs with respect to a specification (correct and incorrect), relative correctness defines a partial ordering between candidate programs, whose maximal elements are the (absolutely) correct programs. In this paper we argue that relative correctness ought to be an integral part of the study of program repair, as it plays for program repair the role that absolute correctness plays for program construction: in the same way that absolute correctness is the criterion by which we judge the process of deriving a program P from a specification R, we argue that relative correctness ought to be the criterion by which we judge the process of repairing a program P to produce a program P' that is more-correct than P with respect to R. In this paper we build on this premise to design a generic program repair algorithm, which proceeds by successive increases of relative correctness until we achieve absolute correctness. We further argue that in the same way that correctness ideas were used, a few decades ago, as a basis for correct-by-design programming, relative correctness ideas may be used, in time, as a basis for more-correct-by-design program repair.
KW - Absolute correctness
KW - Elementary fault removal
KW - Oracle design
KW - Program repair
KW - Relative correctness
KW - Siemens benchmark
UR - http://www.scopus.com/inward/record.url?scp=85027465678&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=85027465678&partnerID=8YFLogxK
U2 - 10.1109/FormaliSE.2017.7
DO - 10.1109/FormaliSE.2017.7
M3 - Conference contribution
AN - SCOPUS:85027465678
T3 - Proceedings - 2017 IEEE/ACM 5th International FME Workshop on Formal Methods in Software Engineering, FormaliSE 2017
SP - 65
EP - 71
BT - Proceedings - 2017 IEEE/ACM 5th International FME Workshop on Formal Methods in Software Engineering, FormaliSE 2017
PB - Institute of Electrical and Electronics Engineers Inc.
T2 - 5th IEEE/ACM International FME Workshop on Formal Methods in Software Engineering, FormaliSE 2017
Y2 - 27 May 2017
ER -