Lecture Notes on Contracts 15 122 Principles of Imperative Computation Frank Pfenning Lecture 1 August 24 2010 1 Introduction For an overview the course goals and the mechanics and schedule of the course 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 role in this class since they represent the key to connect algorithmic ideas to imperative programs We follow the example from lecture developing annotations to a given program that express the contracts thereby making the program understandable and allowing us to find the bug If you have not seen this example we invite you to read this section by section to see how much of the story you can figure out on your own before moving on to the next section L ECTURE N OTES A UGUST 24 2010 Contracts 2 L1 2 A Mysterious Program You are a new employee in a company and a colleague comes to you with the following program written by your predecessor who was summarily fired for being a poor programmer Your colleague claims he has tracked a bug in a larger project to this function It is your job to find and correct this bug 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 try to determine what it does or is supposed to do and see if you spot the problem L ECTURE N OTES A UGUST 24 2010 Contracts 3 L1 3 A Shift in Perspective The code contains a few compound operators that we can expand to make it more readable k e expands into k k e i expands into i i 1 What about i 1 Remembering from your introductory programming class or looking it up you recall that this expression returns the result of shifting the bit representation of i to the left by 1 bit This means that the contribution of each bit to the value of i is doubled 1 Hence this operation corresponds to doubling the value of i modulo the precision of the representation of ints typically 32 or 64 bits With these insights we can rewrite the program into the following which is 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 1 see more in Lecture 3 Ints L ECTURE N OTES A UGUST 24 2010 Contracts 4 L1 4 Making a Conjecture The next step is to symbolically execute the program on some input values to see its results We notice that the computation of the loop is always the same regardless of input but that the number of iterations is controled by the input n We compose a small table with values of i and k in the loop on each iteration It is generally convenient in this kind of enterprise to record the values of variables just before the loop exit condition is tested because we can then directly see whether the test will succeed or fail Iteration 0 1 2 3 4 i k 0 0 1 1 2 4 3 9 4 16 From this we conjecture several propositions 1 i just records the number of iterations through the loop 2 k i2 The loop exits if k n and we return i 1 which was the value of i on the previous iteration For example for n 10 we return after iteration 4 and return 4 1 3 Nothing changes if n increases until it hits 16 in which case we iterate once more since k n and return 5 1 4 This leads us to the conjecture that the function is supposed to return the integer square root For a perfect square that is the root for other numbers it rounds the answer down L ECTURE N OTES A UGUST 24 2010 Contracts 5 L1 5 Finding a Loop Invariant Next we would like to try to verify that indeed the function returns the integer square root For this purpose we want to find the loop invariant A loop 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 time around the loop A loop invariant is checked just before the loop exit condition is evaluated From the simulated execution we conjecture that i i k is a loop invariant We use the syntax for annotations in C0 which is derived from similar syntax in JML and Spec which are languages supporting contracts for 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 L ECTURE N OTES A UGUST 24 2010 Contracts 6 L1 6 Verifying a Loop Invariant The next job is to verify the loop invariant or find a counterexample in case 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 loop invariant 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 will still 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 that is we execute one full iteration of the loop We obtain a new k let s call it k 0 k 0 k 2i 1 We also obtain a new i let s call it i0 i0 i 1 Now we have to show that the loop invariant still holds for i0 and k 0 that is i0 i0 k 0 assuming that it holds for i and k i0 i0 i 1 i 1 i i 2i 1 k 2i 1 k0 by definition if i0 by distributivity of multiplication by assumption by definition of k 0 So indeed the loop invariant still holds We were correct on every iteration i i k L ECTURE N OTES A UGUST 24 2010 Contracts 7 L1 7 A Postcondition for the Function What do we know when the loop exits Every time around the loop just before the exit test we have i i k When we exit the loop we also know that the loop test fails that is k n otherwise we would continue with the loop We can therefore say definitively that …