3. Verification of sequential and concurrent programs. Apt_ Olderog (3rd edition) (2010) (3. Verification of sequential and concurrent programs. Apt_ Olderog (3rd edition) (2010).pdf), страница 12

See Exercise 2.6 for the precise relationship.We also introduce the meaning of an assertion, written as [[p]], and definedby[[p]] = {σ | σ is a proper state and σ |= p}.We say that an assertion p is true, or holds, if for all proper states σ we haveσ |= p, that is, if [[p]] = Σ. Given two assertions p and q, we say that p and qare equivalent if p ↔ q is true.For error states we define ⊥ 6|= p, ∆ 6|= p and fail 6|= p. Thus for allassertions⊥, ∆, fail 6∈ [[p]].The following simple lemma summarizes the relevant properties of the meaning of an assertion.Lemma 2.1.

(Meaning of Assertion)(i) [[¬p]] = Σ − [[p]],(ii) [[p ∨ q]] = [[p]] ∪ [[q]],(iii) [[p ∧ q]] = [[p]] ∩ [[q]],(iv) p → q is true iff [[p]] ⊆ [[q]],(v) p ↔ q is true iff [[p]] = [[q]].⊓⊔Proof. See Exercise 2.7.2.7 SubstitutionTo prove correctness properties about assignment statements, we need theconcept of substitution. A substitution of an expression t for a simple orsubscripted variable u is written as[u := t]2.7 Substitution43and denotes a function from expressions to expressions and from assertionsto assertions. First, we define the application of [u := t] to an expression s,which is written in postfix notation. The result is an expression denoted bys[u := t].A substitution [u := t] describes the replacement of u by t.

For example, wehave• max(x, y)[x := x + 1] ≡ max(x + 1, y).However, substitution is not so easy to define when subscripted variables areinvolved. For example, we obtain• max(a[1], y)[a[1] := 2] ≡ max(2, y),• max(a[x], y)[a[1] := 2] ≡ if x = 1 then max(2, y) else max(a[x], y) fi.In the second case it is checked whether the syntactically different subscriptedvariables a[x] and a[1] are aliases of the same location. Then the substitutionof 2 for a[1] results in a[x] being replaced by 2, otherwise the substitutionhas no effect.

To determine whether a[x] and a[1] are aliases the definitionof substitution makes a case distinction on the subscripts of a (using theconditional expression if x = 1 then . . . else . . . fi).In general, in a given state σ the substituted expression s[u := t] shoulddescribe the same value as the expression s evaluated in the updated stateσ[u := σ(t)], which arises after the assignment u := t has been executed in σ(see Chapter 3). This semantic equivalence is made precise in the SubstitutionLemma 2.4 below.The formal definition of the expression s[u := t] proceeds by induction onthe structure of s:• if s ≡ x for some simple variable x then½t if s ≡ us[u := t] ≡s otherwise,• if s ≡ c for some constant c of basic type thens[u := t] ≡ s,• if s ≡ op(s1 , . .

., sn ) for some constant op of higher type thens[u := t] ≡ op(s1 [u := t], . . ., sn [u := t]),• if s ≡ a[s1 , . . ., sn ] for some array a, and u is a simple variable or a subscripted variable b[t1 , . . ., tm ] where a 6≡ b, thens[u := t] ≡ a[s1 [u := t], . . ., sn [u := t]],442 Preliminaries• if s ≡ a[s1 , . . ., sn ] for some array a and u ≡ a[t1 , .

. ., tn ] thenVns[u := t] ≡ if i=1 si [u := t] = ti then telse a[s1 [u := t], . . ., sn [u := t]] fi,• if s ≡ if B then s1 else s2 fi thens[u := t] ≡ if B[u := t] then s1 [u := t] else s2 [u := t] fi.Note that the definition of substitution does not take into account the infixnotation of binary constants op; so to apply substitution the infix notationmust first be replaced by the corresponding prefix notation.The most complicated case in this inductive definition is the secondclause dealing with subscripted variables, where s ≡ a[s1 , . . ., sn ] and u ≡a[t1 , . . ., tn ].

In that clause the conditional expressionVnif i=1 si [u := t] = ti then . . . else . . . fichecks whether, for any given proper state σ, the expression s ≡ a[s1 , . . ., sn ]in the updated state σ[u := σ(t)] and the expression u ≡ a[t1 , . . ., tn ] inthe state σ are aliases.

For this check the substitution [u := t] needs toapplied inductively to all subscripts s1 , . . ., sn of a[s1 , . . ., sn ]. In case of analias s[u := t] yields t. Otherwise, the substitution is applied inductively tothe subscripts s1 , . . ., sn of a[s1 , . . ., sn ].The following lemma is an immediate consequence of the above definitionof s[u := t].Lemma 2.2. (Identical Substitution) For all expressions s and t, all simple variables x and all subscripted variables a[t1 , .

. ., tn ](i) s[x := t] ≡ s if s does not contain x,(ii) s[a[t1 , . . ., tn ] := t] ≡ s if s does not contain a.⊓⊔The following example illustrates the application of substitution.Example 2.7. Suppose that a and b are arrays of type integer → integerand x is an integer variable. Thena[b[x]][b[1] := 2]≡ {definition of s[u := t] since a 6≡ b}a[b[x][b[1] := 2]]≡ {definition of s[u := t]}a[if x[b[1] := 2] = 1 then 2 else b[x[b[1] := 2]] fi]≡{by the Identical Substitution Lemma 2.2 x[b[1] := 2] ≡ x}a[if x = 1 then 2 else b[x] fi]⊓⊔2.7 Substitution45The application of substitutions [u := t] is now extended to assertions p.The result is again an assertion denoted byp[u := t].The definition of p[u := t] is by induction on the structure on p:• if p ≡ s for some Boolean expression s thenp[u := t] ≡ s[u := t]by the previous definition for expressions,• if p ≡ ¬q thenp[u := t] ≡ ¬(q[u := t]),• if p ≡ q ∨ r thenp[u := t] ≡ q[u := t] ∨ r[u := t],and similarly for the remaining binary connectives: ∧ , → and ↔ ,• if p ≡ ∃x : q thenp[u := t] ≡ ∃y : q[x := y][u := t],where y does not appear in p, t or u and is of the same type as x,• if p ≡ ∀x : q thenp[u := t] ≡ ∀y : q[x := y][u := t],where y does not appear in p, t or u and is of the same type as x.In the clauses dealing with quantification, renaming the bound variable xinto a new variable y avoids possible clashes with free occurrences of x in t.For example, we obtain(∃x : z = 2 · x)[z := x + 1]≡ ∃y : z = 2 · x[x := y][z := x + 1]≡ ∃y : x + 1 = 2 · y.Thus for assertions substitution is defined only up to a renaming of boundvariables.Simultaneous SubstitutionTo prove correctness properties of parallel assignments, we need the conceptof simultaneous substitution.

