A topic in the Open Knowledge Graph — a free, open map of 15,290 topics and the order to learn them in.
The frame problem in program verification asks: how do you specify what a piece of code does NOT change? A function that increments a counter should leave all other variables and heap cells unchanged, but writing explicit "unchanged" clauses for everything the function does not touch is impractical and fragile. The frame problem forces verification frameworks to adopt conventions — modifies clauses, frame rules, or default-unchanged semantics — that let specifications focus on what changes while implicitly preserving everything else. Separation logic's frame rule is the most influential solution.
The frame problem originated in artificial intelligence (McCarthy and Hayes, 1969) as the question of how to specify the effects of actions without explicitly stating everything that does NOT change. The same problem arises in program verification: when you specify what a function does (its postcondition), how do you also specify what it leaves alone? A function that sorts an array should not modify a database connection, but writing "database connection unchanged" in every array function's specification is absurd. The frame problem is about managing this implicit preservation.
For programs with only local variables, the frame problem is mild. The statement `x := x + 1` syntactically reveals that only x changes; a verification tool can automatically conclude that y, z, and everything else is unchanged. But for heap-manipulating programs, the situation is far worse. The statement `*p := 5` modifies the memory cell at address p — but which cell is that? If p might alias q, then `*p := 5` might also change `*q`. Without knowing the aliasing relationships at every program point, you cannot determine what changed and what did not. The number of possible aliasing configurations grows combinatorially with the number of pointers, making explicit frame conditions intractable.
Practical verification tools use several strategies. Modifies clauses (used in Dafny, SPARK Ada, and Frama-C) require the programmer to list which variables or heap locations a function may change. The tool then automatically generates frame conditions asserting that everything outside the modifies set is preserved. This works well but requires the programmer to maintain accurate modifies sets, and for heap-manipulating code, expressing the modifies set precisely can be as hard as the verification itself.
Separation logic offers the most principled solution through its frame rule. A separation logic specification {P} C {Q} describes only the "footprint" of C — the specific heap cells it reads and writes. The frame rule says that any heap disjoint from this footprint (captured by the separating conjunction R in {P * R} C {Q * R}) is automatically preserved. The programmer never writes frame conditions at all; they simply specify what the function touches, and preservation of everything else follows from the logic's structure. This local reasoning principle is why separation logic revolutionized verification of pointer-manipulating programs and enabled tools like Infer to analyze code at industrial scale.
The frame problem connects to broader themes in specification methodology. A specification that describes only what changes is open-frame: it says what is true afterward but allows arbitrary changes elsewhere. A specification with a modifies clause or separation logic footprint is closed-frame: it implicitly constrains what did not change. Closed-frame specifications are far more useful because they enable modular reasoning — you can compose two functions' specifications without wondering whether one might have silently corrupted the other's data. Every serious verification framework must take a position on the frame problem, and the choice profoundly affects the framework's usability and scalability.