Correct-program Technology/Extensibility of Verifiers. Two Papers on Program Verification. By Martin Davis and J.T. Schwartz

Excerpt from Correct-Program Technology/Extensibility of Verifiers: Two Papers on Program Verification
By now the potential importance of formal techniques for proving program correctness has been recognized for over two decades, and something between four and seven hundred papers principally devoted to the development of such techniques have been published (see [London, 1970], [1972] for useful reviews of existing literature). A wide variety of formalisms have been proposed; among these, the inductive assertion technique of [Floyd, 1967], and the variant of it proposed and repeatedly extended by Hoare [1969], [1971] [1972] seem most convenient. But in spite of all this work, a truly practical program verification technology has been slow to develop. The essential difficulty not yet overcome is economic: the cost of formal program verification using existing teachniques is still much too high. This objection is best understood if we consider the way in which a fully formal variant of the Floyd technique would operate. In this approach, one is given a program text P, to which an input assumption I and an output assertion are attached. (These assertions are written in any convenient, sufficiently powerful, logical formalism, e.g., predicate calculus supplemented by Zermelo-Frankel set theory. In general, we shall use LF to denote whatever logical formalism is used.) Call a program text thus annotated (i.e., carrying attached assumptions and assertions) a praa.
About the Publisher
Forgotten Books publishes hundreds of thousands of rare and classic books. Find more at www.forgottenbooks.com
This book is a reproduction of an important historical work. Forgotten Books uses state-of-the-art technology to digitally reconstruct the work, preserving the original format whilst repairing imperfections present in the aged copy. In rare cases, an imperfection in the original, such as a blemish or missing page, may be replicated in our edition. We do, however, repair the vast majority of imperfections successfully; any imperfections that remain are intentionally left to preserve the state of such historical works.