What is Formal Verification-Proof of Correctness
A proof of correctness is a mathematical proof that a computer program or a part thereof will, when executed, yield correct results i.e., results fulfilling specific requirements. Before proving a program correct, the theorem to be proved must, of course, be formulated.
Hypothesis: The hypothesis of such a correctness theorem is typically a condition that the relevant program variables must satisfy immediately “before” the program is executed. This condition is called the “precondition”.
Thesis: The thesis of the correctness theorem is typically a condition that the relevant program variables must satisfy immediately “after” execution of the program. This latter condition is called the ‘post-condition’.
Thus
the correctness theorem can be stated as:
“If the condition, “V”, is true before execution of the program, “S”, then the condition, “P”, will be true after execution of “S” “.
Where “V” is pre-condition and “P” is post-condition.
Notation:Such a correctness theorem is usually written as {V} S {P}, where V, S and P have been explained above.
By “program variable” we broadly include input and output data, e.g., data entered via a keyboard, displayed on a screen or printed on paper. Any externally observable aspect of the program’s execution may be covered by the precondition and post-condition.
Many More Articles on Verification & Validation
An expert on R&D, Online Training and Publishing. He is M.Tech. (Honours) and is a part of the STG team since inception.