What do you think?
Rate this book
Correct-Program Technology/Extensibility of Verifiers: Two Papers on Program Verification
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.
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.
152 pages, Hardcover
Published March 5, 2018
About the author
Martin D. Davis
19 books13 followersMartin David Davis (born 1928) is Professor Emeritus at New York University's Computer Science Department.
Ratings & Reviews
Friends & Following
Create a free account to discover what your friends think of this book!
Community Reviews
No one has reviewed this book yet.