Excerpt from Correct-Program Technology/Extensibility of Verifiers: Two Papers on Program Verification In our approach then, correct praas can be used to generate new correct praas, in much the same way as new correct algebraic or logical formulae can be gererated by combining old formulae. This suggests the following view of the programming process: that it amounts to a type of formal manipulation roughly analogous to algebraic computation, in which text fragments expressing elementary, essentially irreducible, correct algorithms are combined to yield correct programs adapted to one or to another intended application. (and developed to the point at which program efficiency becomes acceptable.) From this point of View, what has been lacking till now is simply a sufficiently full and formal statement of the rules for manipulation and composition of correct praas; here it should be noted that these rules necessarily relate to correct praas and not simply to program texts, which may perhaps help explain why full statement of them has been so long delayed. Observe then that, regarding programming as a type of formal manipulation akin to the algebraic manipulation of (possibly very large) formulae, we can understand why much but not all of it is experienced psychologically as having a routine flavor rather than smacking of the intensely creative. From this same point of view we may say that, just as the generation of reliably correct large algebraic formulae must rest on the use of a formula manipulation program, 80 the reliable generation of large correct praas must rest on theibrmal use of a programmed praa manipulator. In both cases, the probability of error becomes overwhelming if one tries to work manually with large texts. Extending this analogy, we may liken the informal procedures which characterize much of today's programming to what algebraic calculation might be if. 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.