Assumption directives provide invariants that specify additional information about the expected properties of the program that can optionally be used for optimization. An implementation may ignore this information without altering the behavior of the program. Different assumption directive formats facilitate definition of assumptions for a scope that is appropriate to each base language. The scope of a particular format is its assumption scope and is defined in the section that defines that format. If the invariants do not hold at runtime, the behavior is unspecified.