Correctness and Relative Correctness

Nafi Diallo, Wided Ghardallou, Ali Mili

Research output: Chapter in Book/Report/Conference proceedingConference contribution

6 Scopus citations

Abstract

In the process of trying to define what is a software fault, we have foundthat to formally define software faults we need to introduce the conceptof relative correctness, i.e. the property of a program to be more-correctthan another with respect to a given specification. A feature of a programis a fault (for a given specification)only because there exists an alternative to it that would makethe program more-correct with respect to the specification.In this paper, we explore applications of the concept of relative correctness in programtesting, program repair, and program design.Specifically, we argue that in many situations of software testing,fault removal and program repair, testing for relative correctnessrather than absolute correctness leads to clearer conclusions andbetter outcomes. Also, we find that designing programs by stepwisecorrectness-enhancing transformations rather than by stepwise correctness-preserving refinements leads to simpler programs and is more tolerant of designer mistakes.

Original languageEnglish (US)
Title of host publicationProceedings - 2015 IEEE/ACM 37th IEEE International Conference on Software Engineering, ICSE 2015
PublisherIEEE Computer Society
Pages591-594
Number of pages4
ISBN (Electronic)9781479919345
DOIs
StatePublished - Aug 12 2015
Event37th IEEE/ACM International Conference on Software Engineering, ICSE 2015 - Florence, Italy
Duration: May 16 2015May 24 2015

Publication series

NameProceedings - International Conference on Software Engineering
Volume2
ISSN (Print)0270-5257

Other

Other37th IEEE/ACM International Conference on Software Engineering, ICSE 2015
Country/TerritoryItaly
CityFlorence
Period5/16/155/24/15

All Science Journal Classification (ASJC) codes

  • Software

Fingerprint

Dive into the research topics of 'Correctness and Relative Correctness'. Together they form a unique fingerprint.

Cite this