|
An Overview of Formal Program Proving and the Correctness of ADA Programs
A failure of a computer software system in a safety-critical system can cause disastrous consequences. The traditional method of program testing in software development can only improve our confidence in a software system to a certain degree. In this research, we set out to investigate if there is any alternative that will overcome the inherent weaknesses of program testing and will enable us to obtain the highest practicable degree of confidence in a software system.
This research will focus on the possibility of using formal methods to prove (argue and reason about logically) the correctness of computer programs. We will study the theoretical foundations and practical feasibility of such an approach. In particular, we will examine the provability of the Ada programming language as opposed to other programming languages. An initial attempt to establish a formal system for the Ada programming language is discussed. Furthermore we evaluate and demonstrate the methods to prove the correctness of Ada programs. A number of sample proofs will be given and discussions will be made on some theoretical and practical issues encountered in the proofs.
| 
