Advertisement

Safety Properties

  • José Bacelar Almeida
  • Maria João Frade
  • Jorge Sousa Pinto
  • Simão Melo de Sousa
Part of the Undergraduate Topics in Computer Science book series (UTICS)

Abstract

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.

Keywords

Program Expression Verification Condition Verification Method Interpretation Structure Array Position 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.

References

  1. 1.
    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) CrossRefGoogle Scholar
  2. 2.
    Reynolds, J.C.: Reasoning about arrays. Commun. ACM22(5), 290–299 (1979) MATHCrossRefGoogle Scholar
  3. 3.
    Reynolds, J.C.: The Craft of Programming. Prentice-Hall International, Upper Saddle River (1981) MATHGoogle Scholar
  4. 4.
    Reynolds, J.C.: Theories of Programming Languages. Cambridge University Press, Cambridge (1998) MATHCrossRefGoogle Scholar
  5. 5.
    Reynolds, J.C.: Programs that use arrays. Class Notes, Carnegie-Mellon University (February 2004) Google Scholar

Copyright information

© Springer-Verlag London Limited 2011

Authors and Affiliations

  • José Bacelar Almeida
    • 1
  • Maria João Frade
    • 2
  • Jorge Sousa Pinto
    • 1
  • Simão Melo de Sousa
    • 2
  1. 1.Depto. InformáticaUniversidade do MinhoBragaPortugal
  2. 2.Depto. InformáticaUniversidade Beira InteriorCovilhãPortugal

Personalised recommendations