Abstract Invariant relations are used to analyze while loops; while their primary application is to derive the function of a loop, they can also be used to derive loop invariants, weakest preconditions, strongest postconditions, sufficient conditions of correctness, necessary conditions of correctness, and termination conditions of loops. In this paper we present two generic invariant relations that capture the semantics of loops whose loop body applies affine transformations on numeric variables.

It is so inconceivable to debug a program without testing it that these two words are used nearly interchangeably. Yet we argue that using the concept of relative correctness we can indeed remove a fault from a program and prove that the fault has been removed, by proving that the new program is more correct than the original. This is a departure from the traditional roles of proving and testing methods, whereby static proof methods are applied to a correct program to prove its correctness, and dynamic testing methods are applied to an incorrect program to expose its faults.

Relative correctness is the property of a program to be more-correct than another with respect to a specification; this property enables us to rank candidate programs in a partial ordering structure whose maximal elements are the correct programs.Whereas traditionally we think of program derivation as a process of successive correctnesspreserving transformations (using refinement) starting from the specification, we argue that it is possible to derive programs by successive correctness-enhancing transformations (using relative correctness) starting from abort.One of the attributes of our approach is that it captures in the same mathematical model, not only the derivation of programs from scratch, but also most (if not all) of the activities that arise in software evolution.Given that most software is developed nowadays by evolving existing products rather than from scratch, any advance in the technology of program transformation by correctness enhancement stands to yield significant practical benefits.

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.

Proving program termination plays an important role in ensuring reliability of software systems. Many researchers have lent much attention to this open long-standing problem, most of them were interested in proving that iterative programs terminate under a given input. In this paper, we present a method to solve a more interesting and challenging problem, namely, the generation of the termination condition of while loops i.e. condition over initial states under which a loop terminates normally. To this effect, we use a concept introduced by Mili et al., viz. invariant relation.

In this short paper we discuss the design, implementation and operation of an automated tool that computes the function of while loops written in C-like programming languages.