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

As we shall seein Chapter 3, the update σ[u := σ(t)] describes the values of the variablesafter the assignment u := t has been executed in state σ. Formally, the updateσ[u := d] is again a proper state defined as follows:• if u is a simple variable thenσ[u := d]is the state that agrees with σ except for u where its value is d. Formally,for each simple or array variable v½dif u ≡ v,σ[u := d](v) =σ(v) otherwise.• if u is a subscripted variable, say u ≡ a[t1 , .

. ., tn ], then2.3 Semantics of Expressions37σ[u := d]is the state that agrees with σ except for the variable a where the valueσ(a)(σ(t1 ), . . ., σ(tn )) is changed to d. Formally, for each simple or arrayvariable vσ[u := d](v) = σ(v) if a 6≡ vand otherwise for a and argument values d1 , . . ., dnσ[u := d](a)(d1 , .

. ., dn ) =½dif di = σ(ti ) for i ∈ {1, . . . , n},σ(a)(d1 , . . ., dn ) otherwise.Thus the effect of σ[u := d] is a selected update of the array variable a atthe current values of the argument tuple t1 , . . ., tn .We extend the definition of update to error states by putting ⊥[u := d] = ⊥,∆[u := d] = ∆ and fail[u := d] = fail.Example 2.6. Let x be an integer variable and σ a proper state.(i) Thenσ[x := 1](x) = 1,for any simple variable y 6≡ xσ[x := 1](y) = σ(y),and for any array a of type T1 × . . . × Tn → T and di ∈ DTi for i ∈ {1, . . .

, n},σ[x := 1](a)(d1 , . . ., dn ) = σ(a)(d1 , . . ., dn ).(ii) Let a be an array of type integer → integer. Suppose that σ(x) = 3.Then for all simple variables yσ[a[x + 1] := 2](y) = σ(y),σ[a[x + 1] := 2](a)(4) = 2,for all integers k 6= 4σ[a[x + 1] := 2](a)(k) = σ(a)(k),and for any array variable b of type T1 × . . . × Tn → T different from a anddi ∈ DTi for i ∈ {1, .

. . , n},σ[a[x + 1] := 2](b)(d1 , . . ., dn ) = σ(b)(d1 , . . ., dn ).⊓⊔To define the semantics of parallel assignments, we need the notion ofsimultaneous update of a list of simple variables. Let x̄ = x1 , . . . , xn be a382 Preliminarieslist of distinct simple variables of types T1 , . . . , Tn and d¯ = d1 , . . . , dn acorresponding list of elements of types T1 , . . . , Tn . Then we define for anarbitrary (proper or error) state¯ = σ[x1 := d1 ] . . . [xn := dn ].σ[x̄ := d]Thus we reduce the simultaneous update to a series of simple updates.

Thiscaptures the intended meaning because the variables x1 , . . . , xn are distinct.2.4 Formal Proof SystemsOur main interest here is in verifying programs. To this end we investigate socalled correctness formulas. To show that a given program satisfies a certaincorrectness formula we need proof systems for correctness formulas. However,we need proof systems even before talking about program correctness, namelywhen defining the operational semantics of the programs. Therefore we nowbriefly introduce the concept of a proof system as it is known in logic.A proof system or a calculus P over a set Φ of formulas is a finite set ofaxiom schemes and proof rules. An axiom scheme A is a decidable subset of Φ,that is, A ⊆ Φ.

To describe axiom schemes we use the standard set-theoreticnotation A = { ϕ | where “. . .”} usually written asA:ϕwhere “. . .”.Here ϕ stands for formulas satisfying the decidable applicability condition“. . .” of A. The formulas ϕ of A are called axioms and are considered asgiven facts. Often the axiom scheme is itself called an “axiom” of the proofsystem.With the help of proof rules further facts can be deduced from givenformulas. A proof rule R is a decidable k + 1-ary relation on the setΦ of formulas, that is, R ⊆ Φk+1 . Instead of the set-theoretic notationR = { (ϕ1 , ..., ϕk , ϕ) | where “. .

.”} a proof rule is usually written asR:ϕ1 , . . ., ϕkϕwhere “. . .”.Here ϕ1 , . . ., ϕk and ϕ stand for the formulas satisfying the decidable applicability condition “. . .” of R. Intuitively, such a proof rule says that fromϕ1 , . . ., ϕk the formula ϕ can be deduced if the applicability condition “. . .”holds. The formulas ϕ1 , . . ., ϕk are called the premises and the formula ϕ iscalled the conclusion of the proof rule.A proof of a formula ϕ from a set A of formulas in a proof system P is afinite sequence2.5 Assertions39ϕ1...ϕnof formulas with ϕ = ϕn such that each formula ϕi with i ∈ {1, . .

. , n}• is either an element of the set A or it• is an axiom of P or it• can be obtained by an application of a proof rule R of P , that is, thereare formulas ϕi1 , . . . , ϕik with i1 , . . . , ik < i in the sequence such that(ϕi1 , . . . , ϕik , ϕi ) ∈ R.The formulas in the set A are called assumptions of the proof. A should bea decidable subset of Φ. Thus A can be seen as an additional axiom schemeA ⊆ Φ that is used locally in a particular proof.

