3. Verification of sequential and concurrent programs. Apt_ Olderog (3rd edition) (2010) (811405), страница 3
Текст из файла (страница 3)
. . . . . . . . . . . . . . .4.4Case Study: Binary Search . . . . . . . . . . . . . . . . . . . . . . . . . . . .Partial Correctness . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .Total Correctness . . . . . . . . . . . . .
. . . . . . . . . . . . . . . . . . . . . . . .4.5Exercises . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .4.6Bibliographic Remarks . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .1271291291311321321341371381391441451471491505Recursive Programs with Parameters . . .
. . . . . . . . . . . . . . . . . .5.1Syntax . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .5.2Semantics . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .5.3Verification . . . . . . . . .
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .Partial Correctness: Non-recursive Procedures . . . . . . . . . . . .Partial Correctness: Recursive Procedures . . . . . . . . . . . . . . .Modularity . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . .Total Correctness . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .Soundness . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .5.4Case Study: Quicksort . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . .Formal Problem Specification . . . . . . . . . . . . . . . . . . . . . . . . . .Properties of P artition . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .Auxiliary Proof: Permutation Property . . . . . . . . . . . . . . . . . .Auxiliary Proof: Sorting Property . . . . .
. . . . . . . . . . . . . . . . .Total Correctness . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .5.5Exercises . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .5.6Bibliographic Remarks . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . .1511521541571581621651651671721731731741751801821826Object-Oriented Programs . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .6.1Syntax . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . .Local Expressions . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .Statements and Programs . . . . . . . . . . . . . . . . . . . . . . . . . . . . .6.2Semantics . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .Semantics of Local Expressions . . . . . . . . . . . . . . .
. . . . . . . . . .Updates of States . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .Semantics of Statements and Programs . . . . . . . . . . . . . . . . . .6.3Assertions . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . .Substitution . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .6.4Verification . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .185187187188192192194195197199200xxContents6.56.66.76.86.96.106.11Partial Correctness .
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .Total Correctness . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .Adding Parameters . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .Semantics . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . . . . . . . . . . . .Partial Correctness . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .Total Correctness . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .Transformation of Object-Oriented Programs . . . . . . . . . . . .Soundness . . . . . .
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .Object Creation . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .Semantics . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .Assertions . . . . . . . . .
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .Verification . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .Soundness . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . .Case Study: Zero Search in Linked List . . . . . . . . . . . . . . . . . .Partial Correctness . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .Total Correctness . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .Case Study: Insertion into a Linked List . . . . . . . . .
. . . . . . . .Exercises . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .Bibliographic Remarks . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .201204206207208210211214217218219223225226226229232238240Part III Parallel Programs7Disjoint Parallel Programs . .
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .7.1Syntax . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .7.2Semantics . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .Determinism . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . .Sequentialization . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .7.3Verification . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .Parallel Composition . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . . . .Auxiliary Variables . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .Soundness . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .7.4Case Study: Find Positive Element . . .
. . . . . . . . . . . . . . . . . .7.5Exercises . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .7.6Bibliographic Remarks . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .2452472482492522532542562592612642668Parallel Programs with Shared Variables . . .
. . . . . . . . . . . . . . .8.1Access to Shared Variables . . . . . . . . . . . . . . . . . . . . . . . . . . . .8.2Syntax . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .8.3Semantics . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . .Atomicity . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .8.4Verification: Partial Correctness . . . . . . . . . . . . . . . . . . . . . . . .Component Programs . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .No Compositionality of Input/Output Behavior . . . . . .
. . . .Parallel Composition: Interference Freedom . . . . . . . . . . . . . .Auxiliary Variables Needed . . . . . . . . . . . . . . . . . . . . . . . . . . . .267269270271272274274275276279ContentsSoundness . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . . . . . . . . .Verification: Total Correctness . . . . . . . . . . . . . . . . . . . . . . . . .Component Programs . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .Parallel Composition: Interference Freedom . . . . . . . . . . . .
. .Soundness . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .Discussion . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .Case Study: Find Positive Element More Quickly . . . . . . . . .Allowing More Points of Interference . .
. . . . . . . . . . . . . . . . . .Case Study: Parallel Zero Search . . . . . . . . . . . . . . . . . . . . . . .Step 1. Simplifying the program . . . . . . . . . . . . . . . . . . . . . . . .Step 2. Proving partial correctness . . . . . . . . . . . . . . . . . . . . . .Exercises . . . . . . . . . . .
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .Bibliographic Remarks . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .282284284286288289291294299299300303305Parallel Programs with Synchronization . . . . . . . . . . . . . . . . . .9.1Syntax . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . . . . . . . . . . .9.2Semantics . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .9.3Verification . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . .Partial Correctness . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .Weak Total Correctness . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .Total Correctness . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
