3. Verification of sequential and concurrent programs. Apt_ Olderog (3rd edition) (2010) (811405), страница 15
Текст из файла (страница 15)
We now define two input/output semantics for while programs. Each of them associates with a program S and a proper state σ ∈ Σa set of output states.(i) The partial correctness semantics is a mappingM[[S]] : Σ → P(Σ)withM[[S]](σ) = {τ |< S, σ > →∗ < E, τ >}.(ii) The total correctness semantics is a mappingMtot [[S]] : Σ → P(Σ ∪ {⊥})3.2 Semantics61withMtot [[S]](σ) = M[[S]](σ) ∪ {⊥ | S can diverge from σ}.⊓⊔The reason for this choice of names becomes clear in the next section. Thedifference between these semantics lies in the way the ‘negative’ informationabout the program is dealt with —either it is dropped or it is explicitly mentioned: M[[S]](σ) consists of proper states, whereas Mtot [[S]](σ) may contain⊥. Thus the negative information consists here of the possibility of divergence.Observe that, by the Determinism Lemma 3.1, M[[S]](σ) has at most oneelement and Mtot [[S]](σ) has exactly one element.Let us consider an example to clarify the above concepts.Example 3.1.
Consider the programS ≡ a[0] := 1; a[1] := 0; while a[x] 6= 0 do x := x + 1 odand let σ be a proper state in which x is 0.According to the Determinism Lemma 3.1 there is exactly one computationof S starting in σ. It has the following form, where σ ′ stands for σ[a[0] :=1][a[1] := 0], which is the iterated update of σ:< S, σ >→ < a[1] := 0; while a[x] 6= 0 do x := x + 1 od, σ[a[0] := 1] >→ < while a[x] 6= 0 do x := x + 1 od, σ ′ >→ < x := x + 1; while a[x] 6= 0 do x := x + 1 od, σ ′ >→ < while a[x] 6= 0 do x := x + 1 od, σ ′ [x := 1] >→ < E, σ ′ [x := 1] > .Thus S when activated in σ terminates in five steps.
We haveM[[S]](σ) = Mtot [[S]](σ) = {σ ′ [x := 1]}.Now let τ be a state in which x is 2 and for i = 2, 3, . . ., a[i] is 1. Thecomputation of S starting in τ has the following form where τ ′ stands forτ [a[0] := 1][a[1] := 0]:623 while Programs< S, τ >→ < a[1] := 0; while a[x] 6= 0 do x := x + 1 od, τ [a[0] := 1] >→ < while a[x] 6= 0 do x := x + 1 od, τ ′ >→ < x := x + 1; while a[x] 6= 0 do x := x + 1 od, τ ′ >→ < while a[x] 6= 0 do x := x + 1 od, τ ′ [x := τ (x) + 1] >...→ < while a[x] 6= 0 do x := x + 1 od, τ ′ [x := τ (x) + k] >...Thus S can diverge from τ . We have M[[S]](τ ) = ∅ and Mtot [[S]](τ ) = {⊥}.⊓⊔This example shows that the transition relation → indeed formalizes theintuitive idea of a computation.Properties of SemanticsThe semantics M and Mtot satisfy several simple properties that we usein the sequel.
Let Ω be a while program such that for all proper states σ,M[[Ω]](σ) = ∅; for example, Ω ≡ while true do skip od. Define by induction on k ≥ 0 the following sequence of while programs:(while B do S od)0 = Ω,(while B do S od)k+1 = if B then S; (while B do S od)kelse skip fi.In the following let N stand for M or Mtot . We extend N to deal with theerror state ⊥ byM[[S]](⊥) = ∅ and Mtot [[S]](⊥) = {⊥}and to deal with sets of states X ⊆ Σ ∪ {⊥} by[N [[S]](X) =N [[S]](σ).σ ∈XThe following lemmata collect the properties of M and Mtot we need.Lemma 3.3.
(Input/Output)(i) N [[S]] is monotonic; that is, X ⊆ Y ⊆ Σ ∪ {⊥} impliesN [[S]](X) ⊆ N [[S]](Y ).(ii) N [[S1 ; S2 ]](X) = N [[S2 ]](N [[S1 ]](X)).3.3 Verification63(iii) N [[(S1 ; S2 ); S3 ]](X) = N [[S1 ; (S2 ; S3 )]](X).(iv) N [[if B then S1 else S2 fi]](X) =N [[S1 ]](X ∩ [[B]]) ∪ N [[S2 ]](X ∩ [[¬B]]) ∪ {⊥ | ⊥ ∈ X and N = Mtot }.S∞(v) M[[while B do S od]](X) = k=0 M[[(while B do S od)k ]](X).Proof. See Exercise 3.1.⊓⊔Clause (iii) of the above lemma states that two possible parsings of an ambiguous statement S1 ; S2 ; S3 yield programs with the same semantics.
Thisjustifies our previous remark in Section 3.1 that the sequential compositionis associative.Note that clause (v) fails for the case of Mtot semantics. The reasonis that for allS∞proper states σ we have Mtot [[Ω]](σ) = {⊥} and consequently ⊥ ∈ k=0 Mtot [[(while B do S od)k ]](σ) holds for every programwhile B do S od. On the other hand for some programs while B do S odand proper states σ we have ⊥ 6∈ Mtot [[while B do S od]](σ).Lemma 3.4. (Change and Access)(i) For all proper states σ and τ , τ ∈ N [[S]](σ) impliesτ [V ar − change(S)] = σ[V ar − change(S)].(ii) For all proper states σ and τ , σ[var(S)] = τ [var(S)] impliesN [[S]](σ) = N [[S]](τ ) mod Var − var(S).⊓⊔Proof.
See Exercise 3.2.Recall that Var stands for the set of all simple and array variables. Part(i) of the Change and Access Lemma states that every program S changesat most the variables in change(S), while part (ii) states that every programS accesses at most the variables in var(S). This explains the name of thislemma. It is used often in the sequel.3.3 VerificationInformally, a while program is correct if it satisfies the intended input/outputrelation. Program correctness is expressed by so-called correctness formulas.These are statements of the form{p} S {q}where S is a while program and p and q are assertions.
The assertion p isthe precondition of the correctness formula and q is the postcondition. The643 while Programsprecondition describes the set of initial or input states in which the program Sis started and the postcondition describes the set of desirable final or outputstates.More precisely, we are interested here in two interpretations: a correctnessformula {p} S {q} is true in the sense of partial correctness if every terminating computation of S that starts in a state satisfying p terminates in astate satisfying q.
And {p} S {q} is true in the sense of total correctness ifevery computation of S that starts in a state satisfying p terminates andits final state satisfies q. Thus in the case of partial correctness, divergingcomputations of S are not taken into account.Using the semantics M and Mtot , we formalize these interpretations uniformly as set theoretic inclusions.Definition 3.3.(i) We say that the correctness formula {p} S {q} is true in the sense ofpartial correctness, and write |= {p} S {q}, ifM[[S]]([[p]]) ⊆ [[q]].(ii) We say that the correctness formula {p} S {q} is true in the sense oftotal correctness, and write |=tot {p} S {q}, if⊓⊔Mtot [[S]]([[p]]) ⊆ [[q]].In other words, since by definition ⊥ 6∈ [[q]], part (ii) indeed formalizesthe above intuition about total correctness.
Since for all proper states σM[[S]](σ) ⊆ Mtot [[S]](σ) holds, |=tot {p} S {q} implies |= {p} S {q}.The uniform pattern of definitions in (i) and (ii) is followed for all semanticsdefined in the book. We can say that each semantics fixes the correspondingcorrectness notion in a standard manner.Example 3.2. Consider once more the programS ≡ a[0] := 1; a[1] := 0; while a[x] 6= 0 do x := x + 1 odfrom Example 3.1. The two computations of S exhibited there show that thecorrectness formulas{x = 0} S {a[0] = 1 ∧ a[1] = 0}and{x = 0} S {x = 1 ∧ a[x] = 0}are true in the sense of total correctness, while{x = 2} S {true}is false.
Indeed, the state τ of Example 3.1 satisfies the precondition x = 2but Mtot [[S]](τ ) = {⊥}.3.3 Verification65Clearly, all three formulas are true in the sense of partial correctness. Also{x = 2 ∧ ∀i ≥ 2 : a[i] = 1} S {false}is true in the sense of partial correctness. This correctness formula states thatevery computation of S that begins in a state which satisfies x = 2 ∧ ∀i ≥2 : a[i] = 1, diverges. Namely, if there existed a finite computation, its finalstate would satisfy false which is impossible.⊓⊔Partial CorrectnessAs we have seen in Examples 3.1 and 3.2, reasoning about correctness formulas in terms of semantics is not very convenient.
A much more promisingapproach is to reason directly on the level of correctness formulas. FollowingHoare [1969], we now introduce a proof system, called PW, allowing us toprove partial correctness of while programs in a syntax-directed manner, byinduction on the program syntax.PROOF SYSTEM PW :This system consists of the groupof axioms and rules 1–6.AXIOM 1: SKIP{p} skip {p}AXIOM 2: ASSIGNMENT{p[u := t]} u := t {p}RULE 3: COMPOSITION{p} S1 {r}, {r} S2 {q}{p} S1 ; S2 {q}RULE 4: CONDITIONAL{p ∧ B} S1 {q}, {p ∧ ¬B} S2 {q}{p} if B then S1 else S2 fi {q}RULE 5: LOOP{p ∧ B} S {p}{p} while B do S od {p ∧ ¬B}663 while ProgramsRULE 6: CONSEQUENCEp → p1 , {p1 } S {q1 }, q1 → q{p} S {q}We augment each proof system for correctness formulas, in particular PW,by the set of all true assertions.
These assertions are used as premises in theconsequence rule which is part of all proof systems considered in this book.Using the notation of Section 2.4 we write ⊢PW {p} S {q} for provability ofthe correctness formula {p} S {q} in the augmented system PW.Let us now discuss the above axioms and proof rules. The skip axiomshould be obvious. On the other hand, the first reaction to the assignmentaxiom is usually astonishment. The axiom encourages reading the assignment“backwards”; that is, we start from a given postcondition p and determinethe corresponding precondition p[u := t] by backward substitution. We soonillustrate the use of this axiom by means of an example.Easy to understand are the composition rule where we have to find anappropriate intermediate assertion r and the conditional rule which formalizesa case distinction according to the truth value of B.Less apparent is the loop rule.
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
