3. Verification of sequential and concurrent programs. Apt_ Olderog (3rd edition) (2010) (811405), страница 61
Текст из файла (страница 61)
. . . . . . . . . . . . . . . . . . . . . . . . . . .Bibliographic Remarks . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .351352354357360363368370N THE PREVIOUS chapters we have seen that parallel programs introduce nondeterminism: from a given initial state several computationsresulting in different final states may be possible. This nondeterminism isimplicit; that is, there is no explicit programming construct for expressing it.In this chapter we introduce a class of programs that enable an explicitdescription of nondeterminism. This is the class of Dijkstra’s [1975,1976]guarded commands; it represents a simple extension of while programs considered in Chapter 3.
Dijkstra’s guarded commands are also a preparationfor the study of distributed programs in Chapter 11.In Section 10.1 we introduce the syntax and in Section 10.2 the semanticsof the nondeterministic programs. In Section 10.3 we discuss the advantagesof this language.
As we are going to see, nondeterministic program constructshave the advantage that they allow us to avoid a too detailed description oroverspecification of the intended computations.34935010 Nondeterministic ProgramsVerification of nondeterministic programs is considered in Section 10.4;the proof rules are a simple modification of the corresponding rules for whileprograms introduced in Chapter 3. In Section 10.5 we return to an approachoriginated by Dijkstra [1976], and first explained in Section 3.10, allowing usto develop programs together with their correctness proofs.
We extend thisapproach to nondeterministic programs and illustrate it by the case study ofa welfare crook program.Finally, in Section 10.6 we study transformation of parallel programs intonondeterministic programs.10.1 Syntax35110.1 SyntaxWe expand the grammar for while programs by adding for each n ≥ 1 thefollowing production rules:• if command or alternative commandS ::= if B1 → S1 ⊓⊔. . .⊓⊔Bn → Sn fi,• do command or repetitive commandS ::= do B1 → S1 ⊓⊔.
. .⊓⊔Bn → Sn od.These new commands are also written asif ⊓⊔ni=1 Bi → Si fi and do ⊓⊔ni=1 Bi → Si od,respectively. A Boolean expression Bi within S is called a guard and a command Si within S is said to be guarded by Bi . Therefore the construct Bi → Siis called a guarded command.The symbol ¤ represents a nondeterministic choice between guarded commands Bi → Si . More precisely, in the context of an alternative commandif B1 → S1 ⊓⊔. . .⊓⊔Bn → Sn fia guarded command Bi → Si can be chosen only if its guard Bi evaluates totrue; then Si remains to be executed.
If more than one guard Bi evaluatesto true any of the corresponding statements Si may be executed next. Thereis no rule saying which statement should be selected. If all guards evaluateto false, the alternative command will signal a failure. So the alternativecommand is a generalization of the failure statement that we considered inSection 3.7.The selection of guarded commands in the context of a repetitive commanddo B1 → S1 ⊓⊔.
. .⊓⊔Bn → Sn odis performed in a similar way. The difference is that after termination of aselected statement Si the whole command is repeated starting with a newevaluation of the guards Bi . Moreover, contrary to the alternative command,the repetitive command properly terminates when all guards evaluate to false.We call the programs generated by this grammar nondeterministic programs.35210 Nondeterministic Programs10.2 SemanticsAgain we wish to support this intuitive explanation of meaning of nondeterministic programs by a precise operational semantics. First, we expandthe transition system for while programs by the following transition axioms,where σ is a proper state:(xx) < if ⊓⊔ni=1 Bi → Si fi, σ > → < Si , σ >where σ |= Bi and i ∈ {1, .
. . , n},(xxi) < if ⊓⊔ni=1 Bi → Si fi, σ > → < E, fail > where σ |=⊓⊔ni=1(xxii) < doBi → Si od, σ > → < Si ; dowhere σ |= Bi and i ∈ {1, . . . , n},⊓⊔ni=1Vn¬Bi ,Vn¬Bi .i=1Bi → Si od, σ >(xxiii)< do ⊓⊔ni=1 Bi → Si od, σ > → < E, σ > where σ |=i=1Here fail is an exceptional state, originally considered in Section 3.7 in thecontext of the semantics of the failure statement, that represents a runtimedetectable failure or abortion. For a nondeterministic program S a transition< S, σ > → < R, τ >is possible if and only if it is deducible in the extended transition system.Note that as in in Section 3.7 configurations of the form < S, fail > have nosuccessor in the transition relation → .As before, the semantics M[[S]] of nondeterministic programs S is basedon the transition relation → , but it now maps proper initial states intosets possibly containing several final states.
So, as in the case of the failureadmitting programs considered in Section 3.7 we consider the following twosemantics, where σ is a proper state:• partial correctness semantics:M[[S]](σ) = {τ |< S, σ > →∗ < E, τ >},• total correctness semantics:Mtot [[S]](σ) =M[[S]](σ)∪ {⊥ | S can diverge from σ}∪ {fail | S can fail from σ}.10.2 Semantics353Properties of SemanticsHowever, we now admit nondeterminism.
So, in contrast to Section 3.7, boththe partial correctness semantics M[[S]](σ) and the total correctness semantics Mtot [[S]](σ) can yield more than one outcome. But, as with the parallelprograms of Chapters 8 and 9, the nondeterminism is bounded for the classof nondeterministic programs studied in this chapter.Lemma 10.1. (Bounded Nondeterminism) Let S be a nondeterministicprogram and σ a proper state. Then Mtot [[S]](σ) is either finite or it contains⊥.Proof.
For nondeterministic programs S each configuration < S, σ > hasonly finitely many successors in the transition relation → , so we can applyagain König’s Lemma 8.4.⊓⊔Note that the conventional conditionals and loops can be modeled by alternative and repetitive commands.Lemma 10.2. (Correspondence)(i) Mtot [[if B then S1 else S2 fi]] = Mtot [[if B → S1 ¤¬B → S2 fi]],(ii) Mtot [[while B do S od]] = Mtot [[do B → S od]].⊓⊔Therefore, we shall identify from now on:if B then S1 else S2 fi ≡ if B → S1 ¤¬B → S2 fiandwhile B do S od ≡ do B → S od.As in Chapter 3 we can express the semantics of loops by the semanticsof their syntactic approximations.
Let Ω be a nondeterministic program suchthat M[[Ω]](σ) = ∅ holds for all proper states σ. We define by inductionon k ≥ 0 the kth syntactic approximation of a loop do ⊓⊔ni=1 Bi → Si od asfollows:(do ⊓⊔ni=1 Bi → Si od)0(do⊓⊔ni=1k+1Bi → Si od)= Ω,= if ¤ni=1⊔ni=1 Bi → Si od)kVn Bi → Si ; (do ⊓¤ i=1 ¬Bi → skipfi.The above if command has n + 1 guarded commands where the last onemodels the case of termination.Let N stand for M or Mtot .
We extend N to deal with the error states⊥ and fail byM[[S]](⊥) = M[[S]](fail) = ∅35410 Nondeterministic ProgramsandMtot [[S]](⊥) = {⊥} and Mtot [[S]](fail) = {fail}and to deal with sets X ⊆ Σ ∪ {⊥} ∪ {fail} by[N [[S]](X) =N [[S]](σ).σ ∈XThe following lemmata are counterparts of the Input/Output Lemma 3.3and the Change and Access Lemma 3.4, now formulated for nondeterministicprograms.Lemma 10.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)).(iii) N [[(S1 ; S2 ); S3 ]](X) = N [[S1 ; (S2 ; S3 )]](X).(iv) M[[if ⊓⊔ni=1 Bi → Si fi]](X) = ∪ni=1 M[[Si ]](X ∩ [[Bi ]]).(v) if X ⊆ ∪ni=1 [[Bi ]] thenMtot [[if ⊓⊔ni=1 Bi → Si fi]](X) = ∪ni=1 Mtot [[Si ]](X ∩ [[Bi ]]).(vi) M[[do ⊓⊔ni=1 Bi → Si od]] = ∪∞⊔ni=1 Bi → Si od)k ]].k=0 M[[(do ⊓Proof.
See Exercise 10.1.⊓⊔Lemma 10.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 10.2.⊓⊔10.3 Why Are Nondeterministic Programs Useful?Let us discuss the main arguments in favor of Dijkstra’s language for nondeterministic programs.10.3 Why Are Nondeterministic Programs Useful?355SymmetryDijkstra’s “guarded commands” allow us to present Boolean tests in a symmetric manner. This often enhances the clarity of programs.As an example consider the while program that describes the well-knownalgorithm for finding the greatest common divisor (gcd ) of two natural numbers, initially stored in the variables x and y:while x 6= y doif x > y then x := x − y else y := y − x fiod.Using the repetitive command the same algorithm can be written in a morereadable and symmetric way:GCD ≡ do x > y → x := x − y ¤ x < y → y := y − x od.Note that both programs terminate with the gcd stored in the variables xand y.NondeterminismNondeterministic programs allow us to express nondeterminism through theuse of nonexclusive guards.
Surprisingly often, it is both clumsy and unnecessary to specify a sequential algorithm in a deterministic way —the remainingchoices can be resolved in an arbitrary way and need not concern the programmer. As a simple example, consider the problem of computing the maximumof two numbers. Using the conditional statement this can be written asif x ≥ y then max := x else max := y fiSo we broke the tie x = y in ‘favour’ of the variable x. Using the alternativecommand the the maximum can be computed in a more natural, symmetric,way that involves nondeterminism:if x ≥ y → max := x ¤ y ≥ x → max := yfi.Next, the following nondeterministic program computes the largest powersof 2 and 3 that divide a given integer x:twop := 0; threep := 0;do 2 divides x → x := x div 2; twop := twop + 1¤ 3 divides x → x := x div 3; threep := threep + 1od.If 6 divides x, both guards can be chosen.
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
