Experiments in Domonstrating the Correctness of Software.

摘要

This thesis was undertaken to examine the post-development process of verifying the correctness of software programs, specifically to evaluate the effectiveness and practicality of several proposed methods of verification. Of interest were the degree to which utilization of a given method can be said to demonstrate correctness and the feasibility for general use of that method. The method of research was to study current literature concerning software testing and formal proofs of correctness, select a well-documented program of intermediate size for experimentation, apply selected verification methods to that program, and finally to compare the results of the several experimental demonstrations of correctness. The experiments conducted included a proof of correctness and dynamic testing with test data cases selected by a condition table method, by path analysis, and by structural decomposition of the program. (Author).