IntroductionA Mysterious ProgramA Shift in PerspectiveMaking a ConjectureFinding a Loop InvariantVerifying a Loop InvariantA Postcondition for the FunctionA Strengthened PostconditionA Strengthened Loop InvariantA PreconditionTerminationFixed Precision ArithmeticLecture Notes onContracts15-122: Principles of Imperative ComputationFrank PfenningLecture 1August 24, 20101 IntroductionFor an overview the course goals and the mechanics and schedule of thecourse, please see course Overview. In these notes we review contracts,which we use to collectively denote function contracts, loop invariants,and other assertions about the program. Contracts will play a central rolein this class, since they represent the key to connect algorithmic ideas toimperative programs. We follow the example from lecture, developing an-notations to a given program that express the contracts, thereby making theprogram understandable (and allowing us to find the bug).If you have not seen this example, we invite you to read this section bysection to see how much of the story you can figure out on your own beforemoving on to the next section.LECTURE NOTES AUGUST 24, 2010Contracts L1.22 A Mysterious ProgramYou are a new employee in a company, and a colleague comes to you withthe following program, written by your predecessor who was summarilyfired for being a poor programmer. Your colleague claims he has tracked abug in a larger project to this function. It is your job to find and correct thisbug.int f (int n) {int i = 0; int k = 0;while (k <= n) {k += (i<<1) + 1;i++;}return i-1;}Before you read on, you might examine this program for a while to tryto determine what it does, or is supposed to do, and see if you spot theproblem.LECTURE NOTES AUGUST 24, 2010Contracts L1.33 A Shift in PerspectiveThe code contains a few compound operators that we can expand to makeit more readable. k += e; expands into k = k + e;. i++; expands intoi = i + 1;.What about i<<1? Remembering from your introductory programmingclass, or looking it up, you recall that this expression returns the result ofshifting the bit representation of i to the left by 1 bit. This means that thecontribution of each bit to the value of i is doubled.1Hence this opera-tion corresponds to doubling the value of i, modulo the precision of therepresentation of ints (typically 32 or 64 bits).With these insights we can rewrite the program into the following, whichis closer to a mathematical expression of the computation.int f (int n) {int i = 0; int k = 0;while (k <= n) {k = k + 2*i + 1;i = i + 1;}return i-1;}1see more in Lecture 3: IntsLECTURE NOTES AUGUST 24, 2010Contracts L1.44 Making a ConjectureThe next step is to symbolically execute the program on some input valuesto see its results. We notice that the computation of the loop is always thesame, regardless of input, but that the number of iterations is controled bythe input n. We compose a small table with values of i and k in the loop oneach iteration. It is generally convenient in this kind of enterprise to recordthe values of variables just before the loop exit condition is tested because wecan then directly see whether the test will succeed or fail.Iteration i k0 0 011 12 2 43 3 94 4 16From this we conjecture several propositions:1. i just records the number of iterations through the loop.2. k = i2The loop exits if k > n and we return i − 1, which was the value of i on theprevious iteration. For example, for n = 10 we return after iteration 4 andreturn 4 − 1 = 3. Nothing changes if n increases until it hits 16, in whichcase we iterate once more (since k = n) and return 5 − 1 = 4. This leads usto the conjecture that the function is supposed to return the integer squareroot. For a perfect square that is the root, for other numbers it rounds theanswer down.LECTURE NOTES AUGUST 24, 2010Contracts L1.55 Finding a Loop InvariantNext, we would like to try to verify that, indeed, the function returns theinteger square root. For this purpose we want to find the loop invariant. Aloop invariant is a boolean expression (that is, evaluating to true or false)which is true the first time a loop is entered, and remains true every timearound the loop. A loop invariant is checked just before the loop exit con-dition is evaluated.From the simulated execution we conjecture that i * i == k is a loopinvariant. We use the syntax for annotations in C0, which is derived fromsimilar syntax in JML and Spec# which are languages supporting contractsfor Java and C#, respectively.int f (int n) {int i = 0; int k = 0;while (k <= n)//@loop_invariant i * i == k;{k = k + 2*i + 1;i = i + 1;}return i-1;}LECTURE NOTES AUGUST 24, 2010Contracts L1.66 Verifying a Loop InvariantThe next job is to verify the loop invariant, or find a counterexample incase it is wrong. Since we have been told to expect a bug in the program,we have to account for the possibility that the function is indeed incorrect.The best way of finding a counterexample is often to try to verify the loopinvariant and see where the reasoning breaks down.To verify a loop invariant we have to prove two things:1. The loop invariant is true when we enter the loop the first time.2. Assuming the loop invariant is true at the start of one iteration, it willstill be true at the end of that iteration.Let us go through the steps.1. When we enter the loop, we have i = 0 and k = 0, so i × i = 0 = k.The loop invariant holds.2. Now we assume that i × i = k and we go around the loop once (thatis, we execute one full iteration of the loop). We obtain a new k, let’scall it k0.k0= k + 2i + 1We also obtain a new i, let’s call it i0.i0= i + 1Now we have to show that the loop invariant still holds for i0and k0(that is, i0× i0= k0), assuming that it holds for i and k.i0× i0= (i + 1) × (i + 1) by definition if i0= i × i + 2i + 1 by distributivity of multiplication= k + 2i + 1 by assumption= k0by definition of k0So, indeed, the loop invariant still holds! We were correct: on every itera-tion, i × i = k.LECTURE NOTES AUGUST 24, 2010Contracts L1.77 A Postcondition for the FunctionWhat do we know when the loop exits? Every time around the loop, justbefore the exit test, we have i × i = k. When we exit the loop we also knowthat the loop test fails, that is, k > n (otherwise, we would continue withthe loop). We can therefore say definitively thati × i > nwhen we exit the loop. We return i − 1 from the function. If we add 1 to thereturn value on argument n its square must be bigger than