$11.2 ABOUT SOFTWARE CORRECTNESS 333 11.2 ABOUT SOFTWARE CORRECTNESS We should first ask ourselves what it means for a software element to be correct.The observations and deductions that will help answer this question will seem rather trivial at first;but let us not forget the comment (made once by a very famous scientist)that scientific reasoning is nothing but the result of starting from ordinary observations and continuing with simple deductions-only very patiently and stubbornly. Assume someone comes to you with a 300,000-line C program and asks you"Is this program correct?".There is not much you can answer.(Ifyou are a consultant,though,try answering"no"and charging a high fee.You might just be right.) To consider the question meaningful,you would need to get not only the program but also a precise description of what it is supposed to do-a specification. The same comment is applicable,of course,regardless of the size of a program.The instructionx=y+/is neither correct nor incorrect;these notions only make sense with respect to a statement of what one expects from the instruction-what effect it is intended to have on the state of the program variables.The instruction is correct for the specification "Make sure that x and y have different values" but it is incorrect vis-a-vis the specification “Make sure that x has a negative value” (since,assuming that the entities involved are integers,x may end up being non-negative after the assignment,depending on the value of y). These examples illustrate the property that must serve as the starting point of any discussion of correctness: Software Correctness property Correctness is a relative notion. A software system or software element is neither correct nor incorrect per se;it is correct or incorrect with respect to a certain specification.Strictly speaking,we should not discuss whether software elements are correct,but whether they are consistent with their specifications.This discussion will continue to use the well-accepted term "correctness", but we should always remember that the question of correctness does not apply to software elements;it applies to pairs made of a software element and a specification.§11.2 ABOUT SOFTWARE CORRECTNESS 333 11.2 ABOUT SOFTWARE CORRECTNESS We should first ask ourselves what it means for a software element to be correct. The observations and deductions that will help answer this question will seem rather trivial at first; but let us not forget the comment (made once by a very famous scientist) that scientific reasoning is nothing but the result of starting from ordinary observations and continuing with simple deductions — only very patiently and stubbornly. Assume someone comes to you with a 300,000-line C program and asks you “Is this program correct?”. There is not much you can answer. (If you are a consultant, though, try answering “no” and charging a high fee. You might just be right.) To consider the question meaningful, you would need to get not only the program but also a precise description of what it is supposed to do — a specification. The same comment is applicable, of course, regardless of the size of a program. The instruction x := y + 1 is neither correct nor incorrect; these notions only make sense with respect to a statement of what one expects from the instruction — what effect it is intended to have on the state of the program variables. The instruction is correct for the specification “Make sure that x and y have different values” but it is incorrect vis-à-vis the specification “Make sure that x has a negative value” (since, assuming that the entities involved are integers, x may end up being non-negative after the assignment, depending on the value of y). These examples illustrate the property that must serve as the starting point of any discussion of correctness: A software system or software element is neither correct nor incorrect per se; it is correct or incorrect with respect to a certain specification. Strictly speaking, we should not discuss whether software elements are correct, but whether they are consistent with their specifications. This discussion will continue to use the well-accepted term “correctness”, but we should always remember that the question of correctness does not apply to software elements; it applies to pairs made of a software element and a specification. Software Correctness property Correctness is a relative notion