SELF-CHECKING PROGRAMS: AN AXIOMATIC APPROACH TO THE VALIDATION OF PROGRAMS BY THE USE OF ASSERTIONS

The subject of this thesis is the development and investigation of a Methodology for program design and verification. The design part is described by a step-wise refinement process. The verification part is described by a set of Induction Rules. The distinguishing feature of this methodology is that it produces programs which are not proven to be correct but to have a property that is weaker than correctness: The Self-Checking Property.;An example of design and verification of a self-checking program performing Gaussian elimination is shown. It is stressed that very little effort is needed for the verification of its self-checking property.;The self-checking Property is based on a systematic use of assertions and is defined as follows: A program is said to be self-checking if and only if we can prove that any time it is executed on some input data and all assertions return True when they are checked for, then the output obtained is correct.