TY - GEN
T1 - A preliminary evaluation of verifiability in ADA
AU - Tripathi, A. R.
AU - Young, W. D.
AU - Good, D. I.
PY - 1980/1/1
Y1 - 1980/1/1
N2 - In this paper we examine Ada with regard to program verification and make certain suggestions towards writing potentially provable Ada programs. We attempt 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. However, the possibility of having a large number of variables, potentially sharable among concurrent processes, is likely to make the proofs of Ada programs unmanageable. It is asserted, however, that with a certain discipline on the programmer verifiable programs can be written in Ada.
AB - In this paper we examine Ada with regard to program verification and make certain suggestions towards writing potentially provable Ada programs. We attempt 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. However, the possibility of having a large number of variables, potentially sharable among concurrent processes, is likely to make the proofs of Ada programs unmanageable. It is asserted, however, that with a certain discipline on the programmer verifiable programs can be written in Ada.
UR - http://www.scopus.com/inward/record.url?scp=85050507053&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=85050507053&partnerID=8YFLogxK
U2 - 10.1145/800176.809971
DO - 10.1145/800176.809971
M3 - Conference contribution
AN - SCOPUS:85050507053
T3 - Proceedings of the ACM 1980 Annual Conference, ACM 1980
SP - 218
EP - 224
BT - Proceedings of the ACM 1980 Annual Conference, ACM 1980
PB - Association for Computing Machinery, Inc
T2 - 1980 ACM Annual Conference, ACM 1980
Y2 - 27 October 1980 through 29 October 1980
ER -