4.10. Holes and nondeterminism🔗

Two literals stand for a value the program does not determine. They differ in whether repeated evaluation agrees, and choosing the wrong one is a common source of confusion.

A deterministic hole <?> denotes one unknown-but-fixed value. Each hole site is a function of the enclosing procedure's inputs, so the same site reached with the same inputs yields the same value, while two different sites need not agree.

procedure unknownScore(x: int): int
{
  return <?>
};

This is what a front end should emit when it cannot translate a side-effect-free sub-expression: the analysis still runs, and the user sees your diagnostic rather than a cascade. Because a hole stands for a value, replacing an effectful expression with one silently drops the effect and can make an analysis prove something the original program does not satisfy.

A nondeterministic hole <??> takes a fresh unconstrained value at every evaluation, so distinct evaluations are independent:

procedure nondeterminism()
  opaque
{
  var x: int := <??>;
  var y: int := <??>;
  assert x == y      // not provable: the two are independent
};