A Verification Condition Generator for FORTRAN.
Abstract
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)
Document Details
- Document Type
- Technical Report
- Publication Date
- Jun 01, 1980
- Accession Number
- ADA094609
Entities
People
- J. Strother Moore
- Robert S. Boyer
Organizations
- SRI International