An Extended Semantic Definition of Pascal for Proving the Absence of Common Runtime Errors

摘要

We present an axiomatic definition of Pascal which is the logical basis of the Runcheck system, a working verifier for proving the absence of runtime errors such as arithmetic overflow, array subscripting out range, and accessing an uninitialized variable. Such errors cannot be detected at compile time by most compilers. Because the occurrence of a runtime error may depend on the values of data supplied to a program, techniques for assuring the absence of errors must be based on program specifications. Runcheck accepts Pascal programs documented with assertions, and proves that the specifications are consistent with the program and not runtime errors can occur. Our axiomatic definition is similar to Hoare's axiom system, but it takes into account certain restrictions that have not been considered in previous definitions. For instance, our definition accurately models uninitialized variables, and requires a variable to have a well defined value before it can be accessed. The logical problems of introducing the concept of uninitialized variables are discussed. Our definition of expression evaluation deals more fully with function calls than previous axiomatic definitions. Some generalizations of our semantics are presented, including a new method for verifying programs with procedure and function parameters. Our semantics can be easily adopted to similar languages, such as ADA. One of the main potential problems for the user of a verifier is the need to write detailed, repetitious assertions. We develop some simple logical properties of our definition which are exploited by Runcheck to reduce the need for such detailed assertions. (Author)