ADA Exceptions: Specification and Proof Techniques.

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. (Author)

Open PDF

Document Details

Document Type
Technical Report
Publication Date
Feb 01, 1980
Accession Number
ADA086577

Entities

People

  • D. C. Luckham
  • W. Polak

Organizations

  • Stanford University

Tags

DTIC Thesaurus Topics

  • Abstracts
  • Classification
  • Computer Programming
  • Computer Science
  • Computers
  • Consistency
  • Contracts
  • Department Of Defense
  • Language
  • Programming Languages
  • Security
  • Semantics
  • Specifications
  • Standards
  • Structured Programming
  • Universities
  • Verification

Fields of Study

  • Computer science

Readers

  • Database Systems and Applications
  • Mathematical Modeling and Probability Theory.