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.

错误:搜索内容不能为空,请输入英文关键词
错误:关键词超出字数限制,请精简
高级检索

Safety Properties

  • José Bacelar Almeida,
  • Maria João Frade,
  • Jorge Sousa Pinto,
  • Simão Melo de Sousa

摘要

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.