A Complete and Consistent Hoare Axiomatics for a Simple Programming Language
John C. Cherniavsky, Samuel N. Kamin · Journal of the ACM · 1979
A sunple programming language ffm IS defined for which a complete axiomatics is obtamable.Completeness is shown by presemmg a relauvely complete Hoare ax~omaUcs, demonstrating, by direct constmcuon, that the first-order theory of addmon ~+ as express,ve, and noting that ~+ Is complete.It is then shown that • ~m aS maxunal wath this property Further, a notton of complexity of a Hoare system is introduced based upon the lengths of proofs (dasregardmg proofs m the underlying logsc), and the system -~m, .~+ is shown to have polynomial complexity The nouon ts shown to be nontnvlal by presenting a language for which any Hoare axiom system has exponenual complextty rK~v WORDS AND PHRASES venficatmn, logic, complexity, theory of computation, programming languages, subrecurslve functions CR CATEGORIES' 5 21, 5 24, 5 25