59Lecture 6: Representation Invariants and Abstraction Functions 6.1 Introduction In this lecture, we describe two tools for understanding abstract data types: the representation invariant and the abstraction function. The representation invariant describes whether an instance of a type is well formed; the abstraction function tells us how to interpret it. Representation invariants can amplify the power of testing. It’s impossible to code an abstract type or modify it without understanding the abstraction function at least informally. Writing it down is useful, especially for maintainers, and crucial in tricky cases. 6.2 What is a Rep Invariant? A representation invariant, or rep invariant for short, is a constraint that characterizes whether an instance of an abstract data type is well formed, from a representation point of view. Mathematically, it is a formula over the representation of an instance; you can view it as a function that takes objects of the abstract type and returns true or false depending on whether they are well formed: RI : Object -> Boolean Consider the linked list implementation that we discussed last time. Here was its object model: The LinkedList class has a field, header, that holds a reference to an object of the class Entry. This object has three fields: element, which holds a reference to an element of the list; prev, which points to the previous entry in the list; and next, which points to the next element. This object model shows the representation of the data type. As we have ! ? ? ? ? ? List Entry Object header element prev next ?60mentioned before, object models can be drawn at various levels of abstraction. From the point of view of the user of the list, one might elide the box Entry, and just show a specification field from List to Object. This diagram shows that object model in black, with the representation in gold (Entry and its incoming and outgoing arcs) hidden: The representation invariant is a constraint that holds for every instance of the type. Our object model already gives us some of its properties: · It shows, for example, that the header field holds a reference to an object of class Entry. This property is important but not very interesting, since the field is declared to have that type; this kind of property is more interesting for the contents of polymorphic containers such as vectors, whose element type cannot be expressed in the source code. · The multiplicity marking ! on the target end of the header arrow says that the header field cannot be null. (The ! symbol denotes exactly one.) · The multiplicities ? on the target end of the next and prev arrows say that each of the next and prev arrows point to at most one entry. (The ? symbol denotes zero or one.) · The multiplicities ? on the source end of the next and prev arrows say that each entry is pointed to by at most one other entry’s next field, and by at most one other entry’s prev field. (The ? symbol denotes zero or one.) · The multiplicity ? on the target end of the element field says that each Entry points to at most one Object. Some properties of the object model are not part of the representation invariant. For example, the fact that entries are not shared between lists (which is indicated by the multiplicity on the source end of the header arrow) is not a property of any single list. There are properties of the representation invariant which are not shown in the graphical object model: · When there are two e1 and e2 entries in the list, if e1.next = e2, then e2.prev = e1. elems[] ? ? ? ? ? List Entry Object element prev next ? ! header61· The dummy entry at the front of the list has a null element field. There are also properties that do not appear because the object model only shows objects and not primitive values. The representation of LinkedList has a field size that holds the size of the list. A property of the rep invariant is that size is equal to the number of entries in the list representation, minus one (since the first entry is a dummy). In fact, in the Java implementation java.util.LinkedList, the object model has an additional constraint, reflected in the rep invariant. Every entry has a non-null next and prev: Note the stronger multiplicities on the next and prev arrows. Here is a sample list of two elements (and therefore three entries, including the dummy): prev next ( List ) header element prev next ( Entry ) ( Entry ) ( Object ) element prev ( Entry ) ( Object ) next ! ? ! ! ? List Entry Object element prev next ! ! header62When examining a representation invariant, it is important to notice not only what constraints are present, but also which are missing. In this case, there is no requirement that the element field be non-null, nor that elements not be shared. This is what we’d expect: it allows a list to contain null references, and to contain the same object in multiple positions. Let’s summarize our rep invariant informally: for every instance of the class LinkedList the header field is non-null the header field has a null element field there are (size + 1) entries the entries form a cycle starting and ending with the header entry for any entry, taking prev and then next returns you to the entry We can also write this a bit more formally: all p: LinkedList | p.header != null && p.header.element = null && p.size + 1 = | p.header.*next | && p.header = p.header.next p.size + 1 && all e in p.header.*next | e.prev.next = e To understand this formula, you need to know that · for any expression e denoting some set of objects, and any field f, e.f denotes the set of objects you get if you follow f from each of the objects in e; · e.*f means that you collect the set of objects obtained by following f any number of times from each of the objects in e; · | e | is the number of objects in the set denoted by e. So p.header.*next for example denotes the set of all entries in the list, because you get it by taking the list p, following the header field, and then following the next field any number of times. One thing that this formula makes very clear is that the representation invariant is about a single linked list p. Another fine way to write the invariant is this: R(p) = p.header != null && p.header.element = null && p.size + 1 = | p.header.*next| && p.header = p.header.next p.size + 1 && all e in p.header.*next | e.prev.next = e in which we view the