3. Verification of sequential and concurrent programs. Apt_ Olderog (3rd edition) (2010) (811405), страница 19
Текст из файла (страница 19)
Let S be a while program and Φ a set of proper states.We definewlp(S, Φ) = {σ | M[[S]](σ) ⊆ Φ}andwp(S, Φ) = {σ | Mtot [[S]](σ) ⊆ Φ}.We call wlp(S, Φ) the weakest liberal precondition of S with respect to Φ andwp(S, Φ) the weakest precondition of S with respect to Φ.⊓⊔Informally, wlp(S, Φ) is the set of all proper states σ such that wheneverS is activated in σ and properly terminates, the output state is in Φ. In turn,wp(S, Φ) is the set of all proper states σ such that whenever S is activatedin σ, it is guaranteed to terminate and the output state is in Φ.It can be shown that these sets of states can be expressed or defined byassertions in the following sense.3.5 Completeness87Definition 3.11.
An assertion p defines a set Φ of states if the equation[[p]] = Φ holds.⊓⊔Theorem 3.4. (Definability) Let S be a while program and q an assertion. Then the following holds.(i) There is an assertion p defining wlp(S, [[q]]), i.e. with [[p]] = wlp(S, [[q]]).(ii) There is an assertion p defining wp(S, [[q]]), i.e. with [[p]] = wp(S, [[q]]).Proof.
A proof of this theorem for a similar assertion language can be foundin Appendix B of de Bakker [1980] (written by J. Zucker). We omit the proofdetails and mention only that its proof uses the technique of Gödelization,which allows us to code computations of programs by natural numbers in aneffective way. Such an encoding is possible due to the fact that the assertionlanguage includes addition and multiplication of natural numbers.⊓⊔By the Definability Theorem 3.4 we can express weakest preconditions syntactically. Hence we adopt the following convention: for a givenwhile program S and a given assertion q we denote by wlp(S, q) some assertion p for which the equation in (i) holds, and by wp(S, q) some assertionp for which the equation in (ii) holds.
Note the difference between wlp(S, q)and wlp(S, Φ). The former is an assertion whereas the latter is a set of states;similarly with wp(S, q) and wp(S, Φ). Note that wlp(S, q) and wp(S, q) aredetermined only up to logical equivalence.The following properties of weakest preconditions can easily be established.Lemma 3.5. (Weakest Liberal Precondition) The following statementshold for all while programs and assertions:(i) wlp(skip, q) ↔ q,(ii) wlp(u := t, q) ↔ q[u := t],(iii) wlp(S1 ; S2 , q) ↔ wlp(S1 , wlp(S2 , q)),(iv) wlp(if B then S1 else S2 fi, q) ↔(B ∧ wlp(S1 , q)) ∨ (¬B ∧ wlp(S2 , q)),(v) wlp(S, q) ∧ B → wlp(S1 , wlp(S, q)),where S ≡ while B do S1 od,(vi) wlp(S, q) ∧ ¬B → q,where S ≡ while B do S1 od,(vii) |= {p} S {q} iff p → wlp(S, q).Proof. See Exercise 3.15.⊓⊔Note that for a given loop S ≡ while B do S1 od the clauses (v) and(vii) imply|= {wlp(S, q) ∧ B} S1 {wlp(S, q)}.In other words, wlp(S, q) is a loop invariant of S.883 while ProgramsLemma 3.6.
(Weakest Precondition) The statements (i)–(vii) of theWeakest Liberal Precondition Lemma 3.5 hold when wlp is replaced by wpand |= by |=tot .⊓⊔Proof. See Exercise 3.16.Using the definability of the weakest precondition as stated in the Definability Theorem 3.4 we can show the completeness of the proof system PW.For the completeness of TW, however, we need the additional property thatalso all bound functions can be expressed by suitable integer expressions.Definition 3.12.
For a loop S ≡ while B do S1 od and an integer variablex not occurring in S consider the extended loopSx ≡ x := 0; while B do x := x + 1; S1 odand a proper state σ such that the computation of S starting in σ terminates,that is, Mtot [[S]](σ) 6= {⊥}. Then Mtot [[Sx ]](σ) = {τ } for some proper stateτ 6= ⊥. By iter(S, σ) we denote the value τ (x), which is a natural number. ⊓⊔Intuitively, iter(S, σ) is the number of iterations of the loop S occurring inthe computation of S starting in σ. For a fixed loop S we can view iter(S, σ) asa partially defined function in σ that is defined whenever Mtot [[S]](σ) 6= {⊥}holds.
Note that this function is computable. Indeed, the extended loop Sxcan be simulated by a Turing machine using a counter x for counting thenumber of loop iterations.Definition 3.13. The set of all integer expressions is called expressive if forevery while loop S there exists an integer expression t such thatσ(t) = iter(S, σ)holds for every state σ with Mtot [[S]](σ) 6= {⊥}.⊓⊔Thus expressibility means that for each loop the number of loop iterationscan be expressed by an integer expression. Whereas the assertions introducedin Chapter 2 are powerful enough to guarantee the definability of the weakestpreconditions (the Definability Theorem 3.4), the integer expressions introduced there are too weak to guarantee expressibility.Using the function symbols + and · for addition and multiplication, we canrepresent only polynomials as integer expressions.
However, it is easy to writea terminating while loop S where the number of loop iterations exhibit anexponential growth, say according to the function iter(S, σ) = 2σ (x) . Theniter(S, σ) cannot be expressed using the integer expressions of Chapter 2.To guarantee expressibility we need an extension of the set of integer expressions which allows us to express all partially defined computable functionsand thus in particular iter(S, σ).
We omit the details of such an extension.3.5 Completeness89We can now prove the desired theorem.Theorem 3.5. (Completeness)(i) The proof system PW is complete for partial correctness ofwhile programs.(ii) Assume that the set of all integer expressions is expressive. Then theproof system TW is complete for total correctness of while programs.Proof.(i) Partial correctness. We first prove that for all S and q,⊢PW {wlp(S, q)} S {q}.(3.26)We proceed by induction on the structure of S. To this end we use clauses(i)–(vi) of the Weakest Liberal Precondition Lemma 3.5.Induction basis. The cases of the skip statement and the assignment arestraightforward.Induction step. The case of sequential composition is easy.
We consider in more detail the case of the conditional statement S ≡if B then S1 else S2 fi. We have by the Weakest Liberal PreconditionLemma 3.5(iv)wlp(S, q) ∧ B → wlp(S1 , q)(3.27)andwlp(S, q) ∧ ¬B → wlp(S2 , q).(3.28)By the induction hypothesis,⊢PW {wlp(S1 , q)} S1 {q}(3.29)⊢PW {wlp(S2 , q)} S2 {q}.(3.30)andUsing now the consequence rule applied respectively to (3.27) and (3.29), and(3.28) and (3.30), we obtain⊢PW {wlp(S, q) ∧ B} S1 {q}and⊢PW {wlp(S, q) ∧ ¬B} S2 {q},from which (3.26) follows by the conditional rule.Finally, consider a loop S ≡ while B do S1 od. We have by the inductionhypothesis⊢PW {wlp(S1 , wlp(S, q))} S1 {wlp(S, q)}.By the Weakest Liberal Precondition Lemma 3.5(v) and the consequence rule⊢PW {wlp(S, q) ∧ B} S1 {wlp(S, q)};903 while Programsso by the loop rule⊢PW {wlp(S, q)} S {wlp(S, q) ∧ ¬B}.Finally, by the Weakest Liberal Precondition Lemma 3.5(vi) and the consequence rule⊢PW {wlp(S, q)} S {q}.This proves (3.26).
With this preparation we can now prove the completenessof PW. Suppose|= {p} S {q}.Then by the Weakest Liberal Precondition Lemma 3.5(vii)p → wlp(S, q);so by (3.26) and the consequence rule⊢PW {p} S {q}.(ii) Total correctness.We proceed somewhat differently than in (i) and provedirectly by induction on the structure of S that|=tot {p} S1 {q} implies ⊢TW {p} S1 {q}.The proof of the cases skip, assignment, sequential composition and conditional statement is similar to that of (i) but uses the Weakest PreconditionLemma 3.6 instead of the Weakest Liberal Precondition Lemma 3.5.The main difference lies in the treatment of the loop S ≡while B do S1 od. Suppose |=tot {p} S {q}.
It suffices to prove⊢TW {wp(S, q)} S {q}(3.31)because —similar to (i) and using the Weakest Precondition Lemma 3.6(vii)and the consequence rule— this implies ⊢TW {p} S1 {q} as desired. By theWeakest Precondition Lemma 3.6(vii)|=tot {wp(S1 , wp(S, q))} S1 {wp(S, q)};so by the induction hypothesis⊢TW {wp(S1 , wp(S, q))} S1 {wp(S, q)}.Thus by the Weakest Precondition Lemma 3.6(v)⊢TW {wp(S, q) ∧ B} S1 {wp(S, q)}.(3.32)We intend now to apply the loop II rule.
In (3.32) we have already founda loop invariant, namely wp(S, q), but we also need an appropriate bound3.6 Parallel Assignment91function. By the assumption about the expressiveness of the set of all integerexpressions there exists an integer expression t such that σ(t) = iter(S, σ)for all proper states σ with M[[S]](σ) 6= {⊥}.
By the definition of wp(S, q)and t,|=tot {wp(S, q) ∧ B ∧ t = z} S1 {t < z},(3.33)where z is an integer variable that does not occur in t, B and S, andwp(S, q) → t ≥ 0.(3.34)By the induction hypothesis (3.33) implies⊢TW {wp(S, q) ∧ B ∧ t = z} S1 {t < z}.(3.35)Applying the loop II rule to (3.32), (3.35) and (3.34) yields⊢TW {wp(S, q)} S {wp(S, q) ∧ ¬B}.(3.36)Now (3.31) follows from (3.36) by the Weakest Precondition Lemma 3.6(vi)and the consequence rule.⊓⊔Similar completeness results can be established for various other proofsystems considered in subsequent chapters. All these proofs proceed by induction on the structure of the programs and use intermediate assertionsconstructed by means of the weakest (liberal) precondition or similar semantics concepts.
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
