Skip to main content
placeholder image

Semi-proving: an integrated method for program proving, testing, and debugging

Journal Article


Abstract


  • We present an integrated method for program proving, testing, and debugging. Using the concept of metamorphic relations, we select necessary properties for target programs. For programs where global symbolic evaluation can be conducted and the constraint expressions involved can be solved, we can either prove that these necessary conditions for program correctness are satisfied or identify all inputs that violate the conditions. For other programs, our method can be converted into a symbolic-testing approach. Our method extrapolates from the correctness of a program for tested inputs to the correctness of the program for related untested inputs. The method supports automatic debugging through the identification of constraint expressions that reveal failures.

Publication Date


  • 2011

Citation


  • Chen, T., Tse, T. H. & Zhou, Z. Quan. (2011). Semi-proving: an integrated method for program proving, testing, and debugging. IEEE Transactions on Software Engineering, 37 (1), 109-125.

Scopus Eid


  • 2-s2.0-79551537874

Ro Metadata Url


  • http://ro.uow.edu.au/infopapers/3547

Has Global Citation Frequency


Number Of Pages


  • 16

Start Page


  • 109

End Page


  • 125

Volume


  • 37

Issue


  • 1

Place Of Publication


  • Australia

Abstract


  • We present an integrated method for program proving, testing, and debugging. Using the concept of metamorphic relations, we select necessary properties for target programs. For programs where global symbolic evaluation can be conducted and the constraint expressions involved can be solved, we can either prove that these necessary conditions for program correctness are satisfied or identify all inputs that violate the conditions. For other programs, our method can be converted into a symbolic-testing approach. Our method extrapolates from the correctness of a program for tested inputs to the correctness of the program for related untested inputs. The method supports automatic debugging through the identification of constraint expressions that reveal failures.

Publication Date


  • 2011

Citation


  • Chen, T., Tse, T. H. & Zhou, Z. Quan. (2011). Semi-proving: an integrated method for program proving, testing, and debugging. IEEE Transactions on Software Engineering, 37 (1), 109-125.

Scopus Eid


  • 2-s2.0-79551537874

Ro Metadata Url


  • http://ro.uow.edu.au/infopapers/3547

Has Global Citation Frequency


Number Of Pages


  • 16

Start Page


  • 109

End Page


  • 125

Volume


  • 37

Issue


  • 1

Place Of Publication


  • Australia