A preliminary evaluation of verifiability in ADA

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.