CIS 301: Lecture Notes on Program VerificationTorben AmtoftDepartment of Computing and Information SciencesKansas State UniversitySeptember 28, 2006These notes are written as a supplement to [1, Sect. 16.5], but can be readindependently. Section 6 is inspired by Chapter 16 in [3], an excellent treatiseon the subject of program construction; also our Section 10 is inspired bythat book. The proof rules in Section 7 are inspired by the presentation in[4, Chap. 4]. Section 8 is inspired by [2].Contents1 Hoare Triples 32 Software Engineering 33 Specifications 43.1 Square root . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43.2 Factorial . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 54 A Simple Language 65 Loop Invariants 75.1 Motivating Example . . . . . . . . . . . . . . . . . . . . . . . 75.2 Proof Principles for Loop Invariants . . . . . . . . . . . . . . 105.3 Proof Principles for Loop Termination . . . . . . . . . . . . . 1016 Developing a Correct Program 106.1 Deleting a Conjunct . . . . . . . . . . . . . . . . . . . . . . . 116.2 Replacing an Expression By an Identifier . . . . . . . . . . . . 127 Well-Annotated Programs and Valid Assertions 148 Secure Information Flow 218.1 Examples . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 218.2 Specification . . . . . . . . . . . . . . . . . . . . . . . . . . . . 228.3 Examples Revisited . . . . . . . . . . . . . . . . . . . . . . . . 238.4 Declassification . . . . . . . . . . . . . . . . . . . . . . . . . . 248.5 Data Integrity . . . . . . . . . . . . . . . . . . . . . . . . . . . 259 Procedures 259.1 Contracts . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 279.2 Rule for Pro ce dure Calls . . . . . . . . . . . . . . . . . . . . . 2810 Arrays 3110.1 Verifying Programs Reading Arrays . . . . . . . . . . . . . . . 3210.2 Verifying Programs Updating Arrays . . . . . . . . . . . . . . 3521 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. Here φ and ψ are assertions,written in First Order Logic.Actually, the above description is ambiguous: what if P does not terminate?Therefore we shall distinguish b e tweenpartial 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.2 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 in fact it 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.3When it comes to academic discourse, 1 is an interesting task but onlybriefly touched upon (Section 3) in CIS 301. Instead, we shall focus on 3(Sections 5 and 7), but also give a few basic heuristics for how to do 2 and3 simultaneously (Section 6).3 Specifications3.1 Square rootSuppose the user demandsCompute the square ro ot of x and store the result in y.As a first attempt, we may write the sp e cificationP{y2= x}We now remember that we cannot compute the square root of negativenumbers and therefore add a precondition:{x ≥ 0}P{y2= x}Then we realize that if x is not a perfect s quare then we have to settle foran approximation (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. Thus,we must also specify that y is the largest number that does the job:{x ≥ 0}P{y2≤ x ∧ (y + 1)2> x}which seems a sensible specification of the square root program. (Whichentails that y has to be non-negative. Why?)43.2 FactorialNow assume that the user demandsEnsure that y contains the factorial1of x.This might give rise to the specification{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?The answer is that we shall allow our specifications to contain logical vari-ables2: using the logical variable x0to denote the initial (and un-changed)value of the identifier x, a program computing factorials can be specified asfollows:{x = x0≥ 0}P{y = fac(x0) ∧ x = x0}Likewise, the specification of the square root program can be modified.1Remember that the factorial function is defined byfac(0) = 1fac(n + 1) = (n + 1)fac(n) for n ≥ 0and thus fac(0) = 1, fac(1) = 1, fac(2) = 2, fac(3) = 6, fac(4) = 24, etc.2We shall write logical variables with a subscript, so as to emphasize that they do noto ccur in programs.54 A Simple LanguageFor the next sections, we shall consider programs P written in a simplelanguage, omitting3many desirable language features—such as procedures,considered in Section 9, and arrays, considered in Section 10. A program Pis (so far) just a command, with the syntax of commands given by4C ::= x := E| C1; C2| if B then C1else C2fi| while B do C odPrograms are thus constructed from• assignments of the form x := E, the effect of which is to store thevalue of E in x;• sequential compositions of the form C1; C2, the effect of which is tofirst execute C1and next execute C2;• conditionals of the form if B then C1else C2fi, the effect of whichis to execute C1if B evaluates to true, but execute C2if B evaluatesto false;• while loops of the form while B do C od, the effect of which is toiterate executing C as long as B evaluates to true5.We have employed some …