% program
  program[varCount: nat] : DATATYPE
  BEGIN
    IMPORTING bexpression[varCount], State[varCount]
    while(g: bexpression, body: program, inv:[state->bool]): while?
    asgn(varIndex: below(varCount), e: expression): asgn?
    seq(p1, p2:program): seq?
  END program