BIB-VERSION:: CS-TR-v2.0
          ID:: STAN//CS-TR-80-789
       ENTRY:: June 08, 1995
ORGANIZATION:: Stanford University, Department of Computer Science
       TITLE:: ADA exceptions: specification and proof techniques
        TYPE:: Technical Report
      AUTHOR:: Luckham, David C.
      AUTHOR:: Polak, Wolfgang
        DATE:: February 1980
       PAGES:: 20
    ABSTRACT:: A method of documenting exception propagation and handling in
               Ada programs is proposed. Exception propagation declarations
               are introduced as a new component of Ada specifications. This
               permits documentation of those exceptions that can be
               propagated by a subprogram. Exception handlers are documented
               by entry assertions. Axioms and proof rules for Ada
               exceptions are given. These rules are simple extensions of
               previous rules for Pascal and define an axiomatic semantics
               of Ada exceptions. As a result, Ada programs specified
               according to the method can be analysed by formal proof
               techniques for consistency with their specifications, even if
               they employ exception propagation and handling to achieve
               required results (i.e. non-error situations). Example
               verifications are given.
       NOTES:: [Adminitrivia V1/Prg/19950608]
         END:: STAN//CS-TR-80-789