Safety Properties
摘要
This chapter considers a method for dealing 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. In particular, in \(\mathsf {While^{int}}\) division by zero did not go wrong, and the range of arrays in \(\mathsf {While^{array}}\) was \(\mathbb {Z}\) . Finite ranges could not be supported, since there was no way to signal an error when some command tried to access a position of an array outside its range.