IntroductionUnbounded ArraysImplementing Unbounded ArraysAmortized AnalysisDeleting ElementsInterfacesContracts and InterfacesLecture Notes onUnbounded Arrays15-122: Principles of Imperative ComputationFrank PfenningLecture 12February 22, 20111 IntroductionMost lectures so far had topics related to all three major categories of learn-ing goals for the course: computational thinking, algorithms, and program-ming. The same is true for this lecture. With respect to algorithms, we in-troduce unbounded arrays and operations on them. Analyzing them requiresamortized analysis, a particular way to reason about sequences of operationson data structures. We also briefly talk about again about data structure in-variants and interfaces, which are crucial computational thinking concepts.2 Unbounded ArraysIn the second homework assignment, you were asked to read in some filessuch 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? Inlater 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 constitutinga word. A problem is that before we start reading we don’t know howmany words there will be in the file so we cannot allocate an array of theright size! One solution uses either a queue or a stack. We discussed this inLecture 9 on Queues. Another solution is to use an unbounded array. Whilearrays are a language primitive, unbounded arrays are a data structure thatwe need to implement.Thinking about it abstractly, an unbounded array should be like an ar-ray in the sense that we can get and set the value of an arbitrary elementLECTURE NOTES FEBRUARY 22, 2011Unbounded Arrays L12.2via its index i. We should also be able to add a new element to the end ofthe array, and delete an element from the end of the array.We use the unbounded array by creating an empty one before reading afile. Then we read words from the file, one by one, and add them to the endof the unbounded array. Meanwhile we can count the number of elementsto know how many words we have read. We trust the data structure not torun out of space unless we hit some hard memory limit, which is unlikelyfor 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 unboundedarray, in order, the first word at index 0, the second at index 1, etc.The general implementation strategy is as follows. We maintain an ar-ray of a fixed length limit and an internal index size which tracks how manyelements are actually in the array. When we add a new element we incre-ment size , when we remove an element we decrement size. The tricky issueis how to proceed when we are already at the limit and want to add anotherelement. At that point, we allocate a new array with a larger limit and copythe elements we already have to the new array. For reasons we explainlater in this lecture, every time we need to enlarge the array we double itssize. Removing and element from the end is simple: we just decrementsize. There are some issues to consider if we want to shrink the array, butthis is optional.3 Implementing Unbounded ArraysAccording to our implementation sketch, an unbounded array needs totrack three forms of data: an integer limit , an integer size and an arrayof strings. We can put these together in a struct with fields limit , size andA as the fields of the struct. It is declared withtypedef string elem;struct ubarray {int limit; /* limit > 0 */int size; /* 0 <= size && size <= limit */elem[] A; /* \length(A) == limit */};The typedef says that, in this case, the elements are strings, but indicatesthat the implementation should really be independent of the kind of ele-ment stored in the array.LECTURE NOTES FEBRUARY 22, 2011Unbounded Arrays L12.3There are some data structure invariants that we maintain, although theymay be temporarily violated as the elements of the structure are manipu-lated at a low level. Generally, when we pass a pointer to the data structureor assign it to a variable we expect these invariants to hold. C0, however,has no intrinsic support for ensuring these invariants. Instead, our methodis to define a function to test them and then verify adherence to the in-variants in contracts as well as loop invariants and assertions. Here, thefunction is_uba serves that purpose.As a general idiom, when we use structs, we define a new type to standfor a pointer to the struct. This is because most of the time we work withpointers to structs rather than structs themselves. Here we call this newtype 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 canonly be tested in a precondition (or explicit @assert) since \length canonly appear in annotations.To create a new unbounded array, we allocate a struct ubarray andan 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 struc-ture invariants. Since we are implementing a general-purpose data struc-ture, we do not trust that clients will necessarily adhere to the contracts. WeLECTURE NOTES FEBRUARY 22, 2011Unbounded Arrays L12.4therefore check explicitly that the initial limit is strictly positive and signalan error if it is not. This is a common use of explicit assert statements.They will always be checked at runtime, while @assert annotations willnot: they are only verified when dynamic checking of contracts is enabled.Getting and setting an element of an unbounded array is straightfor-ward. 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 (belowlimit), because everything beyond the current size should be consideredto 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 ofwriting 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