PL/CV2(ID:7694/)Verifying logical dialect of PL/CS - Country: us
- Began: 1982
- Type:Predicate
- Sammet:SPC
Version 2 of PL/CV
Related languages
References:
1982- Constable, R. L. S. D. Johnson , C. D. Eichenlaub, An Introduction to the PL/CV2 Programming Logic, Springer-Verlag New York, Inc., Secaucus, NJ, 1982 view detailsExtract: PREFACE
PREFACE
This book is based on the reference manual for the PL/CV Programming Logic and on lecture notes used to teach the logic to first year college students. The Programming Logic consists of a formal system for reasoning about integers, arrays, and programming language commands (in the PL/I dialect called PL/CS). The arguments can be checked by the PL/CV Proof Checker [...]. The programs can be executed by PL/CS compilers [...], including the Cornell Program Synthesizer [...] and the Cornell Program Environment.
The notes are written from the point of view that computer programming is formal algorithmic problem solving. The subject is formal because problem solutions must be written so that a computer can execute them. la some cases this formality can be extended to the entire argument which led to the solution, and the computer can be used to verify the argument.
In cases when the entire argument can be formalized, there are obvious advantages to doing so. For one thing, one"s confidence in the solution is appreciably increased. This observation has been the basis for research in the subject called program verification[...]. Another advantage of formalization is pedagogical - one is able to see the complete structure of the argument and explain it to someone who is learning to reason algorithmically. This is the same advantage that rigorous argument offers to any subject, and is a justification for teaching formal logic in the college curriculum.
Various computer systems to check proofs have been employed in the teaching of formal logic[...]. We feel that such systems can play an especially interesting role in computer science courses. In the first place, programming courses by necessity teach a great deal of formalism and logic. For example, the treatment of Boolean expressions in modern programming languages is an introduction to the prepositional calculus, and the definition of a program state and its effect on assertions in programs is the same as the concept of an interpretation in the predicate calculus.
In the second place, the concepts of program verification, especially the notions of asserted program, weakest pre-condition, loop invariant, procedure call rules, etc. have an increasing place in the computer science curriculum. A rigorous treatment of these concepts is close to a formal treatment in a very high level logic such as PL/CV. A formal treatment allows computer assistance in teaching the subject. In particular, the student can experiment with forms of argument in private and at his own pace.
In the third place, the Proof Checker, like the language translator, is an interesting piece of computer software. Exposing students to it will enhance their appreciation of the potential of computer automation.
For these reasons we feel it is appropriate to teach a programming logic in the computer science curriculum. These notes can be used for that purpose. They introduce a completely formal programming logic, PL/CV2. The logic and its Proof Checker were designed by R, L. Constable, S. D. Johnson, and M. J. O"Donnell. The logic has been reported in the book A Programming Logic and in various articles, and the Proof Checker is described in [various articles, and] the book "Computer System for Checking Proofs. The underlying programming language PL/CS is described in the textbook, The system is a merging of the predicate calculus and the Floyd-Hoare style of reasoning about programs. It was designed to be simple, conventional, high level and efficient so that it could be used in college courses, and so that it could be used to explore elementary program verification.
The odd-numbered chapters introduce topics informally at a very elementary level, and the even-numbered chapters provide a succinct and precise summary of the logic (which may be skipped on a first reading). Numerous examples are provided, and all of the complete proofs have been checked by the Proof Checker (PL/I version). The exposition in the odd-numbered sections is oriented toward the, reader with almost no programming experience. A more advanced account of the logic appears in A Programming Logic.
Experience with the system
We have used PL/CV2 at Cornell to teach logic and basic program verification in a sophomore discrete mathematics course. Our experiences here have been very positive. We also used PL/CV2 to teach introductory programming. We found that students were overwhelmed by the amount of formalism to be grasped at first encounter. We surmise that the system could be successfully used in a second course on programming to help teach the basics of programming methodology.
The interactive synthesizer version improves usability of PL/CV by a factor of 2 or 3 over the batch oriented system. We have not yet used that system in a course however.
The PL/CV programming logic has been considerably extended to include a rich constructive theory of types. In this language, called PL/CV3 it appears possible to formalize the kind of non-elementary algorithmic problem solving exhibited in such textbooks as The Design and Analysis of Computer Algorithms by Aho, Hopcroft and Ullman. The language was designed to allow a feasible formalization of any argument solving a sequential algorithmic problem
The reader interested in the concept of a constructive formal logic as a programming tool should follow the work of the Cornell Automated Logic group. The project on Program Refinement Logics, PRL, is building a programming system which extracts executable code fom formal constructive proofs. Extract: ACKNOWLEDGEMENTS
ACKNOWLEDGEMENTS
The PL/CV1 logic was designed with Michael J. O"Donnell whose active interest and keen insights have shaped the project at every stage. Our initial effort relied on the stability of the PL/C system and the support of its director, Richard Conway.
Our faculty colleagues at Cornell provided both constructive criticism and encouragement. In particular we thank Corky Cartwright, Alan Demers, Jim Donahue, and David Cries, Work on the interactive system, AVID, owes a great deal to Tim Teitelbaum and the Cornell Program Synthesizer Project.
Many former students were active participants in discussions of the logic and implementation. Carl Hauser was co-author of the first manual. Gary Levin and Barry Bakalor were especially helpful.
Special thanks are due the contributing authors, all of whom have also worked on the implementation, including Tat-hung Chan, Dean B. Krafft, Ryan Stansifer and Daniel Zlatin.
Michelle Fish prepared large parts of the manuscript using the UNIX text editing facilities. We are grateful for her very careful work.
Finally we thank our department and its chairman, Juris Hartmanis, who have provided such a stimulating and tolerant atmosphere for our work.
R. L, Constable S. D. Johnson C. D. Eichenlaub
Ithaca, N.Y. August 1981
1984- Constable, Robert L. and Zlatin, Daniel R. "The Type Theory of PL/CV3" ACM Transactions on Programming Languages and Systems (TOPLAS) 6(1) (January 1984) pp94-117 view detailsExtract: Logic of Programming versus Logic of Mathematics
Logic of Programming versus Logic of Mathematics
We investigate the logic of programming because it will help us understand the programming process and enable us to be better at it. This "self-improvement" motive is not the typical reason why people study the logic of mathematics; and traditional logic is not always a good role model for programming logic. Why is there this difference, and does it matter?
The chief reason for the difference is the computer. Programming is a formal activity unlike the "doing" of most other mathematics. It requires communication with unintelligent machines, which do not understand wonderful mathematical solutions to problems. A solution must be programmed, and this means formalized. Although the solution may be a function and hence similar in its form and precision to solutions in analysis and algebra, its description tends to be rather long by comparison with function descriptions in mathematics--say, a page or two instead of a line or two.
More significantly, the exacting requirements of formality and the inherently arbitrary nature of programming formalisms make it very difficult for people to check every detail of these long solutions. In addition, features of programming languages introduced to allow efficient execution of programs complicate explanations of the solution by involving the eccentricities of a specific formalism. Confronted with these difficulties, computer scientists have been seeking logics that will explain programming solutions and permit mechanical help in finding, checking, and changing them. As it becomes more important to know that a program really does what it is claimed to do, that is, meet its specification, more details of the explanation are made explicit and formalized. The limit of this process is a completely formal proof that the program is correct. The program can be seen as the "executable part" of this proof (see [13]).
The more formal the explanation of a program, the greater the opportunity to use the computer to check or help generate it. This reflexive use of the computer to check itself is one of the most intriguing and promising areas of research into the problems of "software reliability" and into the nature of the programming process itself. These incentives to produce formal algorithmic proofs seem to be much higher than any incentive to do the same for mathematical arguments with no computational content. Nevertheless, one of the earliest and most significant efforts to actually use formal proofs was in the AUTOMATH project at Eindhoven in the Netherlands under the direction of N. G. deBruijn [14]. The goal of the project was to write formal mathematical proofs and check them by a computer program. DeBruijn imposed, by desire, the standards of extreme exactness that arise, by necessity, in programming.
The chief characteristics of AUTOMATH and the programming logics is that they are meant to be used, whereas the formal theories presented in logic textbooks are meant to be studied. This difference is crucial and is the driving force behind AUTOMATH as well as PL/CV [8, 11] and PRL [2, 3]. This characteristic means that the logic must be sufficiently expressive that it naturally captures all the informal arguments in the subject being considered. We claim that the V3 described here enjoys such expressiveness.
|