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 language | English (US) |
|---|---|
| Pages | 218-224 |
| Number of pages | 7 |
| State | Published - 1980 |
| Event | Proc Annu Conf ACM 80 - Nashville, TN, USA Duration: Oct 27 1980 → Oct 29 1980 |
Other
| Other | Proc Annu Conf ACM 80 |
|---|---|
| City | Nashville, TN, USA |
| Period | 10/27/80 → 10/29/80 |