A Generic LRU Cache

Problem

A library earns its keep by being usable without its caller ever having to know how it works inside. So the design question here is not "how do I implement LRU eviction" — it is "what four operations does a caller actually need, and what does each one promise?" The answer, settled before any implementation: put, get, contains, and size, generic over any key and value type, with reading a key counting as using it just as much as writing one does — a get has to refresh recency exactly like a put does, or the "L" in LRU is a lie.

Design as Contract

The public surface is deliberately small:

class Lru_Cache [K, V]
create
  make(capacity: Integer)
  require
    positive_capacity: capacity > 0
  do ... end
feature
  size(): Integer do ... end
  contains(key: K): Boolean do ... end
  get(key: K): ?V do ... end
  put(key: K, value: V) do ... end

[K, V] makes the cache generic over any key and value type — the eviction policy does not care what it is caching, so nothing about its implementation should either. get returns ?V, Nex's detachable-type syntax for "a V, or nothing" — a cache miss is represented in the type itself, not by a sentinel value the caller has to know to check for, and not by an exception for what is, for a cache, an entirely ordinary outcome.

The specification that matters most here, though, is not on any individual method — it is the class invariant, which states what must be true of every Lru_Cache at every moment control is not inside one of its own methods:

invariant
  within_capacity: map.size() <= capacity
  order_matches_map: order.length = map.size()

Two internal structures do the work — a Map[K, V] holding the values, and an Array[K] tracking recency, oldest first — and the invariant is the promise that they never disagree. Every method that touches either one is implicitly required to leave both invariant clauses true when it returns, which is a stronger specification than "here is what put does" written as prose: it is the actual condition the type checker and the runtime both hold every method to, on every call, for the life of the object.

Build

put is where the invariant does its clearest work. Overwriting an existing key must not grow the cache or evict anything; inserting a genuinely new key past capacity must evict before inserting, never after:

put(key: K, value: V) do
  if map.contains_key(key) then
    map.set(key, value)
    touch(key)
  else
    if map.size() >= capacity then
      evict_oldest()
    end
    map.set(key, value)
    order.add(key)
  end
ensure
  present: map.contains_key(key)
end

The ensure present postcondition is deliberately modest — just "the key you put is now in the cache" — because the harder guarantees already live in the invariant and apply automatically, on every call, without needing to be restated here. That division of labor is worth noticing: postconditions describe what changed as a result of this call; the invariant describes what stays true regardless of which call just ran.

Recency tracking is a single small helper, called from both get and the overwrite branch of put — the two places something becomes most-recently-used:

-- Move `key` to the most-recently-used end of `order`.
touch(key: K) do
  let idx: Integer := order.index_of(key)
  if idx >= 0 then
    order.remove(idx)
  end
  order.add(key)
end

evict_oldest() do
  if order.length > 0 then
    let oldest: K := order.get(0)
    order.remove(0)
    map.remove(oldest)
  end
end

order's front is always the next eviction candidate and its back is always the most recently touched key — an ordinary array used as a simple recency queue, no separate data structure needed at this scale. Nothing about eviction policy leaks outside these two private methods; a caller of put or get never has any reason to know order exists.

Test

Thirteen checks, each aimed at one specific claim the design makes rather than at the implementation's internals. Capacity eviction, with the exact recency rule this project cares about most — reading a key protects it from eviction just as writing one does:

let cache: Lru_Cache [String, Integer] := create Lru_Cache.make(3)
cache.put("a", 1)
cache.put("b", 2)
cache.put("c", 3)
cache.get("a")          -- touching "a" makes "b" the least-recently-used
cache.put("d", 4)
c.check("b evicted", "false", "" + cache.contains("b"))
c.check("a survives (was touched)", "true", "" + cache.contains("a"))

And the overwrite case, which a less careful implementation could easily get wrong by evicting on every put regardless of whether the key was already present:

cache.put("d", 40)
c.check("overwrite keeps size", "3", "" + cache.size())

A one-line capacity-1 case closes out the suite — a cache where every single put of a new key evicts something, which is the kind of boundary a generic algorithm's own logic should handle without a special case, and here does.

Takeaways

A class invariant can carry more of a specification than any individual method's own postcondition. State the relationship that must always hold between a class's fields once, as an invariant, and every method's own contract gets to stay modest, because the harder guarantee is already someone else's job — ensure present only ever has to say "the key you put is now in the cache," not re-derive what the invariant already promises. And a library whose only purpose is to be reused everywhere is easiest to trust when it depends on as little as possible: the fewer moving parts underneath it, the fewer ways it can surprise a caller who has never seen its implementation.

Chapter 4 also stays inside a single process with no I/O, but its interface is a much larger one than this cache's four methods: every expression a small language can express.