3. Verification of sequential and concurrent programs. Apt_ Olderog (3rd edition) (2010) (811405), страница 20
Текст из файла (страница 20)
However, as the proof systems become more complicated, sodo their completeness proofs.In fact, for parallel and distributed programs the proofs become quiteinvolved and tedious. We do not give these proofs and concentrate insteadon the use of these proof systems for verifying programs, which is the maintopic of this book.3.6 Parallel AssignmentAn assignment u := t updates only a single or subcripted variable u. Often itis convenient to update several variables in parallel, in one step. To this end,we introduce the parallel assignment which updates a list of variables by thevalues of a corresponding list of expressions.
For example, using a parallelassignment we can writex, y := y, xto express that the values of the variables x and y are swapped in a singlestep. With ordinary assigments we need an additional variable, say h, totemporarily store the value of x. Then, the sequential composition923 while Programsh := x; x := y; y := hof assignments has the same effect as the parallel assignment above, exceptfor the variable h. This shows the usefulness of the parallel assignment.
Laterin Chapter 5, we use it to model the semantics of the call-by-value parametermechanism in recursive procedures.In this section, we briefly introduce syntax, semantics, and an axiom forthe verification of parallel assignments.SyntaxWe extend the syntax of while programs S by the following clause for parallelassignments:S ::= x̄ := t̄,where x̄ = x1 , . .
. , xn is a non-empty list of distinct simple variables of typesT1 , . . . , Tn and t̄ = t1 , . . . , tn a corresponding list of expressions of typesT1 , . . . , Tn .SemanticsThe operational semantics of a parallel assignment is defined by the following variant of the transition axiom (ii) for ordinary assignments, stated inSection 3.2:(ii ′ ) < x̄ := t̄, σ > → < E, σ[x̄ := σ(t̄)] >Thus semantically, a parallel assignment is modelled by a simultaneous update of the state. Just as the ordinary assignment, a parallel assignmentterminates in one transition step.As in Section 3.2 we define the input-output semantics of partial and totalcorrectness, referring to the above transition axiom in the case of a parallelassignment. In particular, we haveN [[x̄ := t̄]](σ) = {σ[x̄ := σ(t̄)]}for both N = M and N = Mtot .Example 3.8.
Now we can make precise the semantic relationship betweenthe two programs for the swap operation:N [[x, y := y, x]](σ) = N [[h := x; x := y; y := h]](σ) mod {h}(3.37)3.6 Parallel Assignment93for both N = M and N = Mtot . In the following we prove this relationship.By the semantics of parallel assignments, the left-hand side of (3.37) yieldsN [[x, y := y, x]](σ) = {σ x,y },where σ x,y = σ[x, y := σ(y), σ(x)]. By definition, the simultaneous updatecan be serialized as follows:σ x,y = σ x [y := σ(x)],σ x = σ[x := σ(y)].In turn, the sequential composition of the three assignments of the right-handside of (3.37) yieldsN [[h := x; x := y; y := h]](σ) = {σ h,x,y },where we use the following abbreviations:σ h,x,y = σ h,x [y := σ h,x (h)],σ h,x = σ h [x := σ h (y)],σ h = σ[h := σ(x)].Thus to prove (3.37), it suffices to show the following three claims:1.
σ x,y (x) = σ h,x,y (x),2. σ x,y (y) = σ h,x,y (y),3. σ x,y (v) = σ h,x,y (v) for all simple and array variables v different from x, yand h.The proofs of these claims use the Coincidence Lemma 2.3 and the definitionof an update of a state.Re: 1. We calculate:σ x,y (x) = σ x (x) = σ(y) = σ h (y) = σ h,x (x) = σ h,x,y (x).Re: 2. We calculate:σ x,y (y) = σ(x) = σ h (h) = σ h,x (h) = σ h,x,y (y).Re: 3. We calculate:σ x,y (v) = σ(v) = σ h,x,y (v).This completes the proof of (3.37).⊓⊔943 while ProgramsVerificationThe assignment axiom introduced in Section 3.3, axiom 2, can be easilyadapted to parallel assignment, using simultaneous substitution:AXIOM 2′ : PARALLEL ASSIGNMENT{p[x̄ := t̄]} x̄ := t̄ {p}This axiom is sound for both partial and total correctness.
We call thecorresponding proof systems PW ′ and TW ′ , that is, PW and TW extendedby axiom 2′ , respectively. Definitions 3.6 and 3.8 of proof outlines for partial and total correctness, respectively, carry over to programs with parallelassignments in a straightforward way.Example 3.9. For the program S ≡ x, y := y, x we prove the correctnessformula{x = x0 ∧ y = y0 } S {x = y0 ∧ y = x0 }in the proof system PW ′ . Here the fresh variables x0 and y0 are used toexpress the swap property of S. In the precondition x0 and y0 freeze theinitial values of the variables x and y, respectively, so that these values canbe compared with the new values of these variables in the postcondition.
Wesee that the values of x and y are swapped.We represent the correctness proof in PW ′ as a proof outline:{x = x0 ∧ y = y0 }{y = y0 ∧ x = x0 }S{x = y0 ∧ y = x0 }.The initial application of the consequence rule exploits the commutativityof logical conjunction. Then axiom 2′ is applied to S with the substitution[x, y := y, x].⊓⊔3.7 Failure StatementIn this section we introduce a simple statement the execution of which cancause a failure, also called an abortion.
The computation of a program withsuch a statement can either yield a final state, diverge or, what is new, terminate in a failure.3.7 Failure Statement95SyntaxWe extend the syntax of while programs by the following clause for a failurestatement:S ::= if B → S1 fi,where B is a Boolean expression, called the guard of S, and S1 a statement.We refer to the resulting programs as failure admitting programs.The statement if B → S fi is executed as follows. First the guard B is evaluated.
If B is true, S is executed; otherwise a failure arises. So the executionof the statement if B → S fi crucially differs from that of if B then S fi.Namely, if B evaluates to false, the latter statement simply terminates.The fact that the failure statement fails rather than terminates if its guardevaluates to false allows us to program checks for undesired conditions. Forexample, to avoid integer division by 0, we can writeif y 6= 0 → x := x div y fi.In case of y = 0 this program raises a failure.
By contrast, the conditionalstatementif y 6= 0 then x := x div y fialways properly terminates and does not raise any exception.In the same way, we may use the failure statement to check whether anarray is accessed only within a certain section. For example, executingif 0 ≤ i < n → x := a[i] firaises a failure if the array a is accessed outside of the section a[0 : n − 1].Thus the failure statement can be used to model bounded arrays.As a final example consider the problem of extending the parallel assignment to the subscripted variables. A complication then arises that some parallel assignments can lead to a contradiction, for example a[s1 ], a[s2 ] := t1 , t2 ,when s1 and s2 evaluate to the same value while t1 and t2 evaluate to different values.
The failure statement can then be used to catch the error. Forexample, we can rewrite the above problematic parallel assignment toif s1 6= s2 ∨ t1 = t2 → a[s1 ], a[s2 ] := t1 , t2 fithat raises a failure in the case when the parallel assignment cannot be executed.963 while ProgramsSemanticsThe operational semantics of a failure statement is defined by the followingtwo transition axioms:(iv ′ ) < if B → S fi, σ > → < S, σ > where σ |= B,(v ′ )< if B → S fi, σ > → < E, fail > where σ |= ¬B,that should be compared with the transition axioms (iv) and (v) concernedwith the conditional statement if B then S fi.Here fail is a new exceptional state representing a runtime detectablefailure or abortion.
It should be contrasted with ⊥, representing divergence,which in general cannot be detected in finite time. Note that configurationsof the form < S, fail > have no successor in the transition relation → .Definition 3.14. Let σ be a proper state.(i) A configuration of the form < S, fail > is called a failure.(ii) We say that a failure admitting program S can fail from σ if there is acomputation of S that starts in σ and ends in a failure.⊓⊔Note that the Absence of Blocking Lemma 3.2 does not hold any more forfailure admitting programs because failures block the computation.The partial correctness semantics of M[[S]] of the failure admitting program S is defined as before.
However, the total correctness semantics is nowdefined by taking into account the possibility of a failure. Given a properstate σ we putMtot [[S]](σ) =M[[S]](σ)∪ {⊥ | S can diverge from σ}∪ {fail | S can fail from σ}.This definition suggests that a failure admitting program can yield more thanone outcome. However, this is obviously not the case since the DeterminismLemma 3.1 still holds and consequently Mtot [[S]](σ) has exactly one element,like in the case of the while programs.VerificationThe notions of partial and total correctness of the failure admitting programsare defined in the familiar way using the semantics M and Mtot . For example,total correctness is defined as follows:|=tot {p} S {q} if Mtot [[S]]([[p]]) ⊆ [[q]].3.8 Auxiliary Axioms and Rules97Note that by definition, fail, ⊥ 6∈ [[q]] holds; so |=tot {p} S {q} implies thatS neither fails nor diverges when started in a state satisfying p.To prove correctness of the failure admitting programs we introduce twoproof rules.
In the following proof rule for partial correctness we assume thatthe guard B evaluates to true when S is executed.RULE 4 ′ : FAILURE{p ∧ B} S {q}{p} if B → S fi {q}In contrast, in the following proof rule for total correctness we also haveto show that the precondition p implies that the guard B evaluates to true,thus avoiding a failure.RULE 4 ′′ : FAILURE IIp → B, {p} S {q}{p} if B → S fi {q}We have the following counterpart of the Soundness Theorem 3.1.Theorem 3.6. (Soundness)(i) The proof system PW augmented by the failure rule is sound for partialcorrectness of failure admitting programs.(ii) The proof system TW augmented by the failure II rule is sound for totalcorrectness of failure admitting programs.Proof. See Exercise 3.6.⊓⊔We shall discuss other statements that can cause a failure in Chapters 6and 10.3.8 Auxiliary Axioms and RulesApart from using proof outlines the presentation of correctness proofs canbe simplified in another way —by means of auxiliary axioms and rules.
Theyallow us to prove certain correctness formulas about the same program separately and then combine them. This can lead to a different organization ofthe correctness proof.In the case of while programs these axioms and rules for combining correctness formulas are not necessary, in the sense that their use in the correctness proof can be eliminated by applying other rules. This is the consequenceof the Completeness Theorem 3.5. That is why these rules are called auxiliaryrules.983 while ProgramsApart from the decomposition rule A1 introduced in Section 3.3, the following auxiliary axioms and rules are used in proofs of partial and totalcorrectness for all classes of programs considered in this book.AXIOM A2: INVARIANCE{p} S {p}where f ree(p) ∩ change(S) = ∅.RULE A3: DISJUNCTION{p} S {q}, {r} S {q}{p ∨ r} S {q}RULE A4: CONJUNCTION{p1 } S {q1 }, {p2 } S {q2 }{p1 ∧ p2 } S {q1 ∧ q2 }RULE A5: ∃-INTRODUCTION{p} S {q}{∃x : p} S {q}where x does not occur in S or in f ree(q).RULE A6: INVARIANCE{r} S {q}{p ∧ r} S {p ∧ q}where f ree(p) ∩ change(S) = ∅.RULE A7: SUBSTITUTION{p} S {q}{p[z̄ := t̄]} S {q[z̄ := t̄]}where ({z̄} ∩ var(S)) ∪ (var(t̄) ∩ change(S)) = ∅.Here and elsewhere {z̄} stands for the set of variables present in the sequence z̄ and var(t̄) for the set of all simple and array variables that occur inthe expressions of the sequence t̄.
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
