The Proof of the SIFT Implementation

Abstract

The Software Implemented Fault Tolerance SIFT specifications consist primarily of constraints on the schedule table and descriptions of the changes each routine makes to the global variables. The proof proceeds by proving that each routine is consistent with its specification. Each of these proofs is separate from the others and the order of the proofs is unimportant. A routine is proved by generating a set of verification conditions from the PASCAL code and the SPECIAL specifications. Each verification condition is a set of assertions derived from a particular path in the routine. A verification condition (VC) is generated for each possible path through the routine.