Syntax for assert statements

While a fact is used to force something to be true of the model, an assert is a claim that something must already be true due to the rest of the model. Assertions are verified (or falsified) using a check statement.

  assert name-of-assertion {
    // list of constraints
  }

  assert acyclic {
    no d: Dir | d in d.^contents
  }

Each assertion must have a name, since we will need to refer to them by name in check statements.