3. Verification of sequential and concurrent programs. Apt_ Olderog (3rd edition) (2010) (811405), страница 18
Текст из файла (страница 18)
A formation ruleϕ1 , . . ., ϕkϕk+1should be read as a statement: if ϕ1 , . . ., ϕk are proof outlines, then ϕk+1 isa proof outline.(i) {p} skip {p}(ii) {p[u := t]} u := t {p}(iii)(iv)(v)(vi)(vii){p} S1∗ {r}, {r} S2∗ {q}{p} S1∗ ; {r} S2∗ {q}{p ∧ B} S1∗ {q}, {p ∧ ¬B} S2∗ {q}{p} if B then {p ∧ B} S1∗ {q} else {p ∧ ¬B} S2∗ {q} fi {q}{p ∧ B} S ∗ {p}{inv : p} while B do {p ∧ B} S ∗ {p} od {p ∧ ¬B}p → p1 , {p1 } S ∗ {q1 }, q1 → q{p}{p1 } S ∗ {q1 }{q}{p} S ∗ {q}{p} S ∗∗ {q}where S ∗∗ results from S ∗ by omitting some annotations of the form{r}. Thus all annotations of the form {inv : r} remain.A proof outline {p} S ∗ {q} for partial correctness is called standard if everysubprogram T of S is preceded by exactly one assertion in S ∗ , called pre(T ),and there are no other assertions in S ∗ .⊓⊔3.4 Proof Outlines81Thus, in a proof outline, some of the intermediate assertions used in thecorrectness proof are retained and loop invariants are always retained.
Notethat every standard proof outline {p} S ∗ {q} for partial correctness startswith exactly two assertions, namely p and pre(S). If p ≡ pre(S), then wedrop p from this proof outline and consider the resulting proof outline alsoto be standard.Note that a standard proof outline is not minimal, in the sense that someassertions used in it can be removed. For example, the assertion {p ∧ B} inthe context {inv : p} while B do {p ∧ B} S od {q} can be deduced. Standard proof outlines are needed in the chapters on parallel programs.By studying proofs of partial correctness in the form of standard proofoutlines we do not lose any generality, as the following theorem shows.
Recallthat ⊢itP W stands for provability in the system PW augmented by the set ofall true assertions.Theorem 3.2.(i) Let {p} S ∗ {q} be a proof outline for partial correctness. Then ⊢itP W{p} S {q}.(ii) If ⊢itP W {p} S {q}, there exists a standard proof outline for partialcorrectness of the form {p} S ∗ {q}.Proof. (i) Straightforward by induction on the structure of the programs.For example, if {p} S1∗ ; S2∗ {q} is a proof outline then for some r both{p} S1∗ {r} and {r} S2∗ {q} are proof outlines. By the induction hypothesis ⊢PW {p} S1 {r} and ⊢PW {r} S2 {q}; so ⊢PW {p} S1 ; S2 {q} by thecomposition rule.
Other cases are equally simple to prove.(ii) Straightforward by induction on the length of the proof. For example, ifthe last rule applied in the proof of {p} S {q} was the conditional rule, thenby the induction hypothesis there are standard proof outlines for partialcorrectness of the forms {p ∧ B} S1∗ {q} and {p ∧ ¬B} S2∗ {q}, where S isif B then S1 else S2 fi. Thus there exists a standard proof outline of theform {p} S ∗ {q}. Other cases are equally simple to prove.⊓⊔Also, the proof outlines {p} S ∗ {q} enjoy the following useful and intuitiveproperty: whenever the control of S in a given computation starting in a statesatisfying p reaches a point annotated by an assertion, this assertion is true.Thus the assertions of a proof outline are true at the appropriate moments.To state this property we have to abstract from the operational semanticsthe notion of program control.
To this end we introduce the notation at(T, S).Informally, at(T, S) is the remainder of S that is to be executed when thecontrol is at subprogram T . For example, forS ≡ while x ≥ 0 do if y ≥ 0 then x := x − 1 else y := y − 2 fi od,and823 while ProgramsT ≡ y := y − 2,the following should hold: at(T, S) ≡ at(y := y−2, S) ≡ y := y−2; S becauseonce T has terminated, loop S must be reiterated.More precisely, we introduce the following definition.Definition 3.7.
Let T be a subprogram of S. We define a program at(T, S)by the following clauses:(i) if S ≡ S1 ; S2 and T is a subprogram of S1 , then at(T, S) ≡ at(T, S1 );S2 and if T is a subprogram of S2 then at(T, S) ≡ at(T, S2 );(ii) if S ≡ if B then S1 else S2 fi and T is a subprogram of Si , thenat(T, S) ≡ at(T, Si ) (i = 1, 2);(iii) if S ≡ while B do S ′ od and T is a subprogram of S ′ , then at(T, S)≡ at(T, S ′ ); S;(iv) if T ≡ S then at(T, S) ≡ S.⊓⊔We can now state the desired theorem.Theorem 3.3.
(Strong Soundness) Let {p} S ∗ {q} be a standard proofoutline for partial correctness. Suppose that< S, σ > →∗ < R, τ >for some state σ satisfying p, program R and state τ . Then• if R ≡ at(T, S) for a subprogram T of S, then τ |= pre(T ),• if R ≡ E then τ |= q.Proof. It is easy to prove that either R ≡ at(T, S) for a subprogram T ofS or R ≡ E (see Exercise 3.13).
In the first case, let r stand for pre(T ); inthe second case, let r stand for q. We need to show τ |= r. The proof is byinduction on the length of the computation. If its length is 0 then p → r andσ = τ ; so τ |= r since σ |= p.Suppose now the length is positive. Then for some R′ and τ ′< S, σ > →∗ < R′ , τ ′ > → < R, τ > .We have now to consider six cases depending on the form of the last transition.We consider only two representative ones.(a) Suppose the last transition consists of a successful evaluation of a Booleanexpression B in a conditional statement if B then S1 else S2 fi. Then R′ ≡at(T ′ , S) where T ′ ≡ if B then S1 else S2 fi and R ≡ at(T, S) where T ≡S1 .
By the definition of a proof outlinepre(T ′ ) ∧ B → r.3.4 Proof Outlines83By the induction hypothesis τ ′ |= pre(T ′ ). But by the assumption τ ′ |= Band τ = τ ′ ; so τ |= pre(T ′ ) ∧ B and consequently τ |= r.(b) Suppose the last transition consists of an execution of an assignmentstatement, say u := t. Then R′ ≡ at(u := t, S). By the definition of a proofoutline pre(u := t) → p′ [u := t] and p′ → r for some assertion p′ . Thuspre(u := t) → r[u := t].But by the induction hypothesis τ ′ |= pre(u := t); so τ ′ |= r[u := t].
Also,M[[u := t]](τ ′ ) = {τ }; so by the truth of the assignment axiom in the senseof partial correctness, τ |= r.⊓⊔Total CorrectnessSo far we have only discussed proof outlines for partial correctness. To complete the picture we should take care of the termination of loops. We introducethe following definition.Definition 3.8. (Proof Outline: Total Correctness) Let S ∗ and S ∗∗stand for program S annotated with assertions, some of them labeled bythe keyword inv, and integer expressions, all labeled by the keyword bd.The notion of a proof outline for total correctness is defined as for partialcorrectness (cf.
Definition 3.6), except for formation rule (v) dealing withloops, which is to be replaced by(viii){p ∧ B} S ∗ {p},{p ∧ B ∧ t = z} S ∗∗ {t < z},p→t≥0{inv : p}{bd : t} while B do {p ∧ B} S ∗ {p} od {p ∧ ¬B}where t is an integer expression and z is an integer variable not occurring inp, t, B or S ∗∗ .Standard proof outlines {p} S ∗ {q} for total correctness are defined as forpartial correctness.⊓⊔The annotation {bd : t} represents the bound function of the loopwhile B do S od.
Observe that we do not record in the proof outline the termination proof, that is, the proof of the formula {p ∧ B ∧ t = z} S {t < z}.Usually this proof is straightforward and to reconstruct it, exhibiting the843 while Programsbound function is sufficient. By formation rule (vii) of Definition 3.6 no annotation of the form {inv : p} or {bd : t} may be deleted from a proof outlinefor total correctness.Example 3.7. The following is a proof outline for total correctness of theinteger division program DIV studied in Example 3.4:{x ≥ 0 ∧ y > 0}quo := 0; rem := x;{inv : p′ }{bd : rem}while rem ≥ y do{p′ ∧ rem ≥ y}rem := rem − y; quo := quo + 1{p′ }od{p′ ∧ rem < y}{quo · y + rem = x ∧ 0 ≤ rem < y},wherep′ ≡ quo · y + rem = x ∧ rem ≥ 0 ∧ y > 0.This proof outline represents the proof given in Example 3.4.
It includesthe bound function rem, but it does not include the verification of the lasttwo premises of the loop II rule corresponding to the correctness formulas(3.13) and (3.14) in Example 3.5.We now apply the decomposition rule A1 to DIV and split the proof oftotal correctness into a proof of partial correctness and a proof of termination.To prove{x ≥ 0 ∧ y > 0} DIV {quo · y + rem = x ∧ 0 ≤ rem < y}(3.24)in the sense of partial correctness, let{x ≥ 0 ∧ y ≥ 0} DIV ∗ {quo · y + rem = x ∧ 0 ≤ rem < y}denote the proof outline shown in Example 3.6. We strengthen the precondition by an initial application of the consequence rule, yielding the proofoutline{x ≥ 0 ∧ y > 0}{x ≥ 0 ∧ y ≥ 0}DIV ∗{quo · y + rem = x ∧ 0 ≤ rem < y},which proves (3.24) in the sense of partial correctness.
To show terminationwe prove3.5 Completeness85{x ≥ 0 ∧ y > 0} DIV {true}(3.25)in the sense of total correctness by the following proof outline with a simplerloop invariant than p′ :{x ≥ 0 ∧ y > 0}quo := 0; rem := x;{inv : rem ≥ 0 ∧ y > 0}{bd : rem}while rem ≥ y do{rem ≥ 0 ∧ y > 0 ∧ rem ≥ y}rem := rem − y; quo := quo + 1{rem ≥ 0 ∧ y > 0}od{true}.Together, (3.24) and (3.25) establish the desired total correctness result forDIV .⊓⊔Proof outlines are well suited for the documentation of programs becausethey allow us to record the main assertions that were used to establish thecorrectness of the programs, in particular the invariants and bound functionsof loops.3.5 CompletenessA natural question concerning any proof system is whether it is strong enoughfor the purpose at hand, that is, whether every semantically valid (i.e., true)formula can indeed be proved.
This is the question of completeness of a proofsystem. Here we are interested in the completeness of the proof systems PWand TW. We introduce the following more general definition.Definition 3.9. Let G be a proof system allowing us to prove correctnessformulas about programs in a certain class C. We say that G is complete forpartial correctness of programs in C if for all correctness formulas {p} S {q}about programs S in C|= {p} S {q} implies ⊢G {p} S {q}and that G is complete for total correctness of programs in C if for all correctness formulas {p} S {q} about programs S in C|=tot {p} S {q} implies ⊢G {p} S {q}.⊓⊔Thus completeness is the counterpart of soundness as defined in Definition 3.4.863 while ProgramsThere are several reasons why the proof systems PW and TW could beincomplete.(1) There is no complete proof system for the assertions used in the rule ofconsequence.(2) The language used for assertions and expressions is too weak to describethe sets of states and the bound functions needed in the correctnessproofs.(3) The proof rules presented here for while programs are not powerfulenough.Obstacle (1) is indeed true.
Since we interpret our assertions over a fixedstructure containing the integers, Gödel’s Incompleteness Theorem appliesand tells us that there cannot be any complete proof system for the set of alltrue assertions. We circumvent this problem by simply adding all true assertions to the proof systems PW and TW. As a consequence, any completenessresult will be in fact a completeness relative to the truth of all assertions.Obstacle (2) is partly true.
On the one hand, we see that all sets of statesneeded in correctness proofs can be defined by assertions. However, we alsoobserve that the syntax for expressions as introduced in Chapter 2 is notpowerful enough to express all necessary bound functions.Thus our question about completeness of the proof systems PW and TWreally address point (3). We can show that the axioms and proof rules given inthese proof systems for the individual program constructs are indeed powerfulenough. For example, we show that together with the consequence rule theloop II rule is sufficient to prove all true total correctness formulas aboutwhile programs.First let us examine the expressiveness of the assertions and expressions.For this purpose we introduce the notion of weakest precondition originallydue to Dijkstra [1975].Definition 3.10.
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
