Axiomatic Approach to Total Correctness of Programs
STANFORD UNIV CA DEPT OF COMPUTER SCIENCE
Pagination or Media Count:
The authors present an axiomatic approach which enables one to prove by formal methods that his program is totally correct i.e., it terminates and is logically correct -- does what it is supposed to do. The approach is similar to Hoares approach for proving that a program is partially correct i. e., that whenever it terminates it produces correct results. The extension to Hoares method lies in the possibility of proving correctness and termination at once, and in the enlarged scope of properties that can be proved by it.
- Theoretical Mathematics
- Computer Programming and Software