SPECIFICATION TPSpec
INVARIANT TPInvariant
PROPERTY Bar_AltSpec