SPECIFICATION Spec
INVARIANT TypeInvariant