Note that the first formulaϕ1 in each proof is either an assumption from the set A or an axiom of P .The length n of the sequence is called the length of the proof.We say that ϕ is provable from A in P if there exists a proof from A in P .In that case we writeA ⊢P ϕ.For a finite set of assumptions, A = {A1 , . .

. , An }, we drop the set bracketsand write A1 , . . . , An ⊢P ϕ instead of {A1 , . . . , An } ⊢P ϕ. If A = ∅ we simplywrite⊢P ϕinstead of ∅ ⊢P . In that case we call the formula ϕ a theorem of the proofsystem P .2.5 AssertionsTo prove properties about program executions we have to be able to describeproperties of states. To this end, we use formulas from predicate logic. In thecontext of program verification these formulas are called assertions becausethey are used to assert that certain conditions are true for states.

Assertionsare usually denoted by letters p, q, r, and are defined, inductively, by thefollowing clauses:• every Boolean expression is an assertion,• if p, q are assertions, then ¬p, (p ∨ q), (p ∧ q), (p → q) and (p ↔ q) are alsoassertions,• if x is a variable and p an assertion, then ∃x : p and ∀x : p are alsoassertions.402 PreliminariesThe symbol ∃ is the existential quantifier and ∀ is the universal quantifier.Thus in contrast to Boolean expressions, quantifiers can occur in assertions.Note that quantifiers are allowed in front of both simple and array variables.As in expressions the brackets ( and ) can be omitted in assertions if noambiguities arise.

To this end we extend the binding order used for expressionsby stipulating that the connectives→ and ↔ ,bind stronger than∃ and ∀.For example, ∃x : p ↔ q ∧ r is interpreted as ∃x : (p ↔ (q ∧ r)). Also, we canalways delete the outer brackets.Further savings on brackets can be achieved by assuming the right associativity for the connectives ∧ , ∨ , → and ↔ , that is to say, by allowingA ∧ (B ∧ C) to be written as A ∧ B ∧ C, and analogously for the remainingbinary connectives.To simplify notation, we also use the following abbreviations:n^piabbreviates p1 ∧ ... ∧ pni=1s ≤ t abbreviates s < t ∨ s = ts ≤ t < u abbreviates s ≤ t ∧ t < us 6= t abbreviates ¬(s = t)∃x, y : p abbreviates ∃x : ∃y : p∀x, y : p abbreviates ∀x : ∃y : p∃x ≤ t : p abbreviates ∃x : (x ≤ t ∧ p)∀x ≤ t : p abbreviates ∀x : (x ≤ t → p)∀x ∈ [s : t] : p abbreviates ∀x : (s ≤ x ≤ t → p)We also use other abbreviations of this form which are obvious.For lists s̄ = s1 , . .

. , sm and t̄ = t1 , . . . , tn of expressions, we writes̄ = t̄if m = n and si = ti holds for i = 1, . . . , n. In particular, we write x̄ = ȳ forlists x̄ and ȳ of simple variables.The same variable can occur several times in a given assertion. For example, the variable y occurs three times inx > 0 ∧ y > 0 ∧ ∃y : x = 2 ∗ y.2.6 Semantics of Assertions41In logic one distinguishes different kinds of occurrences.

By a bound occurrence of a simple variable x in an assertion p we mean an occurrence within asubassertion of p of the form ∃x : r or ∀x : r. By a subassertion of an assertionp we mean a substring of p that is again an assertion. An occurrence of asimple variable in an assertion p is called free if it is not a bound one. In theabove example, the first occurrence of y is free and the other two are bound.By var(p) we denote the set of all simple and array variables that occurin an assertion p. By f ree(p) we denote the set of all free simple and arrayvariables that have a free occurrence (or occur free) in p.2.6 Semantics of AssertionsThe semantics of an assertion p in a structure S is a mappingS[[p]] : Σ → {true, false}that assigns to p a truth value S[[p]](σ) depending on a given proper state σ.Since the structure S is fixed, we abbreviate the standard notation S[[p]](σ)from logic by writing σ |= p instead of S[[p]](σ) = true.When σ |= p holds, we say that σ satisfies p or that p holds in σ or thatσ is a p-state.

This concept is defined by induction on the structure of p. Weput• for Boolean expressions Bσ |= B, iff σ(B) = true,• for negationσ |= ¬p iff not σ |= p (written as σ 6|= p),• for conjunctionσ |= p ∧ q, iff σ |= p and σ |= q,• for disjunctionσ |= p ∨ q, iff σ |= p or σ |= q,• for implicationσ |= p → q, iff σ |= p implies σ |= q,• for equivalenceσ |= (p ↔ q), iff (σ |= p if and only if σ |= q),422 Preliminaries• for the universal quantifier applied to a simple or an array variable v oftype Tσ |= ∀v : p iff τ |= p for all proper states τ with σ = τ mod v ,• for the existential quantifier applied to a simple or an array variable v oftype Tσ |= ∃v : p iff τ |= p for some proper state τ with σ = τ mod v ,By the definition of mod, the states σ and τ agree on all variables except v.For simple variables x we can use updates and determine τ = σ[x := d] for adata value d in DT .