CIS 301: Lecture Notes on Program VerificationTorben AmtoftDepartment of Computing and Information SciencesKansas State UniversityFebruary 26, 2008These notes are written as a supplement to [1, Sect. 16.5], but can be readindependently. Section 6 is inspired by Chapter 16 in [4], 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 [5,Chap. 4]. Section 10 is inspired by [3].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 . . . . . . . . . . . . . . . . . . . . . . . 85.2 Proof Principles for Loop Invariants . . . . . . . . . . . . . . 105.3 Proof Principles for Loop Termination . . . . . . . . . . . . . 1016 Developing a Correct Program 116.1 Deleting a Conjunct . . . . . . . . . . . . . . . . . . . . . . . 126.2 Replacing an Expression By an Identifier . . . . . . . . . . . . 137 Well-Annotated Programs and Valid Assertions 158 Arrays 228.1 Verifying Programs Reading Arrays . . . . . . . . . . . . . . . 228.2 Verifying Programs Updating Arrays . . . . . . . . . . . . . . 269 Procedures 319.1 Contracts . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 329.2 Rule for Pro ce dure Calls . . . . . . . . . . . . . . . . . . . . . 3410 Secure Information Flow 3710.1 Examples . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 3710.2 Specification . . . . . . . . . . . . . . . . . . . . . . . . . . . . 3810.3 Examples Revisited . . . . . . . . . . . . . . . . . . . . . . . . 3910.4 Dec lassification . . . . . . . . . . . . . . . . . . . . . . . . . . 4010.5 Data Integrity . . . . . . . . . . . . . . . . . . . . . . . . . . . 4021 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 numerousdiscussions with the users) and hardly ever done completely, whereas 2 ob-viously has to be done. Until recently, 3 was almost never carried out, but3the c urrent trend in industry is towards increased use of formal verification.A noteworthy example of this is the ASTREE system1which has been usedto prove, completely automatically, the absence of certain kind of errors inthe flight control software of the Airbus A340 and A380 airplanes.When 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}1ASTREE has a web page at http://www.astree.ens.fr, and a description of its corewas published in [2].4On 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?)3.2 FactorialNow assume that the user demandsEnsure that y contains the factorial2of 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.2Remember 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.5Well, 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 whichidentifiers3are allowed to be modified; in the above case, we would excludex from that set. Another approach is to allow specifications to containlogical variables4: using the logical variable x0to denote the initial (andun-changed) value of the identifier x, a program computing factorials can bespecified as follows:{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, omitting5many 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 by6C ::= x := E| C1; C2| if B then C1else C2fi| while B do C od3We shall use the term “identifier” for what is often called a “program variable”, soas to avoid confusion with the variables of First O …