These annotations are used to express known (or presumed) features of the semantics of the specification, e.g., that an extension is `conservative', or that certain formulae are consequences of the specification. A set of semantic annotations has been proposed, but not yet decided.