Introduction
SWEN90010: HIGH INTEGRITY SYSTEMS ENGINEERING DEPARTMENT OF COMPUTING AND INFORMATION SYSTEMS THE UNIVERSITY OF MELBOURNE
Workshop Hoare Logic
In this workshop you will explore and use Hoare logic for reasoning about programs. The rules of Hoare logic introduced in lectures are summarised in Figure 1.
Copyright By PowCoder代写 加微信 powcoder
{P}skip{P} SKIP {P[E/x]}x := E{P} ASSIGN
{P1} S1 {Q} {P2} S2 {Q} {(B⇒P1)∧(¬B⇒P2)}ifBthenS1elseS2endif{Q} IF
{P∧B}S{P} P∧¬B⇒Q
{P} while B do S done {Q} WHILE
{P} S1 {R} {R} S2 {Q} SEQ {P}S1; S2 {Q}
Your tasks
P′⇒P {P}S{Q} Q⇒Q′ {P′} S {Q′}
CONSEQ Figure 1: Hoare Logic Rules
1. The rule of consequence, CONSEQ, is very useful for deriving new rules from existing ones. For example, the following is a slightly less general rule for while-loops that is often presented:
{P ∧ B} S {P }
{P } while B do S done {P ∧ ¬B}
Show how this rule can be derived from the WHILE rule above.
Solution: We give a formal proof of the more restricted while-loop rule.
Proof. Let P be a predicate (precondition), B a boolean condition and S a statement. To prove the more
restricted rule, it suffices to prove that
{P } while B do S done {P ∧ ¬B}, under the assumption that {P ∧ B} S {P } is true.
{P∧B}S{P} byassumption P∧¬B⇒P∧¬B bypredicatelogic
{P } while B do S done {P ∧ ¬B}
2. The following program is designed to sum up the elements of an array a, of length N, where elements of a are indexed from 1.
i := 0; sum := 0; whilei̸=N doi := i+1; sum := sum+a[i]done An invariant I for a while-loop while B do S done is a predicate that:
(a) is True at the start of the while-loop (i.e. at the point in the program just before the loop’s guard B is tested for the first time),
(b) is maintained by each iteration of the loop body S, i.e. {I ∧ B} S {I} holds,
(c) is strong enough to conclude that the postcondition of the loop holds, i.e. if the loop’s postcondition is
Q, then I ∧ ¬B ⇒ Q must hold.
Suppose we want to prove that after the while-loop above,
sum = a[j]. (1) j=1
Find a suitable invariant I for this loop to establish this postcondition, arguing informally that your choice of I meets the three criteria above.
Solution: The loop body modifies sum and i, so the invariant I likely has to relate the values of these two variables. It also has to tell us something about sum that will allow us to conclude that when i = N ,
sum = a[j]. j=1
Hence, it probably has to mention something of the form ?j=? a[j] somewhere.
At the point that we encounter the loop, sum is zero, which is the same as having summed up no elements of the array, i.e. sum = 0j=1 a[j]. i is also zero at this point. After one iteration (when i = 1 now), sum is
0 + a[1], or the sum of just the first element in the array, i.e. sum = 1j=1 a[j]. After the second iteration (when i = 2 now), sum is a[1] + a[2], i.e. sum = 2j=1 a[j].
The pattern emerging above is that:
So let I be this statement.
We show each of the three criteria:
sum = a[j] j=1
(a) Atthestartofthewhile-loop,i=0andsum=0. Soij=1a[j]=0andsosum=ij=1a[j]as required.
(b) Weneedtoshow{I∧i̸=N}i := i+1; sum := sum+a[i]{I}.Therearetwowaystodothis. One is informally, as the question suggests, which we do below. The other is to use Hoare logic, which happens later in the workshop.
Letting i0 and sum0 be the values of i and sum respectively in the pre-state before the two assignment statements are executed, and if and sumf be their final values after the two assignment statements, wehaveif =i0 +1andsumf =sum0 +a[if]=sum0 +a[i0 +1].
Since we know that I holds in the pre-state, we know that
sum0 =a[j]. (2)
a[j], i.e. sum0 + a[i0 + 1] = i0+1 a[j]. From j=1
What we need to prove is that sumf = if j=1
Formula 2 this is equivalent to
i0+1 +a[i0 +1]= a[j].
This statement follows trivially (since addition is associative).
(c) Finally, we have to show that the invariant I guarantees the postcondition, from Formula 1, once the loop terminates (i.e. when the loop guard is false). So we have to show I ∧ i = N ⇒ sum = Nj=1 a[j], i.e. that
This holds trivially.
sum=a[j]∧i=N ⇒sum=a[j]. j=1 j=1
3. Prove the above program correct under no assumptions about the state it executes from, i.e. prove:
{true} i := 0; sum := 0; while i ̸= N do i := i+1; sum := sum+a[i] done {sum = a[j]}. j=1
Solution: We have to prove
{true} i := 0; sum := 0; while i ̸= N do i := i+1; sum := sum+a[i] done {sum = a[j]}.
Applying the consequence rule to generalise the precondition, and the sequence rule, we insert the as-yet- unknown intermediate annotations ?P, ?Q and ?I:
whilei̸=N doi := i+1; sum := sum+a[i]done
{sum = Nj=1 a[j]}
We work backwards, beginning with the final goal:
whilei̸=N doi := i+1; sum := sum+a[i]done
{sum = Nj=1 a[j]}
The only rule we can apply (besides the consequence rule) is the while loop rule. Applying that rule requires us to prove that the loop body preserves the invariant (under the loop guard), and that, once the loop is done, the invariant (with the negation of the loop guard) implies the loop postcondition:
whilei̸=Ndo{?I∧i̸=N}i := i+1;sum := sum+a[i]{?I}done {?I ∧ i = N}
{sum = Nj=1 a[j]}
Clearly ?I should be our invariant I above, i.e. ?I is sum = j=1 ia[j]. We have to prove that I ∧ i =
N ⇒ sum = Nj=1 a[j], which holds trivially. Therefore the invariant with the negation of the loop guard implies the loop postcondition.
We also have to prove the invariant is preserved on each loop iteration:
{I∧i̸=N}i := i+1; sum := sum+a[i]{I}
We generalise the precondition via the consequence rule and apply the sequence rule to insert an intermediate
assertion, giving us:
{I ∧ i ̸= N}
sume := sum+a[i] {I}
We compute ?R2 by applying the assignment axiom ASSIGN: ?R2 is I[sum + a[i]/sum], which is sum + a[i] = j=1 ia[j]. We compute ?R similarly, so ?R is (sum + a[i] = j=1 ia[j])[i + 1/i], i.e. sum + a[i + 1] = j=1 i + 1. Finally we must check that I ∧ i ̸= N implies what we computed for ?R, namely sum + a[i + 1] = j=1 i + 1, i.e. we have to check whether:
i+1 sum = ia[j] ⇒ sum + a[i + 1] = j=1 j=1
… continued on next page …
Solution (continued): This is true since i a[j]+a[i+1] = i+1 a[j]. Therefore we have established j=1 j=1
that the loop body preserves the invariant.
We have now proved the loop establishes the postcondition, assuming the invariant I holds when the loop is
whilei̸=N doi := i+1; sum := sum+a[i]done
{sum = Nj=1 a[j]}
We now continue to work backwards through the program. We compute ?Q via the assignment axiom,
which says that ?Q is I[0/sum], i.e. (sum = ij=1 a[j])[0/sum], i.e. 0 = ij=1 a[j]. We then compute ?P similarly, so ?P is (0 = ij=1 a[j])[0/i], i.e. 0 = 0j=1 a[j].
Finally we must check whether true implies the computed ?P , i.e. whether
true ⇒ 0 = a[j] j=1
The summation sums from 1 up to 0, i.e. over an empty range, and so is 0 by definition. Therefore the right-hand side of the implication can be simplified to 0 = 0 which is a tautology and so is implied by true.
4. Compare the reasoning you just did to the informal reasoning you did earlier about the loop invariant. Ignoring the process of having to come up with the appropriate loop invariant, which kind of reasoning felt more mechanical? Which was more straightforward? Which felt more prone to errors?
Solution: The idea is that the second kind of reasoning with the rules is supposed to be entirely mechanical, once you have found the appropriate loop invariant. Because it is done by a series of rule applications and logical reasoning, the second (formal) approach should also be less error prone. Indeed, when reasoning informally about code you have written, it is always easy to convince yourself that your code is correct. The point of Hoare logic is to force you to check your reasoning objectively, by relying only on logical deduction and dispensing with intuition.
Where intuition does come in, in Hoare logic, is of course the process of coming up with appropriate loop invariants. However, once you have a good enough loop invariant, you no longer need to trust your intuition — you can use the rules of Hoare logic to prove that your intuition was correct (as well as proving your program correct too).
5. Suppose we implemented the above program in Ada, exactly as written, with sum and i being declared as type Integer. Does the proof we did above guarantee that the Ada program is correct? Why/why not?
Solution: No. If the array is too large, the Integer type will overflow, causing a potential runtime error. The proof above deals with mathematical integers, not fixed width ones. It probably guarantees that the program would be correct up to the limits of fixed width integers, although that assumes no bugs in the compiler or operating system etc. on which the program executes.
程序代写 CS代考 加微信: powcoder QQ: 1823890830 Email: powcoder@163.com