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.
New to topics? Read the docs here!