A Verification Condition Generator for FORTRAN.

This paper provides both a precise specification of a subset of FORTRAN 66 and FORTRAN 77 and a specification of the verification condition generator we have implemented for that subset. Our subset includes all the statements in FORTRAN 66 except the following: READ, WRITE, REWIND, BACKSPACE, ENDFILE, FORMAT, EQUIVALENCE, DATA, and BLOCK DATA. We place some restrictions on the remaining statements; however, our subset includes certain uses of COMMON, adjustable array dimensions, function subprograms, subroutine subprograms with side effects, and computed and assigned GO TOs. Unusual features of our system include a syntax checker that enforces all our syntactic restrictions on the language, the thorough analysis of aliasing, the generation of verification conditions to prove termination, and the generation of verification conditions to ensure against such run-time errors as array bound violations and arithmetic overflow. We have used the system to verify several running FORTRAN programs. We present one such program and discuss its verification. (Author)