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), страница 13

. ., tn ], we haveσ(s[u := t])=={definition of substitution, s ≡ a[s1 , . . ., sn ], u ≡ a[t1 , . . ., tn ] }Vnσ(if i=1 si [u := t] = ti then t else a[s1 [u := t], . . ., sn [u := t]] fi)½{definition of semantics}σ(t)if σ(si [u := t]) = σ(ti ) for i ∈ {1, . . . , n}σ(a)(σ(s1 [u := t]), . . ., σ(sn [u := t]))otherwise={definition of update, u ≡ a[t1 , . . ., tn ]}σ[u := σ(t)](a)(σ(s1 [u := t]), . . ., σ(sn [u := t]))={induction hypothesis}σ[u := σ(t)](a)(σ[u := σ(t)](s1 ), . .

., σ[u := σ(t)](sn ))={definition of semantics, s ≡ a[s1 , . . ., sn ]}σ[u := σ(t)](s).The remaining cases are straightforward and left to the reader.(ii) The proof also proceeds by induction on the structure of p. The base case,which concerns Boolean expressions, is now implied by (i). The induction stepis straightforward with the exception of the case when p is of the form ∃x : ror ∀x : r. Let y be a simple variable that does not appear in r, t or u and isof the same type as x. We then have2.8 Substitution Lemma49σ |= (∃x : r)[u := t]iff {definition of substitution}σ |= ∃y : r[x := y][u := t]iff {definition of truth}σ ′ |= r[x := y][u := t]for some element d from the type associatedwith y and σ ′ = σ[y := d]iff{induction hypothesis}σ ′ [u := σ ′ (t)] |= r[x := y]for some d and σ ′ as aboveiff {y 6≡ x so σ ′ [u := σ ′ (t)](y) = d,induction hypothesis}σ ′ [u := σ ′ (t)][x := d] |= rfor some d and σ ′ as aboveiff{Coincidence Lemma 2.3, choice of y}σ[u := σ(t)][x := d] |= rfor some d as aboveiff {definition of truth}σ[u := σ(t)] |= ∃x : r.An analogous chain of equivalences deals with the case when p is of theform ∀x : r.

This concludes the proof.⊓⊔Example 2.9. Let a and b be arrays of type integer → integer, x an integervariable and σ a proper state such that σ(x) = 1 and σ(a)(1) = 2. Thenσ[b[1] := 2](a[b[x]])={Substitution Lemma 2.4}σ(a[b[x]][b[1] := 2])={Example 2.7}σ(a[if x = 1 then 2 else b[x] fi])= {Example 2.5}= σ(a[2]).Of course, a direct application of the definition of an update also leads tothis result.⊓⊔Finally, we state the Substitution Lemma for the case of simultaneoussubstitutions.502 PreliminariesLemma 2.5.

(Simultaneous Substitution) Let x̄ = x1 , . . . , xn be a list ofdistinct simple variables of type T1 , . . . , Tn and t̄ = t1 , . . . , tn a correspondinglist of expressions of type x1 , . . . , xn . Then for all expressions s, all assertionsp, and all proper states σ,(i) σ(s[x̄ := t̄]) = σ[x̄ := σ(t̄)](s),(ii) σ |= p[x̄ := t̄] iff σ[x̄ := σ(t̄)] |= p,where σ(t̄) = σ(t1 ), .

. . , σ(tn ).Clause (i) relates the value of the expression s[x̄ := t̄] in a state σ to thevalue of the expression s in an updated state, and similarly with (ii).Proof. Analogously to that of the Substitution Lemma 2.4.⊓⊔2.9 Exercises2.1.

Simplify the following assertions:(i) (p ∨ (q ∨ r)) ∧ (q → (r → p)),(ii) (s < t ∨ s = t) ∧ t < u,(iii) ∃x : (x < t ∧ (p ∧ (q ∧ r))) ∨ s = u.2.2. Compute the following expressions using the definition of substitution:(i) (x + y)[x := z][z := y],(ii) (a[x] + y)[x := z][a[2] := 1],(iii) a[a[2]][a[2] := 2].2.3. Compute the following values:(i) σ[x := 0](a[x]),(ii) σ[y := 0](a[x]),(iii) σ[a[0] := 2](a[x]),(iv) τ [a[x] := τ (x)](a[1]), where τ = σ[x := 1][a[1] := 2].2.4. Prove that(i) p ∧ (q ∧ r) is equivalent to (p ∧ q) ∧ r,(ii) p ∨ (q ∨ r) is equivalent to (p ∨ q) ∨ r,(iii) p ∨ (q ∧ r) is equivalent to (p ∨ q) ∧ (p ∨ r),(iv) p ∧ (q ∨ r) is equivalent to (p ∧ q) ∨ (p ∧ r),(v) ∃x : (p ∨ q) is equivalent to ∃x : p ∨ ∃x : q,(vi) ∀x : (p ∧ q) is equivalent to ∀x : p ∧ ∀x : q.2.10 Bibliographic Remarks512.5.(i)(ii)(iii)(iv)IsIsIsIs∃x : (p ∧ q) equivalent to ∃x : p ∧ ∃x : q?∀x : (p ∨ q) equivalent to ∀x : p ∨ ∀x : q?(∃x : z = x + 1)[z := x + 2] equivalent to ∃y : x + 2 = y + 1?(∃x : a[s] = x + 1)[a[s] := x + 2] equivalent to ∃y : x + 2 = y + 1?2.6.

