15 122 Principles of Imperative Computation Fall 2023 Recitation 01 C0 Basics Solutions Friday September 1st Administrivia and general advice Welcome to 15 122 recitation Take a moment to cid 28 ll in the particulars for this section so that you know which section you re in as well as your TAs name and email Section G TA Names Honk Chonk TA Emails honk andrew cmu edu N A TAGS syntax Checkpoint 0 Identify and correct the syntax errors in the following code to make it valid C0 9 int main print This is the fibonacci sequence starting from 0 n 1 use conio 3 def fib i if i 0 i 1 true return i 7 return fib i 1 fib i 2 for int i 0 i 10 i printf fib d d n Solution 1 use conio 3 int fib int i if i 0 i 1 return i return fib i 1 fib i 2 2 4 5 6 8 10 11 12 13 14 2 4 5 6 7 9 11 12 13 14 15 16 8 10 int main return 0 17 print This is the fibonacci sequence starting from 0 n for int i 0 i 10 i printf fib d d n i fib i Carnegie Mellon University 2023 Recitation 01 C0 Basics Page 2 of 8 Printing The simplest way to print something in C0 is to use printf For example printf Today is d s d n day month year The cid 28 rst argument is the string that you wish to print optionally containing format speci cid 28 ers among d s and c During printing these format speci cid 28 ers will be replaced by the values of the subsequent arguments in the order here the variables day month and year You use d to print an int value s for a string and c for a char Printing is bu cid 27 ered in C0 which means that output will be displayed on the terminal only when a new line character written n is encountered See the documentation for the conio library for more on printing in C0 Although printf is most commonly used C0 provides other printing functions print to print a string printint to print an integer etc See the documentation for the conio library for a complete list Carnegie Mellon University 2023 Recitation 01 C0 Basics Executing C0 Programs TAGS interpreter compilation Page 3 of 8 There are two ways to execute a C0 program run it through the interpreter or compile it Using coin the C0 interpreter allows you to execute individual functions with your chosen inputs interactively The cc0 compiler for C0 cid 28 rst translates your C0 code into an executable cid 28 le the default name is a out which you can then run to execute the main function and any function main calls There must be exactly one main function when using cc0 but no main is needed for coin Consider the following example where our program has been split into three cid 28 les What it does isn t important what matters is that dotproduct c0 calls a function in multiply c0 which itself calls a function in add c0 File add c0 File dotproduct c0 File multiply c0 int add int x int y return x y int multiply int x int y requires y 0 Dot product of x y and a b x y a b x a y b int dot product int x int y int a int b int result 0 while y 0 result add result x y int first multiply x a int second multiply y b return add first second return result int main return dot product 150 61 100 2 How would we compile this program with contract checking enabled cc0 d add c0 multiply c0 dotproduct c0 How would you run the resulting executable a out dptest How would you compile this program without contract checking enabled so that the executable is called dptest How would you then run it cc0 o dptest add c0 multiply c0 dotproduct c0 How would you use coin to check that multiply 3 2 evaluates to 6 What about using coin to cid 28 nd out what multiply 3 2 produces You may want to enable contracts coin d add c0 multiply c0 C0 interpreter coin 1 0 0 Quarter multiply 3 2 6 int multiply 3 2 multiply c0 2 4 2 20 requires annotation failed cid 4 cid 5 cid 4 cid 5 cid 4 cid 5 cid 4 cid 5 cid 7 cid 6 cid 7 cid 6 cid 7 cid 6 cid 7 cid 6 Carnegie Mellon University 2023 Recitation 01 C0 Basics Contracts TAGS correctness loop invariant safety There are 4 types of contract annotations in C0 for convenience we re using exp here to mean any Boolean expression Page 4 of 8 Annotation Checked requires exp ensures exp loop invariant exp assert exp before function execution before function returns before the loop condition is checked wherever you put it in the code There are certain special variables and functions you have access to only in annotations One of these is result It can be used only in ensures statements and it will give you the return value of the function There are other such variables functions that we ll get to later in the semester To help you develop an intuition about contracts here are some explanations of the di cid 27 erent kinds of annotations cid 136 requires For checking preconditions cid 136 ensures For checking postconditions Allow use of the special expression backslash result cid 136 loop invariant We can only write these immediately after the beginning of a while loop or for loop When are these checked immediately before the loop guard cid 136 assert Assertion statements don t play the special role in reasoning that requires ensures and loop invariant statements do They can be very helpful for debugging code and summarizing what you know especially after a loop TAGS correctness Proving the correctness of the mystery function We use contracts to both test our code and to reason about code With contracts careful point to reasoning and good testing both help us to be con cid 28 dent that our code is correct The code for the mystery function from lecture is reproduced on the left below To its right is an annotated control cid 29 ow diagram that highlights the di cid 27 erent parts in in what sequence they are executed Carnegie Mellon University 2023 Recitation 01 C0 Basics Page 5 of 8 1 int f int x int y 2 requires y 0 3 ensures POW x y result 4 int b x int e y int r 1 while e 0 loop invariant e 0 loop invariant POW b e r POW x y 5 6 7 8 9 10 11 12 13 14 15 16 17 18 if e 2 1 r b r b b b e e 2 return r 19 Proving that this function is correct is divided into four steps For …