Abstract data type 2026-10-13
An abstract data type specifies values and operations independently of their storage. A FIFO queue has ordered sequences as its abstract values; an array and a linked list can represent those same values. A representation invariant identifies valid storage states, and an abstraction function says what each valid state means.[ref]
Reading 13: Abstraction Functions & Rep Invariants. Reading 13, Rep Invariant and Abstraction Function: representation values, abstract values, AF and RI
Abstract data type invariant Created 2026-10-24 Updated 2026-10-31
A condition describing legal abstract states, independently of their concrete storage. A bounded-key multiset has nonnegative counts and zero counts outside its allowed range. A representation invariant instead constrains implementation states; an abstraction function connects a valid representation to its abstract state. The two kinds of invariant should not be conflated.
Abstraction function Created 2026-10-13 Updated 2026-10-14
An abstraction function maps a valid concrete representation to its abstract value. Write and . Different storage states can denote the same abstract value. Correct implementation requires both preservation of the representation invariant and agreement with the specified operation after applying the abstraction function; preserving a length bound alone would not prove first-in, first-out behavior.
The representation invariant answers "is this storage state allowed?" The abstraction function answers "which value does it represent?" Thus is a truth value, whereas is a value of the abstract data type. Treating as a partial function on all storage states, or as a function defined on only, expresses the same restriction. The abstraction function may forget storage details, and need not be executable code: its purpose is to connect an implementation to its formal specification.[ref]
Reading 13: Abstraction Functions & Rep Invariants. Rep Invariant and Abstraction Function: representation space, abstract space, partial AF and boolean RI
This distinction makes functional correctness manageable one operation at a time. The unreduced rational representation below separates valid storage from mathematical meaning; correct operations through an abstraction function then checks whether an implementation performs the promised addition. For an example with hidden mutable storage and failure cases, the bounded queue with encapsulation supplies a different abstraction function, reading an occupied prefix of an array as a sequence.
Array multiset Created 2026-10-25 Updated 2026-10-31
A multiset of keys in a fixed finite integer range represented by one nonnegative count per key. The abstraction function extends the stored array counts by zero outside the range. Single-key additions, removals and queries use constant array work, provided overflow and operation preconditions are handled. Encapsulation of the count array is necessary to preserve its representation invariant.
Bounded queue with encapsulation 2026-10-13
Consider an original FIFO queue example storing immutable labels, with fixed positive integer capacity . Its abstract state is a finite sequence , with . The API has
enqueue(x), dequeue(), peek() and size(). Successful enqueue returns ok; a full queue returns full and is unchanged. Successful dequeue returns the first label and removes it; an empty queue returns empty and is unchanged. peek returns the first label or empty without modification, and size returns . The status results are distinct from stored labels.For a compact array representation , fix and require the representation invariantThe abstraction function is . Only these first entries matter; unused slots have no abstract meaning. On successful
enqueue(x), write and then set . On successful dequeue(), save , shift the remaining entries left, and decrement . Testing the full or empty case before updating gives the specified unchanged failure state.Permitted queue calls preserve valid states; an unrestricted count write bypasses the API
. Details. With and ,
enqueue(C) produces ; enqueue(D) returns full without change. A raw write violates the representation invariant. More subtly, changing the count from two to one satisfies its bounds but discards without a permitted operation. Validity of the storage state and legality of the API transition are different obligations. A setter for every storage field would surrender the useful boundary even if its name looked like an ordinary operation. Circular buffer indices Created 2026-10-18 Updated 2026-10-24
Let the capacity be a positive integer , and allocate exactly array slots . Store the front array index and count . The representation invariant isThe logical sequence and next-write array index areHere denotes the nonnegative remainder from modular arithmetic. The count determines which slots are live: leftover bits in other slots are not members of the FIFO queue. If , has no current front item; it identifies the position where the next successful insertion begins. If , points at a live item, so writing there requires an explicit overwrite policy.
For ,
enqueue(x) writes , then increments , leaving fixed. For , dequeue() saves and returns , then sets and . These are sequential updates, completed before the next call. A rejecting interface tests or first and returns full or empty, respectively, without changing state. peek returns only when ; size returns .One can instead store and , recovering . On insertion, advance and increment ; on removal, keep fixed and decrement . Thus the next-write array index is not necessarily the front array index.
Names such as
head and tail require checking the actual API: the kernel documentation calls the insertion position head and the removal position tail.[ref]Circular Buffers by David Howells and Paul E. McKenney. David Howells and Paul E. McKenney, Circular Buffers, What is a circular buffer?: head is insertion, tail is removal
The diagram is the state after step 8 of circular buffer operation trace. Reading the physical array from slot zero would give , which includes a removed label and puts first. Reading from for exactly items gives . The next insertion uses slot , not slot . This distinction also explains why the live sequence may need two contiguous pieces of the array: here slots through , followed by slot . No items need to move to make this wrap work.
Constant-time distinct-size counter 2026-10-25
Maintain a counter equal to the number of positive count-array entries. Increment it only when an addition changes zero to one; decrement it only when a removal changes one to zero. Other count changes leave the support unchanged. Initialization at zero and these cases prove the representation invariant by induction over completed operations, giving a constant-time distinct-size query.
For a deterministic binary operation on an abstract data type, let be its specified operation on abstract values and the implementation on concrete states. For every permitted valid input pair , require bothThe first condition preserves the representation invariant. The second makes a commutative diagram: either execute and then apply the abstraction function, or apply the abstraction function to both inputs and then execute the abstract operation ; both paths reach the same value. These conditions state functional correctness of a completed operation; termination is an additional obligation for algorithm correctness.[ref]
8.3 Module Documentation. Sections 8.3.3, Commutative Diagrams, and 8.3.4, Representation Invariants: matching abstract results and preservation of valid representations
For addition in the unreduced rational representation, chooseFor example, represents , precisely the sum of and . The short correctness argument uses nonzero denominators: and imply , preserving the representation invariant, and
Correct rational addition makes both paths agree; an invariant-preserving incorrect operation gives a different value
. Details. Now consider an incorrect implementation that uses addition on the numerators and multiplication on the denominators:It preserves the representation invariant for every valid input pair because its denominator is still . Yet represents , not the specified sum . Even perfect checks of the representation invariant before and after this call would miss the error: the result is a legal representation of the wrong rational number.
The incorrect operation also exposes an accidental dependence on representation. Replace by the equivalent state while keeping . The correct operation gives , still representing ; the incorrect operation gives , representing instead of its previous . A correct addition must yield the same abstract result for equivalent inputs, although its concrete outputs may differ. This is why checks against the formal specification should compare abstract values, including unreduced representations and representations with a negative denominator, rather than demand identical stored pairs.
The calculation assumes exact integers. An implementation with bounded storage must additionally specify how it handles products and sums outside its supported range; the mathematical argument alone does not establish its functional correctness. The bounded queue with encapsulation illustrates the corresponding need to account for returned status values and failed operations, alongside the abstract state transition.
Defensive copying 2026-10-24
Protect an owned mutable representation by copying mutable data received from clients and by returning independent copies instead of internal mutable objects. Copying only on entry leaves an accessor leak; copying only on exit leaves the constructor argument aliased. For an object containing only primitive fields, a field-by-field copy suffices. Nested mutable references can require a deep copy, immutable components or a stronger ownership contract.
The correctness argument follows aliases: after copying, no client-held reference reaches the owned mutable fields, and every public mutation goes through operations preserving the owner's representation invariant. Copying is one technique for encapsulation, not a substitute for deciding which state is meant to remain mutable.
Encapsulation (computer programming) Created 2026-10-13 Updated 2026-10-24
Encapsulation bundles related program state and operations or hides implementation details behind an interface. Encapsulation in object-oriented programming realizes this through objects and their permitted operations; encapsulation also applies to modules outside object-oriented programs.
The useful boundary is a promise: clients request operations through an API, and the implementation maintains a representation invariant. Instead of proving that every client updates several storage fields consistently, prove that the permitted operations preserve the representation invariant. Information hiding also leaves room to replace the data structure while keeping the client-facing behavior, a property called representation independence.
Bundling state and operations alone does not establish that promise. Representation exposure can let clients bypass the API. A
private annotation alone is not a security guarantee: it does not establish correctness of operations, isolation from hostile code or safe handling of shared mutable storage. The examples below concern sequential calls with no concurrent access and no client access to internal storage; they do not claim protection against arbitrary memory modification. List-based set representation 2026-10-31
Represent a finite set by a list of its elements. Allowing repeated elements makes set union cheap by list concatenation; imposing uniqueness requires membership checks. A representation sorted by a total order and containing no duplicates permits set union and set intersection by a simultaneous scan in linear time. These are different representation invariants for the same abstract set.
Object composition 2026-10-24
Object composition builds behavior by storing component software objects and delegating operations to them. A containing software object can expose a distinct object interface and control which operations affect additional state. Exclusive ownership or a specified reference-aliasing discipline may be needed to protect its representation invariant. Unlike subclass overrides, object methods of a separate component do not dynamically dispatch into the containing wrapper.
Object constructor 2026-10-24
An operation used when creating and initializing a software class instance. Construction should establish the representation invariant before ordinary clients can access the software object. Class inheritance and initialization order require care if construction invokes overridable object methods before subclass fields are initialized.
Use two permanent stacks, and , and one temporary stack, . At operation boundaries is empty. Maintain the representation invariant that the deque, read from front to back, is the top-to-bottom contents of followed by the bottom-to-top contents of . Thus the tops of and are the two accessible ends. Maintain their sizes using two counters, requiring only additional storage in Big O notation.
Adding at the front pushes onto ; adding at the back pushes onto . Removing at an end whose permanent stack is nonempty simply pops that stack. If both permanent stacks are empty, report an empty deque.
- Move the top elements of onto .
- Move all remaining elements of onto .
- Move all elements of back onto .
- Pop and return the top of .
The parked elements are the back half of the deque; the unparked elements are the front half. Moving the front half onto reverses their stack order and exposes the correct front element. Parking and restoring the back half reverses it twice, preserving its original order in . The temporary stack is empty again. For a back removal with empty, exchange the roles of and throughout. Rebalance approximately half the elements, so both ends retain accessible elements after a large transfer.
For the amortized analysis, count each push or pop as one unit and use the potential method withInitially the deque is empty, so , and is always nonnegative. An ordinary insertion or removal costs one unit and changes the size difference by at most one, giving amortized cost at most .
For a rebalancing removal, let . The parked half makes two transfers per element and the other half makes one; each transfer is a pop and a push. Including the final removal, the actual cost isBefore rebalancing the absolute size difference is . Immediately after the split it is at most , and after the removal it is at most . HenceSize tests and counter updates change only these constants. Summing the amortized costs and using nonnegative final potential proves amortized running time for all four operations, with three stacks and additional storage. An individual rebalancing operation can still take linear time in the current size.
In the Observer pattern, an observable subject keeps registered observers behind a shared object interface. After a relevant update, the subject calls that object interface on each observer. Observers can register and unregister independently, and the subject needs no knowledge of their concrete software classes.
For this model-view-controller application,
DataList is the subject, while graph views are observers. After a successful insertion, a notification tells each registered view to redraw from the updated model. An invalid insertion leaves the model unchanged and needs no change notification. Calling observers only after restoring the representation invariant prevents views from seeing a half-completed insertion. HenceKeep storage private. Find the first entry whose horizontal coordinate is not smaller than the new one. Equality there means that the coordinate is already present; otherwise insertion at that position preserves strict ordering. Reject nonfinite coordinates, since a
NaN would make the required comparisons meaningless. This is an explicit finite-coordinate contract for a display application.[ref]Java 8 Double API documentation. isFinite(double)
The Observer pattern uses a small callback Java interface. With
import java.util.*;, the full implementation is:interface GraphObserver {
void changed(DataList source);
}
final class DataList implements Iterable<Point> {
private final List<Point> points;
private final List<GraphObserver> observers;
public DataList() {
points = new ArrayList<Point>();
observers = new ArrayList<GraphObserver>();
}
public void addObserver(GraphObserver observer) {
if (observer == null)
throw new IllegalArgumentException("null observer");
for (GraphObserver old : observers)
if (old == observer) return;
observers.add(observer);
}
public void removeObserver(GraphObserver observer) {
for (int i = 0; i < observers.size(); ++i) {
if (observers.get(i) == observer) {
observers.remove(i);
return;
}
}
}
public void addPoint(double x, double y) throws Exception {
if (!Double.isFinite(x) || !Double.isFinite(y))
throw new Exception("nonfinite coordinate");
int i = 0;
while (i < points.size() && points.get(i).getX() < x) ++i;
if (i < points.size() && points.get(i).getX() == x)
throw new Exception("duplicate x coordinate");
points.add(i, new Point(x, y));
List<GraphObserver> current =
new ArrayList<GraphObserver>(observers);
for (GraphObserver observer : current) observer.changed(this);
}
public Iterator<Point> iterator() {
List<Point> snapshot = new ArrayList<Point>(points.size());
for (Point p : points) snapshot.add(p.clone());
return Collections.unmodifiableList(snapshot).iterator();
}
}This is a sequential implementation. Callback object methods are required to return normally and not reenter
addPoint; they may change their registrations. Copying the registration list means such changes affect future notifications, while each observer present at the start of this notification gets exactly one call. Repeated registration of the same observer is ignored by object identity. Both signed zeros compare equal and therefore count as the same horizontal coordinate.For correctness, all old entries before position
i have smaller horizontal coordinates. If an entry at i exists after the duplicate check, it has a strictly larger coordinate. Inserting between these two groups preserves the representation invariant; rejecting a duplicate has no state effect. No client receives a stored mutable Point. ThusRepresent a wall by a list of rows indexed by height. Within each row keep brick placements sorted by their left coordinate, with disjoint occupied half-open intervals. The public
Brick in the paper is a mutable input specification; internal placements snapshot its width and colour, so later client edits cannot invalidate an existing wall. Empty intermediate rows cannot occur in a supportive wall with occupied rows above them.The following Java uses
import java.util.*; and import java.awt.Color;. Keep the source's Brick input software class. All other representation types are private nested software classes of Wall, which prevents clients from inserting directly into a row. The row(int y) query returns a detached row for the equality operation in part (e).final class Wall {
private static final class Placed {
final long x, end;
final Color colour;
Placed(long x, int width, Color colour) {
this.x = x;
this.end = x + width;
this.colour = colour;
}
}
private static final class Row {
private final List<Placed> bricks = new ArrayList<Placed>();
boolean contains(long x) {
for (Placed b : bricks) {
if (x < b.x) return false;
if (x < b.end) return true;
}
return false;
}
boolean canInsert(Placed b) {
for (Placed old : bricks)
if (b.x < old.end && old.x < b.end) return false;
return true;
}
void insert(Placed b) {
int i = 0;
while (i < bricks.size() && bricks.get(i).x < b.x) ++i;
bricks.add(i, b);
}
Row copy() {
Row r = new Row();
r.bricks.addAll(bricks);
return r;
}
// Insert the equality members from part (e) here.
}
private final List<Row> rows = new ArrayList<Row>();
public void addBrick(Brick b, int x, int y) throws Exception {
if (b == null || b.col == null || b.width <= 0 || y < 0)
throw new Exception("invalid brick or height");
// Snapshot mutable input. Long arithmetic protects x + width.
int width = b.width;
Color colour = new Color(b.col.getRGB(), true);
Placed placed = new Placed((long) x, width, colour);
if (y > rows.size()) throw new Exception("unsupported height");
Row target = y == rows.size() ? new Row() : rows.get(y);
if (!target.canInsert(placed)) throw new Exception("overlap");
if (y > 0) {
Row below = rows.get(y - 1);
if (!below.contains(placed.x) || !below.contains(placed.end - 1))
throw new Exception("unsupported end");
}
// All checks precede the first modification of this wall.
target.insert(placed);
if (y == rows.size()) rows.add(target);
}
public boolean contains(int x, int y) {
return y >= 0 && y < rows.size() && rows.get(y).contains((long) x);
}
public Object row(int y) {
if (y < 0) throw new IllegalArgumentException("negative row");
return y < rows.size() ? rows.get(y).copy() : new Row();
}
}Here
Placed instances and their captured Color values are immutable objects, so copying a row's outer list suffices to create a detached snapshot. Returning its static type as Object exposes just the equality operation needed below, without exposing a mutable row API. A fuller application could instead return an immutable row-view object interface.The empty list represents a valid supportive wall. A rejected insertion performs no wall update. On success, the overlap test establishes validity in the target row; all other rows are unchanged. The support checks establish support for the new brick; adding material cannot remove support from old bricks. Appending a row only at the current height count keeps the row representation contiguous. Integer overflow in a right endpoint is prevented by converting the horizontal coordinate to
long before adding the positive int width. For instance, a brick at Integer.MAX_VALUE can still have a mathematically meaningful right endpoint.A particularly transparent design uses six D flip-flops in a one-hot encoding. Let mean that face is displayed. Initialize and , and wire the next-state inputs as a ring:All six D flip-flops share the same active clock edge. Each pulse moves the single stored to the next position, giving the state-transition diagram cycle . The representation invariant “exactly one is high” holds after initialization and is preserved by rotation. Six D flip-flops are more than the three-bit theoretical minimum, but their simple wiring gives a complete implementation without requiring that minimum.
One-hot ring state register and the six lamp patterns, including the original opposite diagonals on faces 2 and 3
. Details. Decode the seven lamps by their positions, with denoting top, middle and bottom, and denoting left and right. Let be the center lamp. In the original figure, face 2 uses top-left and bottom-right, while face 3 uses top-right and bottom-left plus center; the two diagonals must therefore have different controls.[ref]
Functional programming, data structures and algorithms, procedural programming, and digital hardware examination paper by the University of Oxford (2005). Printed p. 6, Figure 1(b), faces 2 and 3
The required OR gate decoder isFor example, only the center is high in state , the first diagonal is high in state , and in state both outer columns are high while the center is low. This verifies all six layouts directly.To implement the switch behavior, use a rapid common clock signal and a sampled enable , high while the switch is pressed. Each next-state input is then selected between its advancing value and its own stored value:One multiplexer per D flip-flop implements that selection. While enabled the electronic dice advances; otherwise every D flip-flop reloads its own value and the display holds. The enable supplied to this synchronous design must be stable at sampling edges. A reset or preset facility must establish the specified one-hot initial state: an all-zero ring does not start itself.
With a rapid clock signal, uncertainty in human release timing makes the final face practically unpredictable. The sequential circuit itself is deterministic; this observation alone is not a proof that its six outcomes have equal probabilities.
Let be the two input lengths and suppose numeric comparisons cost constant time. The list-based set representation determines which representation invariant each answer must preserve.
For unsorted lists allowing repetition, retain every left-hand occurrence whose value appears on the right for set intersection, and use list concatenation for set union:
interR xs ys = [x | x <- xs, x `elem` ys]
unionR xs ys = xs ++ ysThe resulting lists represent exactly the desired sets; repeated entries are permitted. Membership by sequential search makes
interR take time complexity in the worst case. The list concatenation in unionR costs to build its copied left spine and shares ys; fully enumerating the resulting list costs .For unsorted, duplicate-free inputs, the same intersection keeps uniqueness, while the union retains
xs and appends only right-hand elements absent from xs:interU xs ys = [x | x <- xs, x `elem` ys]
unionU xs ys = xs ++ [y | y <- ys, not (y `elem` xs)]Neither filtered list has internal repetitions, and the filter in
unionU also excludes overlap with xs. Both operations have worst-case time complexity, customarily written when both lengths are positive. Using the original xs for each membership test avoids searching an ever-growing output.interS [] ys = []
interS xs [] = []
interS (x:xs) (y:ys)
| x < y = interS xs (y:ys)
| x > y = interS (x:xs) ys
| otherwise = x : interS xs ys
unionS [] ys = ys
unionS xs [] = xs
unionS (x:xs) (y:ys)
| x < y = x : unionS xs (y:ys)
| x > y = y : unionS (x:xs) ys
| otherwise = x : unionS xs ysWhen , sortedness proves that cannot occur anywhere in the right list, so it can be discarded from the set intersection or immediately emitted to the set union. The symmetric argument handles ; equal heads are consumed together. Each step consumes at least one input head, so both have worst-case time complexity. These bounds assume the sorted representation invariant is already established; sorting arbitrary inputs has its own cost.
| Representation | Set intersection | Set union, including output traversal |
|---|---|---|
| Unsorted, repetitions allowed | ||
| Unsorted, unique | ||
| Sorted, unique |
Use an Oberon record containing an active coefficient count and a bounded array of coefficients in ascending power order. A count of zero represents the zero polynomial; a count represents . Trailing zero coefficients are allowed, so the count need not be the degree of a polynomial plus one.
CONST Capacity = 1024;
TYPE Polynomial = RECORD
len: INTEGER;
coeff: ARRAY Capacity OF REAL
END;
PROCEDURE Horner(VAR p: Polynomial; x: REAL): REAL;
VAR i: INTEGER; value: REAL;
BEGIN
i := p.len; value := 0.0;
WHILE i > 0 DO
i := i-1;
value := p.coeff[i] + x*value
END;
RETURN value
END Horner;The representation invariant is , with only indices below
len significant. The parameter is passed by reference to avoid a full record copy; the procedure does not modify it.Let be the original coefficient count. At each guard test the loop invariant isThe empty sum is zero initially. If the old index is , after decrementing and updating,which preserves the loop invariant. The loop variant is , decreasing by one until zero. At exit,This is exactly the right-to-left nesting of Horner's method, matching the supplied right fold. It uses arithmetic operations and additional scalar storage.
REAL gives ordinary floating-point evaluation; the displayed identities specify the ideal arithmetic calculation, with the usual rounding in an actual floating-point implementation.


