Relative correctness: A bridge between testing and proving

Nafi Diallo, Wided Ghardallou, Ali Mili

Research output: Contribution to journalConference articlepeer-review

1 Scopus citations

Abstract

Relative correctness is the property of a program to be more- correct than another with respect to a specification. Whereas tradition-Ally we distinguish between two categories of candidate programs, namely correct programs and incorrect programs, relative correctness arranges candidate programs on a partial ordering structure, whose maximal elements are the correct programs. Also, whereas traditionally we deploy proof methods on correct programs to prove their correctness and we de- ploy testing methods on incorrect programs to detect and remove their faults, relative correctness enables us to bridge this gap by showing that we can deploy static analytical methods to an incorrect program to prove that while it may be incorrect, it is still more-correct than another. We are evolving a technique, called debugging without testing, in which we can remove a fault from a program and prove that the new program is more-correct than the original, all without any testing (and its associated uncertainties/ imperfections). Given that there are orders of magnitude more incorrect programs than correct programs in use nowadays, this has the potential to expand the scope of proving methods significantly. Also, relative correctness has other broad implications for testing and proving, which we briefly explore in this paper.

Original languageEnglish (US)
Pages (from-to)141-156
Number of pages16
JournalCEUR Workshop Proceedings
Volume1689
StatePublished - 2016
Event10th Workshop on Verification and Evaluation of Computer and Communication System, VECoS 2016 - Tunis, Tunisia
Duration: Oct 6 2016Oct 7 2016

All Science Journal Classification (ASJC) codes

  • Computer Science(all)

Keywords

  • Absolute correctness
  • Debugging without testing
  • Program proving
  • Program testing
  • Programming without refining
  • Relative correctness
  • Testing for relative correctness

Fingerprint

Dive into the research topics of 'Relative correctness: A bridge between testing and proving'. Together they form a unique fingerprint.

Cite this