6.6. Exceptional frames🔗

modifies at the top level frames the normal return. A modifies inside a case frames that case's throwing path: it names the locations that may change when the procedure throws for that reason.

composite Cell {
  value: int
}
composite Err {}

procedure doWork(c: Cell, logCell: Cell, fail: bool) returns (r: int)
  throws (e: Err)
  opaque
  modifies c
  throwsOn fail {
    modifies logCell
  }
{
  if fail then {
    logCell#value := 1;
    var e: Err := new Err;
    throw e
  };
  c#value := 42;
  r := 0
};

Only c may change on the normal path, and only logCell when it throws because fail. All frames are checked against the body and assumed at call sites, a case's modifies accepts the same targets the top-level one does including field-granular ones (modifies logCell#value), and an object allocated inside the body is exempt from all of them.

Because each case carries its own frame, a procedure that writes different locations for different reasons can say so — one case each — rather than declaring only their union. A caller that rules out one case can then conclude the others' targets are unchanged.

Two things to keep in mind. Guards are not checked for overlap: if two can hold at once both frames apply, and a caller gets only their intersection, which is rarely what was meant. And framing a throwing path means naming its condition, so a procedure whose throwing condition cannot be stated — one that propagates a callee's exception, say — has to leave that path unframed by stating no case.