= Representation invariant
{title2=$I(r)$}
A <representation invariant> $I(r)$ specifies which concrete storage states $r$ are valid at the <API> boundary. Construction must establish it, and each completed operation must preserve it. Internal steps may temporarily violate it only while that state is inaccessible to observers; callbacks or concurrent access would require further reasoning.<6.005 Software Construction, Spring 2016/Reading 13: Abstraction Functions & Rep Invariants>[Reading 13, How to Establish Invariants: creation, preservation and absence of representation exposure]{ref}
The short proof pattern is <mathematical induction> on the number of completed calls: the initial state satisfies $I$; every permitted transition from an $I$-state ends in an $I$-state; hence every state observable through the <API> satisfies $I$. An unrestricted external write falls outside this argument.
Back to article page
