This chapter considers a method for dealing statically with the occurrence of errors during the execution of programs. Recall that to this point we have been considering that evaluation of an expression could never go wrong, and neither could the execution of a command.
This is clearly unsatisfying since in real-world languages runtime errors do occur, and one of the main uses of verification methods is precisely to ensure the safety of programs, i.e. the absence of such error situations. This chapter presents a general framework for reasoning with errors and safety.
KeywordsProgram Expression Verification Condition Verification Method Interpretation Structure Array Position
- 5.Reynolds, J.C.: Programs that use arrays. Class Notes, Carnegie-Mellon University (February 2004) Google Scholar