The bibliographic entry was discovered and compiled by a machine, and published without a person checking it against the publication. The publication itself is the authors' own work — this badge says nothing about it.
A Complete and Consistent Hoare Axiomatics for a Simple Programming Language
From OpenAlex, which stores abstracts as an
index of words and their positions: what is shown is rebuilt from that,
and reads fluently whether or not it is what the author wrote.
Abstract
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
@article{cherniavsky1979complete,
title = {A Complete and Consistent Hoare Axiomatics for a Simple Programming Language},
author = {John C. Cherniavsky and Samuel N. Kamin},
year = {1979},
journal = {Journal of the ACM},
publisher = {Association for Computing Machinery},
volume = {26},
number = {1},
pages = {119--128},
doi = {10.1145/322108.322120},
}