Application of an informal program verification method to Ada

Author

Wieand, Bruce ; Howden, W.E.

Author_Institution

IBM Corp., Research Triangle Park, NC, USA

fYear

1994

fDate

27 Jun-1 Jul 1994

Firstpage

81

Lastpage

89

Abstract

The QDA informal program verifcation method is a comments analysis technique in which an analyst´s assumptions about a program are expressed in the form of structured comments in the program and are checked by an analyzer. Previous work has shown QDA to be effective for detecting errors in assembly language programs. An experiment was performed to determine how well QDA would scale to high-level languages. The implementation and use of a prototype analyzer for Ada indicated both the usefulness of QDA for high level languages and the desirability for further development of the prototype

Keywords

Ada; program debugging; program diagnostics; program verification; Ada; QDA; assembly language programs; comments analysis technique; error detection; high-level languages; informal program verification method; prototype; prototype analyzer; structured comments; Assembly; Azimuth; Computer languages; Formal verification; High level languages; Inspection; Military aircraft; Programming profession; Prototypes; Text analysis;

fLanguage

English

Publisher

ieee

Conference_Titel

Computer Assurance, 1994. COMPASS '94 Safety, Reliability, Fault Tolerance, Concurrency and Real Time, Security. Proceedings of the Ninth Annual Conference on

Conference_Location

Gaithersburg, MD

Print_ISBN

0-7803-1855-2

Type

conf

DOI

10.1109/CMPASS.1994.318465

Filename

318465