3. Verification of sequential and concurrent programs. Apt_ Olderog (3rd edition) (2010) (811405), страница 23
Текст из файла (страница 23)
One useful strategy is to generalize the postconditionq by replacing a constant by a variable. The following example illustrates thepoint.Summation ProblemLet N be an integer constant with N ≥ 0. The problem is to find a programSUM that stores in an integer variable x the sum of the elements of a givensection a[0 : N − 1] of an array a of type integer → integer. We require thata 6∈ change(SUM ). By definition, the sum is 0 if N = 0. Define nowr≡N ≥0andN −1q ≡ x = Σi=0a[i].The assertion q states that x stores the sum of the elements of the sectiona[0 : N − 1].
Our goal is to derive a program SUM of the formSUM ≡ T ; while B do S od.We replace the constant N by a fresh variable k. Putting appropriatebounds on k we obtaink−1p ≡ 0 ≤ k ≤ N ∧ x = Σi=0a[i]as a proposal for the invariant of the program to be developed.We now attempt to satisfy conditions 1–5 by choosing B, S and t appropriately.Re: 1. To establish {r} T {p}, we choose T ≡ k := 0; x := 0.Re: 3. To establish p ∧ ¬B → q, we choose B ≡ k 6= N .Re: 4. We have p → N − k ≥ 0, which suggests choosing t ≡ N − k as thebound function.Re: 5.
To decrease the bound function with each iteration, we choose theprogram k := k + 1 as part of the loop body.Re: 2. Thus far we have the following incomplete proof outline:1163 while Programs{r}k := 0; x := 0;{inv : p}{bd : t}while k 6= N do {p ∧ k 6= N }S1 ;{p[k := k + 1]}k := k + 1{p}od{p ∧ k = N }{q}where S1 is still to be found.To this end, we compare now the precondition and postcondition of S1 .The precondition p ∧ k 6= N impliesk−1a[i]0 ≤ k + 1 ≤ N ∧ x = Σi=0and the postcondition p[k := k + 1] is equivalent tok−10 ≤ k + 1 ≤ N ∧ x = (Σi=0a[i]) + a[k].We see that adding a[k] to x will “transform” one assertion into another.Thus, we can chooseS1 ≡ x := x + a[k]to ensure that p is a loop invariant.Summarizing, we have developed the following program together with itscorrectness proof:SUM ≡ k := 0; x := 0;while k 6= N dox := x + a[k];k := k + 1od.3.11 Case Study: Minimum-Sum Section ProblemWe now systematically develop a less trivial program.
We study here an example from Gries [1982]. Consider a one-dimensional array a of type integer→ integer and an integer constant N > 0. By a section of a we mean afragment of a of the form a[i : j] where 0 ≤ i ≤ j < N . The sum of a sectionja[i : j] is the expression Σk=ia[k]. A minimum-sum section of a[0 : N − 1] is asection a[i : j] such that the sum of a[i : j] is minimal among all subsectionsof a[0 : N − 1].3.11 Case Study: Minimum-Sum Section Problem117For example, the minimum-sum section of a[0 : 4] = (5, −3, 2, −4, 1) isa[1 : 3] = (−3, 2, −4) and its sum is −5.
The two minimum-sum sections ofa[0 : 4] = (5, 2, 5, 4, 2) are a[1 : 1] and a[4 : 4].Let si,j denote the sum of section a[i : j], that is,jsi,j = Σk=ia[k].The problem now is to find a program MINSUM such that achange(MINSUM ) and the correctness formula6∈{N > 0} MINSUM {q}holds in the sense of total correctness, whereq ≡ sum = min {si,j | 0 ≤ i ≤ j < N }.Thus q states that sum is the minimum of all si,j with i and j varying,where 0 ≤ i ≤ j < N holds.So the above correctness formula states that MINSUM stores in the variable sum the sum of a minimum-sum section of a[0 : N − 1].First we introduce the following notation, where k ∈ {1, .
. . , n}:sk = min {si,j | 0 ≤ i ≤ j < k}.Thus sk is the sum of a minimum-sum section of a[0 : k − 1]. Then wehave q ≡ sum = sN .We begin as in the previous example and try to find the invariant p byreplacing the constant N in the postcondition q by a fresh variable k and byputting appropriate bounds on k:p ≡ 1 ≤ k ≤ N ∧ sum = sk .As before, we now attempt to satisfy conditions 1–5 of Section 3.10 choosingB, S and t in an appropriate way.Re: 1. To establish {N > 0} T {p}, we choose as initialization T ≡ k :=1; sum := a[0].Re: 3. To establish p ∧ ¬B → q, we choose B ≡ k 6= N .Re: 4. Because p → N − k ≥ 0, we choose t ≡ N − k as the bound function.Re: 5. To decrease the bound function with each iteration, we put k := k + 1at the end of the loop body.Re: 2.
So far we have obtained the following incomplete proof outline fortotal correctness:1183 while Programs{N > 0}k := 1; sum := a[0];{inv : p}{bd : t}while k 6= N do {p ∧ k 6= N }S1 ;{p[k := k + 1]}k := k + 1{p}od{p ∧ k = N }{q},where S1 is still to be found. To this end, as in the previous example, wecompare the precondition and postcondition of S1 . We havep ∧ k 6= N → 1 ≤ k + 1 ≤ N ∧ sum = skandp[k := k + 1]↔ 1 ≤ k + 1 ≤ N ∧ sum = sk+1↔ 1 ≤ k + 1 ≤ N ∧ sum = min {si,j | 0 ≤ i ≤ j < k + 1}↔{{si,j | 0 ≤ i ≤ j < k + 1} ={si,j | 0 ≤ i ≤ j < k} ∪ {si,k | 0 ≤ i < k + 1}and min(A ∪ B) = min {minA, minB}}1 ≤ k + 1 ≤ N ∧ sum = min(sk , min {si,k | 0 ≤ i < k + 1}).Using the abbreviationtk ≡ min {si,k−1 | 0 ≤ i < k}for k ∈ {1, .
. . , n} we obtainp[k := k + 1] ↔ 1 ≤ k + 1 ≤ N ∧ sum = min(sk , tk+1 ).It is easy to check that the assignmentS1 ≡ sum := min(sum, tk+1 )(3.45)transforms the precondition 1 ≤ k+1 ≤ N ∧ sum = sk into the postcondition1 ≤ k + 1 ≤ N ∧ sum = min(sk , tk+1 ). In (3.45) the expression tk+1 stillneeds to be computed. We discuss two possible solutions.3.11 Case Study: Minimum-Sum Section Problem119Solution 1: Direct Computation.
If we just expand the definition of tk+1we arrive at the programk := 1; sum := a[0];while k 6= N dosum := min(sum, tk+1 );k := k + 1odwithtk+1 ≡ min {si,k | 0 ≤ i < k + 1}.The computation of tk+1 needs a number of steps proportional to k. Since thewhile loop is executed for k = 1, . . ., N , the whole program needs a numberof steps proportional toNΣk=1k=N · (N + 1),2that is, proportional to N 2 .Solution 2: Efficient Computation.
To develop a more efficient programwe introduce a new variable x which should store the value of tk+1 just beforeexecuting the assignment (3.45) to sum. For this purpose we strengthen theinvariant p. Since at the beginning of the kth iteration only the sums si,jwith i ≤ j < k have been investigated, we choose as the new invariantp∗ ≡ p ∧ x = tk ≡ 1 ≤ k ≤ N ∧ sum = sk ∧ x = tkand repeat the development process. We reuse the bound function t = N − kand add the initialization x := a[0].
This yields the following proof outlinefor total correctness:{N > 0}k := 1; sum := a[0]; x := a[0];{inv : p∗ }{bd : t}while k 6= N do{p∗ ∧ k 6= N }S1 ∗ ;{p∗ [k := k + 1]}k := k + 1{p∗ }od{p∗ ∧ k = N }{q},where S1 ∗ remains to be developed. To this end, we compare again the preand postcondition of S1 ∗ . We have1203 while Programsp∗ ∧ k 6= N → 1 ≤ k + 1 ≤ N ∧ sum = sk ∧ x = tkandp∗ [k := k + 1]↔ 1 ≤ k + 1 ≤ N ∧ sum = sk+1 ∧ x = tk+1↔{see p[k := k + 1] in Solution 1}1 ≤ k + 1 ≤ N ∧ sum = min(sk , tk+1 ) ∧ x = tk+1↔ 1 ≤ k + 1 ≤ N ∧ sum = min(sk , x) ∧ x = tk+1 .To bring this condition closer to the form of the precondition, we expresstk+1 with the help of tk :tk+1={definition of tk }min {si,k | 0 ≤ i < k + 1}={associativity of min}min(min {si,k | 0 ≤ i < k}, sk,k )={si,k = si,k−1 + a[k]}min(min {si,k−1 + a[k] | 0 ≤ i < k}, a[k]){property of min}min(min {si,k−1 | 0 ≤ i < k} + a[k], a[k])= {definition of tk }=min(tk + a[k], a[k]).Thusp∗ [k := k + 1]↔ 1 ≤ k + 1 ≤ N ∧ sum = min(sk , x) ∧ x = min(tk + a[k], a[k]).Using the assignment axiom, the composition rule and the rule of consequence, it is easy to check that the precondition1 ≤ k + 1 ≤ N ∧ sum = sk ∧ x = tkgets transformed into the postcondition1 ≤ k + 1 ≤ N ∧ sum = min(sk , x) ∧ x = min(tk + a[k], a[k])by the following sequence of assignments:S1 ∗ ≡ x := min(x + a[k], a[k]); sum := min(sum, x).3.12 Exercises121Thus we have now developed the following program MINSUM together withits correctness proof:MINSUM ≡ k := 1; sum := a[0]; x := a[0];while k 6= N dox := min(x + a[k], a[k]);sum := min(sum, x);k := k + 1od.To compute its result MINSUM needs only a number of steps proportionalto N .
This is indeed optimal for the problem of the minimum-sum sectionbecause each element of the section a[0 : N − 1] needs to be checked at leastonce.3.12 ExercisesLet N stand for M or Mtot .3.1. Prove the Input/Output Lemma 3.3.3.2. Prove the Change and Access Lemma 3.4.3.3. Prove that(i) N [[if B then S1 else S2 fi]] = N [[if ¬B then S2 else S1 fi]],(ii) N [[while B do S od]] =N [[if B then S; while B do S od else skip fi]].3.4.
Which of the following correctness formulas are true in the sense ofpartial correctness?(i) {true} x := 100 {true},(ii) {true} x := 100 {x = 100},(iii) {x = 50} x := 100 {x = 50},(iv) {y = 50} x := 100 {y = 50},(v) {true} x := 100 {false},(vi) {false} x := 100 {x = 50}.Give both an informal argument and a formal proof in the system PW. Whichof the above correctness formulas are true in the sense of total correctness?3.5.
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