Let x̄ = x1 , . . . , xn be a list of distinct simple462 Preliminariesvariables of type T1 , . . . , Tn and t̄ = t1 , . . . , tn a corresponding list of expressions of type T1 , . . . , Tn . Then a simultaneous substitution of t̄ for x̄ is writtenas[x̄ := t̄]and denotes a function from expressions to expressions and from assertions toassertions. The application of [x̄ := t̄] to an expression s is written in postfixnotation. The result is an expression denoted bys[x̄ := t̄]and defined inductively over the structure of s. The definition proceeds analogously to that of a substitution for a single simple variable except that inthe base case we now have to select the right elements from the lists x̄ and t̄:• if s ≡ x for some simple variable x then½ti if x ≡ xi for some i ∈ {1, . . . , n}s[x̄ := t̄] ≡s otherwise.As an example of an inductive clause of the definition we state:• if s ≡ op(s1 , .

. ., sn ) for some constant op of higher type thens[x̄ := t̄] ≡ op(s1 [x̄ := t̄], . . ., sn [x̄ := t̄]).Using these inductive clauses the substitution for each variable xi from thelist x̄ is pursued simultaneously. This is illustrated by the following example.Example 2.8. We take s ≡ max(x, y) and calculatemax(x, y)[x, y := y + 1, x + 2]≡{op ≡ max in the inductive clause above}max(x[x, y := y + 1, x + 2], y[x, y := y + 1, x + 2])≡{the base case shown above}max(y + 1, x + 2).Note that a sequential application of two single substitutions yields a differentresult:max(x, y)[x := y + 1][y := x + 2]≡ max(y + 1, y)[y := x + 2])≡ max((x + 2) + 1, x + 2).⊓⊔Note 2.1.

The first clause of the Lemma 2.2 on Identical Substitutions holdsalso, appropriately rephrased, for simultaneous substitutions: for all expressions s2.8 Substitution Lemma47• s[x̄ := t̄] ≡ s if s does not contain any variable xi from the list x̄.⊓⊔The application of simultaneous subsitution to an assertion p is denotedbyp[x̄ := t̄]and defined inductively over the structure of p, as in the case of a substitutionfor a single simple variable.2.8 Substitution LemmaIn this section we connect the notions of substitution and of update introduced in Sections 2.7 and 2.3. We begin by noting the following so-calledcoincidence lemma.Lemma 2.3. (Coincidence) For all expressions s, all assertions p and allproper states σ and τ(i) if σ[var(s)] = τ [var(s)] then σ(s) = τ (s),(ii) if σ[f ree(p)] = τ [f ree(p)] then σ |= p iff τ |= p.⊓⊔Proof.

See Exercise 2.8.Using the Coincidence Lemma we can prove the following lemma which isused in the next chapter when discussing the assignment statement.Lemma 2.4. (Substitution) For all expressions s and t, all assertions p,all simple or subscripted variables u of the same type as t and all proper statesσ,(i) σ(s[u := t]) = σ[u := σ(t)](s),(ii) σ |= p[u := t] iff σ[u := σ(t)] |= p.Clause (i) relates the value of the expression s[u := t] in a state σ to thevalue of the expression s in an updated state, and similarly with (ii).Proof.

(i) The proof proceeds by induction on the structure of s. Supposefirst that s is a simple variable. Then when s ≡ u, we haveσ(s[u := t])= {definition of substitution}σ(t)={definition of update}σ[s := σ(t)](s)={s ≡ u}σ[u := σ(t)](s),482 Preliminariesand when s 6≡ u the same conclusion follows by the Identical SubstitutionLemma 2.2 and the definition of an update.The case when s is a subscripted variable, say s ≡ a[s1 , .

. ., sn ], is slightlymore complicated. When u is a simple variable or u ≡ b[t1 , . . ., tm ] wherea 6≡ b, we haveσ(s[u := t])={definition of substitution}σ(a[s1 [u := t], . . ., sn [u := t]])={definition of semantics}σ(a)(σ(s1 [u := t]), . . ., σ(sn [u := t])){induction hypothesis}σ(a)(σ[u := σ(t)](s1 ), . . ., σ[u := σ(t)](sn ))= {by definition of update, σ[u := σ(t)](a) = σ(a)}=σ[u := σ(t)](a)(σ[u := σ(t)](s1 ), . . ., σ[u := σ(t)](sn ))= {definition of semantics, s ≡ a[s1 , . . ., sn ]}σ[u := σ(t)](s)and when u ≡ a[t1 , .