SPECIFICATION SemAltSpec
INVARIANT SemAltInvariant