Unformatted text preview:

CIS 301: Lecture Notes on Program VerificationTorben AmtoftDepartment of Computing and Information SciencesKansas State UniversityMay 5, 2003These notes are written as a supplement to [1, Sect. 16.5], but can be read in-dependently. The proof rules are inspired by the presentation in [3, Chap. 4].Section 5 is inspired by Chapter 16 in [2], an excellent treatise on the subjectof program construction.1 Hoare TriplesTo reason about correctness we shall consider Hoare triples, of the form{φ}P{ψ}saying that if φ (the precondition) holds prior to executing program code Pthen ψ (the postcondition) holds afterwards.Actually, the above description is ambiguous: what if P does not terminate?Therefore we shall distinguish betweenpartial correctness: if P terminates then ψ holds;total correctness: P does terminate and then ψ holds.In these notes, we shall interpret a Hoare triple as denoting partial correct-ness unless stated otherwise.12 Software EngineeringIn light of the notion of Hoare triples, one can think of software engineeringas a 3-stage process:1. Translate the demands D of the user into a specification (φD, ψD).2. Write a program P that satisfies the specification constructed in 1.3. Prove that it in fact holds that{φD}P{ψD}When it comes to software practice, 1 is a huge task (involving numerous dis-cussions with the users) and hardly ever done completely. While 2 obviouslyhas to be done, 3 is almost never carried out.When it comes to academic discourse, 1 is an interesting task but only brieflytouched upon (Section 3) in CIS 301. Instead, we shall focus on 3 (Section4), but also give a few basic heuristics for how to do 2 and 3 simultaneously(Section 5).3 SpecificationsSquare rootSuppose the user demandsCompute the square root of x and store the result in yAs a first attempt, we may write the specificationP{y2= x}We now remember that we cannot compute the square root of negativenumbers and therefore add a precondition:2{x ≥ 0}P{y2= x}Then we realize that if x is not a square then we have to settle for anapproximation (since we are working with integers):{x ≥ 0}P{y2≤ x}On the other hand, this is too liberal: we could just pick y to be zero.Therefore, we must also specify that y is the largest number that does thejob:{x ≥ 0}P{y2≤ x ∧ (y + 1)2> x}which seems a sensible specification of the square root program. (Observethat it entails that y has to be non-negative. Why?)FactorialNow assume that the user demandsEnsure that y contains the factorial of x.(Remember that the factorial function is defined byfac(0) = 1fac(n + 1) = (n + 1)fac(n) for n ≥ 0and thusfac(0) = 1, fac(1) = 1, fac(2) = 2, fac(3) = 6, fac(4) = 24, etc.)It therefore seems that this should produce the specification3{x ≥ 0}P{y = fac(x)}Well, it’s not hard to write a program satisfying this specification:{x ≥ 0}x := 4;y := 24{y = fac(x)}The user may respond:Hey, that’s cheating! You were not allowed to change x.Well, if not that better has to be part of the specification! But how toincorporate such demands? We shall need the concept of logical variables:these do not occur in programs, only in specifications, and are written witha subscript.Using the logical variable x0to denote the initial (and un-changed) value ofx, a program computing factorials can be specified as follows:{x = x0≥ 0}P{y = fac(x0) ∧ x = x0}Similarly, the specification of the square root program can be modified.4 Proving CorrectnessWe shall now discuss how to verify a claim that{φ}P{ψ}4where P is a program written in a language with the following simple1syntax:C ::= x := E| C1; C2| if B then C1else C2fi| while B do C odwhere B stands for boolean tests of the form E1< E2, E1≤ E2, E16= E2,etc; and E stands for integer expressions of the form n (a constant), x(a variable), E1+ E2, E1− E2, etc. Programs are thus constructed fromassignments, sequential composition, conditionals, and while-loops2.4.1 InvariantsFor the purpose of verification, the notion of invariants is crucial.4.1.1 Motivating exampleWe look at the following program for computing the factorial function3(cf.Section 3).{x ≥ 0}y := 1;z := 0;while z 6= x doz := z + 1;y := y ∗ zod{y = fac(x)}1Many desirable language features (such as procedures) are absent from our languagewhich, however, is “Turing-complete” in that it can encode all other features one canimagine!2Note that we use the symbol od to end while-loops, rather than a curly bracket as thissymbol is used for writing pre- and post-conditions. Similarly, we use fi as a delimiterfor conditionals.3Since the program does not change the value of x, we can safely write its specificationwithout employing a logical variable x0.5There are many mistakes we could have made when writing that program:for instance we could have reversed the two lines in the loop body (in whichcase y would be assigned zero and keep that value forever), or we could havewritten the loop test as z ≤ x (in which case y would end up containingfac(x + 1)).Let us now convince ourselves that what we wrote is correct. We might firsttry a simulation: if say x = 4, the situation at the entry of the loop is:x y zAfter 0 iterations 4 1 0After 1 iterations 4 1 1After 2 iterations 4 2 2After 3 iterations 4 6 3After 4 iterations 4 24 4and then z = x so that the loop terminates, with y containing the desiredresult 24 = fac(x). This may boost our confidence in the program, but stilla general proof is needed. Fortunately, the table above may help us in thatendeavor. For it suggests that it is always the case that y = fac(z).Definition 4.1. A property which holds each time the loop test is evaluatedis called an invariant for the loop.Equivalently, a property ψ is an invariant for a loop iff ψ holds after anynumber (≥ 0) of loop iterations.We now annotate the program with our prospective invariant:{x ≥ 0}y := 1;z := 0;{y = fac(z)}while z 6= x doz := z + 1;y := y ∗ zod{y = fac(x)}Of course, we must prove that what we have found is indeed an invariant:Proposition 4.2. For all k ≥ 0, after k iterations of the loop it holds thaty = fac(z).6This proposition almost begs for a proof by induction!Establishing the invariant. The base step amounts to checking thaty = fac(z) after 0 iterations. But since the preamble assigns y the value 1and assigns z the value 0, the claim follows from the fact that fac(0) = 1.Maintaining the invariant. The inductive step amounts to checkingthat if y = fac(z) holds after k iterations, then it also


View Full Document

K-State CIS 301 - Study Notes

Download Study Notes
Our administrator received your request to download this document. We will send you the file to your email shortly.
Loading Unlocking...
Login

Join to view Study Notes and access 3M+ class-specific study document.

or
We will never post anything without your permission.
Don't have an account?
Sign Up

Join to view Study Notes 2 2 and access 3M+ class-specific study document.

or

By creating an account you agree to our Privacy Policy and Terms Of Use

Already a member?