CIS 301: Lecture Notes on Program VerificationTorben AmtoftDepartment of Computing and Information SciencesKansas State UniversitySeptember 29, 2007These 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 8 is inspired by thatbook. The proof rules in Section 7 are inspired by the presentation in [4,Chap. 4]. Section 10 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 Arrays 228.1 Verifying Programs Reading Arrays . . . . . . . . . . . . . . . 228.2 Verifying Programs Updating Arrays . . . . . . . . . . . . . . 259 Procedures 299.1 Contracts . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 309.2 Rule for Pro ce dure Calls . . . . . . . . . . . . . . . . . . . . . 3210 Secure Information Flow 3510.1 Examples . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 3510.2 Specification . . . . . . . . . . . . . . . . . . . . . . . . . . . . 3610.3 Examples Revisited . . . . . . . . . . . . . . . . . . . . . . . . 3710.4 Dec lassification . . . . . . . . . . . . . . . . . . . . . . . . . . 3810.5 Data Integrity . . . . . . . . . . . . . . . . . . . . . . . . . . . 3821 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 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.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 root of x and store the result in y.As 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:{x ≥ 0}P{y2= x}Then we realize that if x is not a perfect square 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 m ight 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 modify x.Well, if not, that better has to be part of the specification! But how toincorporate such demands?One approach is to augment specifications with information ab out whichidentifiers2are allowed to be modified; in the above case, we would excludex from that set. Another approach is to allow specifications to containlogical variables3: using the logical variable x0to denote the initial (andun-changed) value of the identifier x, a program computing factorials can bespecified as follows: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 use the term “identifier” for what is often called a “program variable”, soas to avoid confusion with the variables of First O rder Logic. To further facilitate thatdistinction, we shall always write identifiers in typewriter font.3We shall write logical variables with a subscript, so as to emphasize that they do noto ccur in programs.5{x = x0≥ 0}P{y = fac(x0) ∧ x = x0}Likewise, the specification of the square root program can be augmented soas to express that x must not be modified.4 A Simple LanguageFor the next sections, we shall consider programs P written in a simplelanguage, omitting4many des irable language features—such as procedures,considered in Section 9, and arrays, considered in Sec tion 8. A program Pis (so far) just a command, with the syntax of commands given by5C ::= 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, …