Abstract
Axiomatic analysis extracts from the functions and predicates of a program the properties and relations upon which the correct functioning of the program is based. The analysis is done by converting the program to a program scheme and studying a correctness proof for the scheme. Information of this sort can be used to look for programs whose correctness does not depend on axioms of arithmetic which may not hold in a computer implementation. Another application is to the problem of choosing appropriate data structures for implementation of an algorithm. Several sample programs are examined, and in one case, a comparison made of the properties required for implementations of different recursive definitions of a function.