Show that for a simple variable x of type T updates can be used tocharacterize the semantics of quantifiers:• σ |= ∀x : p iff σ[x := d] |= p for all data values d from DT ,• σ |= ∃x : p iff σ[x := d] |= p for some data value d from DT .2.7. Prove the Meaning of Assertion Lemma 2.1.2.8. Prove the Coincidence Lemma 2.3.2.9.(i) Prove that p[x := 1][y := 2] is equivalent to p[y := 2][x := 1], where xand y are distinct variables.Hint. Use the Substitution Lemma 2.4.(ii) Give an example when the assertions p[x := s][y := t] and p[y := t][x :=s] are not equivalent.2.10.(i) Prove that p[a[1] := 1][a[2] := 2] is equivalent to p[a[2] := 2][a[1] := 1].Hint.

Use the Substitution Lemma 2.4.(ii) Give an example when the assertions p[a[s1 ] := t1 ][a[s2 ] := t2 ] andp[a[s2 ] := t2 ][a[s1 ] := t1 ] are not equivalent.2.11. Prove Lemma 2.5 on Simultaneous Substitution.2.10 Bibliographic RemarksOur use of types is very limited in that no subtypes are allowed and highertypes can be constructed only directly out of the basic types. A more extendeduse of types in mathematical logic is discussed in Girard, Lafont and Taylor[1989], and of types in programming languages in Cardelli [1991] and Mitchell[1990].For simplicity all functions and relations used in this book are assumed tobe totally defined. A theory of program verification in the presence of partiallydefined functions and relations is developed in the book by Tucker and Zucker[1988].

In Chapter 3 of this book we explain how we can nevertheless modelpartially defined expressions by the programming concept of failure.522 PreliminariesOur definition of substitution for a simple variable is the standard oneused in mathematical logic. The definitions of substitution for a subscriptedvariable, of a state, and of an update of a state are taken from de Bakker[1980], where the Substitution Lemma 2.4 also implicitly appears.To the reader interested in a more thorough introduction to the basicconcepts of mathematical logic we recommend the book by van Dalen [2004].Part IIDeterministic Programs3 while Programs3.13.23.33.43.53.63.73.83.93.103.113.123.13ISyntax .

. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .Semantics . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .Verification . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .Proof Outlines . . . . . . . . . . . .

. . . . . . . . . . . . . . . . . . . . . . . . . .Completeness . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .Parallel Assignment . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .Failure Statement . . .

. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .Auxiliary Axioms and Rules . . . . . . . . . . . . . . . . . . . . . . . . .Case Study: Partitioning an Array . . . . . . . . . . . . . . . . . . . .Systematic Development of Correct Programs . . .

. . . . . .Case Study: Minimum-Sum Section Problem . . . . . . . . . .Exercises . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .Bibliographic Remarks . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .575863798591949799113116121124N A DETERMINISTIC program there is at most one instruction to beexecuted “next,” so that from a given initial state only one executionsequence is generated.

In classical programming languages like Pascal, onlydeterministic programs can be written. In this chapter we study a small classof deterministic programs, called while programs, which are included in allother classes of programs studied in this book.We start by defining the syntax (Section 3.1), then introduce an operational semantics (Section 3.2), subsequently study program verification byintroducing proof systems allowing us to prove various program propertiesand prove the soundness of the introduced proof systems (Section 3.3). This55563 while Programspattern is repeated for all classes of programs studied in this book.

We introduce here two semantics —partial correctness and total correctness semantics.The former does not take into account the possibility of divergence while thelatter does.The proof theory deals with correctness formulas. These formulas havethe form {p} S {q} where p and q are assertions and S is a program. Weintroduce here two proof systems —one for proving the correctness formulasin the sense of partial correctness and the other for proving them in thesense of total correctness. Then we prove their soundness with respect to theunderlying semantics.Next, in Section 3.4, we introduce a convenient proof presentation, called aproof outline, that allows us to present correctness proofs by giving a programinterleaved with assertions at appropriate places.