Accession Number:

AD0767335

Title:

Axiomatic Approach to Total Correctness of Programs

Descriptive Note:

Corporate Author:

STANFORD UNIV CA DEPT OF COMPUTER SCIENCE

Personal Author(s):

• Manna, Zohar
• Pnueli, Amir

Report Date:

1973-07-01

Pagination or Media Count:

29.0

Abstract:

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.

Descriptors:

• *COMPUTER PROGRAMMING
• *MATHEMATICAL LOGIC
• INEQUALITIES
• MAPPING(TRANSFORMATIONS)

Subject Categories:

• Theoretical Mathematics
• Computer Programming and Software

Distribution Statement:

APPROVED FOR PUBLIC RELEASE