Required Annotations
	• global definitions in procedures • dependency relations in procedures • the inherit clause in a SPARK package declaration • the own variable clause in a SPARK package specification • the initialization annotation in a SPARK package specification