Lecture Notes on Unbounded Arrays 15 122 Principles of Imperative Computation Frank Pfenning Lecture 12 February 22 2011 1 Introduction Most lectures so far had topics related to all three major categories of learning goals for the course computational thinking algorithms and programming The same is true for this lecture With respect to algorithms we introduce unbounded arrays and operations on them Analyzing them requires amortized analysis a particular way to reason about sequences of operations on data structures We also briefly talk about again about data structure invariants and interfaces which are crucial computational thinking concepts 2 Unbounded Arrays In the second homework assignment you were asked to read in some files such as the Collected Works of Shakespeare or the Scrabble Players Dictionary What kind of data structure do we want to use when we read the file In later parts of the assignment we want to look up words perhaps sort them so it is natural to want to use an array of strings each string constituting a word A problem is that before we start reading we don t know how many words there will be in the file so we cannot allocate an array of the right size One solution uses either a queue or a stack We discussed this in Lecture 9 on Queues Another solution is to use an unbounded array While arrays are a language primitive unbounded arrays are a data structure that we need to implement Thinking about it abstractly an unbounded array should be like an array in the sense that we can get and set the value of an arbitrary element L ECTURE N OTES F EBRUARY 22 2011 Unbounded Arrays L12 2 via its index i We should also be able to add a new element to the end of the array and delete an element from the end of the array We use the unbounded array by creating an empty one before reading a file Then we read words from the file one by one and add them to the end of the unbounded array Meanwhile we can count the number of elements to know how many words we have read We trust the data structure not to run out of space unless we hit some hard memory limit which is unlikely for the kind of task we have in mind given modern operating systems When we have read the whole file the words will be in the unbounded array in order the first word at index 0 the second at index 1 etc The general implementation strategy is as follows We maintain an array of a fixed length limit and an internal index size which tracks how many elements are actually in the array When we add a new element we increment size when we remove an element we decrement size The tricky issue is how to proceed when we are already at the limit and want to add another element At that point we allocate a new array with a larger limit and copy the elements we already have to the new array For reasons we explain later in this lecture every time we need to enlarge the array we double its size Removing and element from the end is simple we just decrement size There are some issues to consider if we want to shrink the array but this is optional 3 Implementing Unbounded Arrays According to our implementation sketch an unbounded array needs to track three forms of data an integer limit an integer size and an array of strings We can put these together in a struct with fields limit size and A as the fields of the struct It is declared with typedef string elem struct ubarray int limit int size elem A limit 0 0 size size limit length A limit The typedef says that in this case the elements are strings but indicates that the implementation should really be independent of the kind of element stored in the array L ECTURE N OTES F EBRUARY 22 2011 Unbounded Arrays L12 3 There are some data structure invariants that we maintain although they may be temporarily violated as the elements of the structure are manipulated at a low level Generally when we pass a pointer to the data structure or assign it to a variable we expect these invariants to hold C0 however has no intrinsic support for ensuring these invariants Instead our method is to define a function to test them and then verify adherence to the invariants in contracts as well as loop invariants and assertions Here the function is uba serves that purpose As a general idiom when we use structs we define a new type to stand for a pointer to the struct This is because most of the time we work with pointers to structs rather than structs themselves Here we call this new type uba typedef struct ubarray uba bool is uba uba L requires L limit length L A return L limit 0 0 L size L size L limit Note that consistency between the L limit and the length of L A can only be tested in a precondition or explicit assert since length can only appear in annotations To create a new unbounded array we allocate a struct ubarray and an array of a supplied initial limit uba uba new int initial limit requires initial limit 0 ensures is uba result assert initial limit 0 uba L alloc struct ubarray L limit initial limit L size 0 L A alloc array elem L limit return L We ascertain in the postcondition that the result adheres to the data structure invariants Since we are implementing a general purpose data structure we do not trust that clients will necessarily adhere to the contracts We L ECTURE N OTES F EBRUARY 22 2011 Unbounded Arrays L12 4 therefore check explicitly that the initial limit is strictly positive and signal an error if it is not This is a common use of explicit assert statements They will always be checked at runtime while assert annotations will not they are only verified when dynamic checking of contracts is enabled Getting and setting an element of an unbounded array is straightforward However we do have to verify that the array access is in bounds This is stricter than checking that it is within the allocated array below limit because everything beyond the current size should be considered to be undefined These array elements have not yet been added to the array so reading or writing them is meaningless We show only the operation of writing to an unbounded array uba set void uba set uba L int index elem e requires is uba L assert 0 index index L size L A index e return More interesting is the operation of adding an element to the end of an unbounded array For that we need a function to resize an unbounded array This function takes an unbounded array L and a new limit new limit It is required that the new limit is strictly greater than the current size to make sure we have enough room to