Accession Number:

ADA230611

Title:

Toward Ada Verification: A Collection of Relevant Topics

Descriptive Note:

Final rept.

Corporate Author:

INSTITUTE FOR DEFENSE ANALYSES ALEXANDRIA VA

Report Date:

1986-06-01

Pagination or Media Count:

133.0

Abstract:

IDA Paper P-1900, Towards Ada Verification A Collection of Relevant Topics, is a survey of various topics in Ada verification, the state of progress in both near-term and far-term goals, and some possible directions for future work. Chapter 1 studies the extent to which the existing general purpose literature on program verification already covers the Ada language and concludes with an annotated bibliography. Chapter 2 surveys the possibility of adapting existing verification tools as near-term vehicles for Ada verification. Chapter 3 is a discussion of specification languages, cast in the form of a commentary on and criticism of ANNA, with suggestions for some extensions and improvements to it. Chapter 4 describes the far-term European project for a formal definition of the whole of Ada. It concludes with a brief discussion of the possibility of standards for the acceptance of verification systems. Chapter 5 presents the results of an attempt to survey as wide as possible a community of users, in particular, Ada users, on the ways in which, if at all, they use features of Ada which currently present problems for verification.

Subject Categories:

  • Computer Programming and Software

Distribution Statement:

APPROVED FOR PUBLIC RELEASE