SPECIFICATION AltSpec
INVARIANT AltInvariant