PRELIMINARY EVALUATION OF VERIFIABILITY IN ADA.

A. R. Tripathi, W. D. Young, D. I. Good

Research output: Contribution to conferencePaper

1 Scopus citations

Abstract

An examination is made of Ada with regard to program verification and make certain suggestions towards writing potentially provable Ada programs. An attempt is made to isolate and discuss those features of Ada which are not susceptible to current verification techniques. From verifiability considerations, the most critical features in Ada appear to be those which deal with data sharing under concurrent processing, direct referencing of non-local variables, access variables, ″approximate″ data-types, and generic program units. The independence of program units along with well defined interfaces for interactions is presented as desirable not only from software engineering aspects but also from the formal proof considerations.

Original languageEnglish (US)
Pages218-224
Number of pages7
StatePublished - Jan 1 1980
EventProc Annu Conf ACM 80 - Nashville, TN, USA
Duration: Oct 27 1980Oct 29 1980

Other

OtherProc Annu Conf ACM 80
CityNashville, TN, USA
Period10/27/8010/29/80

Fingerprint Dive into the research topics of 'PRELIMINARY EVALUATION OF VERIFIABILITY IN ADA.'. Together they form a unique fingerprint.

  • Cite this

    Tripathi, A. R., Young, W. D., & Good, D. I. (1980). PRELIMINARY EVALUATION OF VERIFIABILITY IN ADA.. 218-224. Paper presented at Proc Annu Conf ACM 80, Nashville, TN, USA, .