SPECIFICATION AltPgmSpec
INVARIANTS AltPgmTypeOK AltPgmInvariant