3. Verification of sequential and concurrent programs. Apt_ Olderog (3rd edition) (2010) (811405), страница 2
Текст из файла (страница 2)
During this timewe have benefited very much from discussions with Pierre America, Jacode Bakker, Luc Bougé, Ed Clarke, Werner Damm, Henning Dierks, Edsger W. Dijkstra, Nissim Francez, David Gries, Tony Hoare, Shmuel Katz,Leslie Lamport, Hans Langmaack, Jay Misra, Cees Pierik, Andreas Podelski,Amir Pnueli, Gordon Plotkin, Anders P. Ravn, Willem Paul de Roever, FredSchneider, Jonathan Stavi and Jeffery Zucker. Many thanks to all of them.For the third edition Maarten Versteegh helped us with the migration offiles to adapt to the new style file. Alma Apt produced all the drawings inthis edition.The bibliography style used in this book has been designed by Sam Buss;Anne Troelstra deserves credit for drawing our attention to it.Finally, we would like to thank the staff of Springer-Verlag, in particularSimon Rees and Wayne Wheeler, for the efficient and professional handlingof all the stages of the production of this book.
The TEX support group ofSpringer, in particular Monsurate Rajiv, was most helpful.Amsterdam, The Netherlands,Oldenburg, Germany,Krzysztof R. Apt and Frank S. de BoerErnst-Rüdiger OlderogxivOutlines of One-Semester CoursesPrerequisites: Chapter 2.Course on Program SemanticsClass of programsSyntax Semanticswhile programs3.13.2Recursive programs4.14.2Recursive programswith parameters5.15.2Object-oriented programs6.16.2Disjoint parallel programs7.17.2Parallel programs withshared variables8.1, 8.28.3Parallel programs withsynchronization9.19.2Nondeterministic programs10.110.2Distributed programs11.111.2Fairness12.112.2Course on Program VerificationClass of programsSyntax SemanticsProof theorywhile programs3.13.23.3, 3.4, 3.10Recursive programs4.14.24.3, 4.4Recursive programswith parameters5.15.25.3Object-oriented programs6.16.2 6.3, 6.4, 6.5, 6.6Disjoint parallel programs7.17.27.3Parallel programs withshared variables8.1, 8.28.38.4, 8.5Parallel programs withsynchronization9.19.29.3Nondeterministic programs10.110.210.4Distributed programs11.111.211.4PrefacePrefaceCourse Towards Object-Oriented ProgramVerificationClass of programsSyntax Semantics Proof theory Case studieswhile programs3.13.23.3, 3.43.9Recursive programs4.14.24.3, 4.44.5Recursive programswith parameters5.15.25.35.4Object-oriented programs6.16.26.3, 6.46.8Course on Concurrent Program VerificationClass of programsSyntax Semantics Proof theory Case studieswhile programs3.13.23.3, 3.43.9Disjoint parallel programs7.17.27.37.4Parallel programs withshared variables8.1, 8.28.38.4, 8.58.6Parallel programs withsynchronization9.19.29.39.4, 9.5Nondeterministic programs10.110.210.410.5Distributed programs11.111.211.411.5Course on Program Verification withEmphasis on Case StudiesClass of programsSyntax Proof theory Case studieswhile programs3.13.3, 3.43.9Recursive programs4.14.3, 4.44.5Recursive programswith parameters5.15.45.4Object-oriented programs6.16.3–6.56.8Disjoint parallel programs7.17.37.4Parallel programs withshared variables8.1, 8.28.4, 8.58.6Parallel programs withsynchronization9.19.39.4, 9.5Nondeterministic programs 10.1, 10.310.410.5Distributed programs11.111.411.5xvContentsPreface .
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . ixOutlines of One-semester Courses . . . . . . . . . . . . . . . . . . . . . . . . . . . . . xivPart I In the Beginning1Introduction . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . . . . . . . . . .1.1An Example of a Concurrent Program . . . . . . . . . . . . . . . . . .Solution 1 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .Solution 2 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . .Solution 3 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .Solution 4 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .Solution 5 . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . . . . . . . . . . . . . .Solution 6 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .1.2Program Correctness . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .1.3Structure of this Book . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .1.4Automating Program Verification . . .
. . . . . . . . . . . . . . . . . . . .1.5Assertional Methods in Practice . . . . . . . . . . . . . . . . . . . . . . . .344568910111316172Preliminaries . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .2.1Mathematical Notation . . . . .
. . . . . . . . . . . . . . . . . . . . . . . . . .Sets . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .Tuples . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .Relations . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . . . . . . . . . . . . . .Functions . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .Sequences . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .Strings . . . . . . . . . . . . .
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .Proofs . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .Induction . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . .Grammars . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .2.2Typed Expressions . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .Types . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .19212122232324252627292929xviixviiiContents2.32.42.52.62.72.82.92.10Variables . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .Constants . . . . . . . . . .
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .Expressions . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .Subscripted Variables . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .Semantics of Expressions . . . . . . . . . . . . .
. . . . . . . . . . . . . . . . .Fixed Structure . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .States . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .Definition of the Semantics . . . . . .
. . . . . . . . . . . . . . . . . . . . . .Updates of States . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .Formal Proof Systems . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .Assertions . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . . . . . . .Semantics of Assertions . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .Substitution . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .Substitution Lemma . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . . . .Exercises . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .Bibliographic Remarks . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .30303132323334353638394142475051Part II Deterministic Programs3while Programs . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . . . . . .3.1Syntax . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .3.2Semantics . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .Properties of Semantics . . . .
. . . . . . . . . . . . . . . . . . . . . . . . . . .3.3Verification . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .Partial Correctness . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .Total Correctness . . . . . . . . . .
. . . . . . . . . . . . . . . . . . . . . . . . . . .Decomposition . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .Soundness . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .3.4Proof Outlines . . . . . . . .
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .Partial Correctness . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .Total Correctness . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .3.5Completeness . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . . . . . . . . .3.6Parallel Assignment . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .3.7Failure Statement . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .3.8Auxiliary Axioms and Rules . . . . . . . . . . . . . .
. . . . . . . . . . . . .3.9Case Study: Partitioning an Array . . . . . . . . . . . . . . . . . . . . . .3.10Systematic Development of Correct Programs . . . . . . . . . . . .Summation Problem . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . .3.11Case Study: Minimum-Sum Section Problem . . . . . . . . . . . . .3.12Exercises . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .3.13Bibliographic Remarks . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .5557586263657073737979838591949799113115116121124Contentsxix4Recursive Programs .
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .4.1Syntax . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .4.2Semantics . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .Properties of the Semantics . . . . . . . . . . .
. . . . . . . . . . . . . . . . .4.3Verification . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .Partial Correctness . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .Total Correctness . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . . . . .Decomposition . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .Discussion . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .Soundness . . . . . . . . . . . . . . . . . . . . . . . . . . . .
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
