5.10. Lemmas with invokeOn🔗

Sometimes the fact you need is not a property of one call but a general rule: for every input, this holds. invokeOn turns a procedure's postconditions into a universally quantified fact over its inputs, using the given expression as the trigger. It declares a lemma, not something that runs.

procedure P(x: int): bool;

procedure pLemma(x: int)
  invokeOn P(x)
  opaque
  ensures P(x) ==> x >= 0;

That declares, once and for all, that P(x) ==> x >= 0 for every x, and arranges for the fact to fire whenever the term P(x) appears. Nothing calls pLemma.

An invokeOn procedure may not declare outputs, because an output would be unbound in the resulting quantified fact.