Frame condition
= Frame condition
A clause stating which parts of a <program state> an operation preserves. A query's returned value alone does not prohibit it from also mutating the receiver; a binary update's result equation alone does not preserve its distinct operand. Explicit <frame conditions> rule out these behaviors and make substitution and composition arguments possible.