Swipe to navigate through the chapters of this book
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.
Please log in to get access to this content
Hartel, P.H., Moreau, L.: Formalizing the safety of Java, the Java virtual machine, and Java card. ACM Comput. Surv. 33(4), 517–558 (2001) CrossRef
Reynolds, J.C.: The Craft of Programming. Prentice-Hall International, Upper Saddle River (1981) MATH
Reynolds, J.C.: Programs that use arrays. Class Notes, Carnegie-Mellon University (February 2004)
- Safety Properties
Dr. José Bacelar Almeida
Dr. Maria João Frade
Dr. Jorge Sousa Pinto
Dr. Simão Melo de Sousa
- Springer London
- Sequence number
- Chapter number
- Chapter 7