Pragmas and Aspects#

pragma Pragma_Name;
pragma Pragma_Name(<argument list>);

with Aspect_Name1,
     Aspect_Name2 => <aspect definition>;
-- Attributes may be specified
for Entity_Name1'Attribute_Designator use <expression>;
for Entity_Name2'Attribute_Designator use <name>;

Aspects such as No_Return that have a simple boolean value may elide it as with Aspect_Name1. Most pragmas in modern Ada should instead be used via aspects except where there is no equivalent aspect, such as with Assert or Suppress.

Aspects for subprograms and types are never repeated and should (in order) go on the:

Specification
Stub
Body

Aspects will often break the linear order of evaluation rule by necessity, but they are only elaborated when the type is frozen.

Contracts#

Contracts are a method for defining and enforcing rules that are laid out for entities such as subprograms, tasks and types. Should any of these rules be broken, an exception is raised. Pre- and post-conditions may be set for a subprogram, impact on global state and invariant properties of a type may all be specified. Contracts are laid out as aspects for an entity.

The aspects relating to contracts all require boolean expressions.

Pre / Pre'Class
Post / Post'Class
Type_Invariant / Type_Invariant'Class
Static_Predicate
Dynamic_Predicate
Global / Global'Class
Stable_Properties
Nonblocking

Ada2022

Global, Global'Class, Stable_Properties and Nonblocking are only available from Ada2022.

Assertion policies may be set for each individual aspect: pragma Assertion_Policy(Pre => Check, Post => Ignore);

Useful attributes for contracts

'Old: Can be used for postconditions and it gives the value of an object on entry into the subprogram. It can be useful to track changes such as those to in out parameters and global variables or to check that certain fields of an out parameter have not been tampered with. 'Old can generally be applied to any value, but certain conditional structures relying on short circuit forms are illegal.
'Result: In the case of a postcondition, the result returned by a function F is accessed via F'Result.

Preconditions and Postconditions#

Preconditions (Pre) and postconditions (Post) are controlled via the same mechanism as the assert pragma which also allows them to be turned off in the same way with Assertion_Policy. As their names imply, checks are done upon calling a subprogram and returning from a subprogram respectively.

type Stack is private;

function Is_Empty(S: Stack) return Boolean;
function Is_Full (S: Stack) return Boolean;

function Push(S: Stack) return Integer
   with Pre  => not Is_Full(S),
        Post => not Is_Empty(S);

function Pop(S: Stack) return Integer
   with Pre  => not Is_Empty(S),
        Post => not Is_Full(S);

They are not allowed for null procedures in order to allow all null procedures to be equivalent, but Pre'Class and Post'Class for tagged types may be used for null procedures.

When calling a subprogram that has contracts, the calling site is obligated to meet the preconditions and, after the subprogram has completed, the postconditions may then be assumed following the calling site. The inverse of this is then that the subprogram is allowed to assume the preconditions and it is obligated to ensure the postconditions.

Perspective	Precondition	Postcondition
Caller	Obligation	Assumption
Body	Assumption	Obligation

Ada2022

In Ada2022, pre- and postconditions can also be applied to access-to-subprogram types:

type Positive_Input_Function is access function(X: Float) return Float
   with Pre => X >= 0.0;
type Negative_Return_Function is access function(X: Float) return Float
   with Post => Negative_Return_Function'Result < 0.0;

Class-Wide Preconditions and Postconditions#

When inheriting a subprogram, the pre- and postconditions are also inherited for primitive operations. Overriding them does not carry over the pre- and postconditions, however, and so they may not be applied to abstract subprograms because they do not have bodies and will have to be overridden.

Pre'Class and Post'Class act in a similar way to the standard versions, but apply to the entire class. They are inherited by their children and cannot be overridden. Although they cannot be overridden, extra 'Class pre- and postconditions may be added on for children in the subtree. This allows for a subprogram to have multiple pre- or postconditions:

procedure Do_Something(X: Shape)    with -- ...
procedure Do_Something(X: Circle)   with -- ...
procedure Do_Something(X: Cylinder) with -- ...

-- These could potentially lead to many pre- and postconditions
Pre'Class for Shape
Pre'Class for Circle
Pre for Cylinder

Post'Class for Shape
Post'Class for Circle
Post for Cylinder

Initial Conditions#

Ada2022 only

Default_Initial_Condition may be applied to a private type or private type extension in order to set a condition that must hold true following the initialisation of an object. This follows any Initialize for a controlled type.

-- Ensure that any declaration of a `T` starts out empty.
type T is new Abstract_T with private
   with Default_Initial_Condition => Is_Empty(T);

Multiple Inheritance#

Multiple inheritance can complicate matters with contracts. In the case of preconditions, they are combined with or (thus weakening) and, in the case of postconditions, they are combined with and (thus strengthening).

type T is new P and G1 and G2;

overriding procedure Op(X: T);
-- This allows potentially for the following implicit contracts:
-- Pre'Class  for P, G1 and G2
-- Post'Class for P, G1 and G2

This procedure potentially has implicit pre- and postconditions for each of P'Class, G1'Class and G2'Class for any one subprogram. Any 'Class contracts from them will be automatically inserted for Op(X: T) by the compiler. A postcondition list might be: Post => Post_P and Post_G1 and Post_G2 and a fourth one may also be added onto T’s overload. Preconditions are the same except that they would be joined via or: Pre => Pre_P or Pre_G1 or Pre_G2.

Type Invariants#

Type invariants are properties of types that are given via aspects and can be assumed to be true. Invariants are only meaningful on private types and only apply to the external view of the type. This allows a value to be manipulated however you wish in private subprograms and only then will the invariant be checked when the object is returned back out of the private scope.

type T is -- ...
   with Type_Invariant       => Is_X_True(T),
        Type_Invariant'Class => Is_Y_True(T);

The invariant may be given on either the private or full definitions and it is checked for the type (or a part of it):

After a default initialisation
After a conversion
After calling 'Read or 'Input
After an external subprogram call involving it

Type_Invariant and Type_Invariant'Class are similar to Post and Post'Class respectively. The idea with the pre and post being inside and outside of the package (where it is normally inside and outside of a subprogram) and the 'Class variation for tagged types is inherited. Note that inherited operations (or just generally where view conversions are necessary) may involved non-'Class invariant checks that belong to parent types.

Subtype Predicates#

Subtype predicates are two aspects that can be added to types and subtypes: Static_Predicate and Dynamic_Predicate. There is no requirement for 'Class versions as predicates are naturally inherited and derived types will check their parent’s predicates.

subtype Prime_Teens is Integer range 13 .. 19
   with Static_Predicate => Prime_Teens in 13 | 17 | 19;

subtype Letter is Character
   with Static_Predicate => Letter in 'a' .. 'z' | 'A' .. 'Z';

subtype Even_Integer is Integer
   with Dynamic_Predicate => Even_Integer mod 2 = 0;

Static predicates may only be used when the test is (including, of course, boolean operators):

A membership selection (piped values).
A case expression where dependent expressions are static.
A predefined operation (=, /=, <, <=, > and >=).
A static expression.

Both types with dynamic and static predicates have restrictions on where they may be used. For example, Static predicates may not be used as an array index type to create an array with holes and dynamic predicates may not be used as a for-loop value (for X in Even_Integer -- ...). The 'First, Last and Range attributes do not work with predicates (although 'Succ and 'Pred do), but the attributes 'First_Valid and 'Last_Valid work with ranges defined by predicates.

Subtype predicates are checked on:

Assignment
A conversion
Parameter passing
Initialization

Record Fields

Beware that using predicates detached from their actual type can bypass the intended usage:

type T is record
   X: Integer;
end record;
subtype ST is T
   with Dynamic_Predicate => ST.X mod 2 = 0;

With some object of type O: ST, O.X := 3 will not be checked because T.X is simply of type Integer which is not directly subject to the predicate for ST. The predicate would only be checked if the record as a whole were modified.

Messages#

The aspect Predicate_Failure may be used in order to use specific messages for failures. When the predicate fails, either the error message is used for an assertion if a string is used or you can manually raise a specific exception to be raised.

type TT is new T
   with Dynamic_Predicate => Check(TT),
        Predicate_Failure => "Check on TT failed";
-- Or with a more specific exception
type TT is new T
   with Dynamic_Predicate => Check(TT),
        Predicate_Failure => raise My_Error with "Check on TT failed";

Global State#

Ada2022 only

The aspect Global is used to indicate which global objects may be manipulated. The global values are marked with in, out and in out in a similar way that subprogram parameters are. When package-scoped globals are used, they are simply referenced via the package name.

package P is 
   State: Integer;

   -- Op1 may write to global variable State.
   procedure Op1 with Global => out State;

   -- Op2 may read from and write to State and may
   -- also use global variables defined in P's body.
   procedure Op2 with Global => (in out State; in P);
end P;

Global aspects may also be given to packages in which case they apply to each subprogram in the package. Global aspects given to subprograms within such a unit will then override any inherited global aspects.

In addition to in, out and in out, globals may be annotated with null, all and synchronized. Global => null means that not access to global variables is permitted. Global => all means that there is no restriction on reading global variables (implicit in) and it can annotated with out and in out for write access to all and read/write access to all respectively. Finally, synchronized, is the same as all except that access is only permitted to values that can be accessed by several tasks or threads without interference.

A library-level package with the aspect Pure sets the default of the Global aspect to null.

TODO

overriding parameters in global annotations (AARM High Integrity Annex)
No_Unspecified_Globals and No_Hidden_Indirect_Globals

Stable Properties#

TODO

Stable_Property and Stable_Property'Class

Default Values#

Default_Value

Used to set the default value for scalar types.

type My_Enum is (A, B, C)
   with Default_Value => C;

Default_Component_Value

Used to set the default value of the components for an array of scalar types.

type My_Array is (Integer range <>) of Float
   with Default_Component_Value => 77.0;

Ada2022

Default_Iterator :

Default_Storage_Pool :

Runtime Checks#

AARM

The pragmas Suppress and Unsuppress may be used to enable and disable certain runtime checks. Unsuppress says that they must not be turned off while Suppress says that they may be turned off (but might not be due to checks done by the hardware).

pragma Suppress(Access_Check);
pragma Unsuppress(Access_Check);

Runtime Check	Description of the Check
`Access_Check`	If an access value is null when dereferencing or converting to `not null` type.
`Discriminant_Check`	If a discriminant value is consistent with the component being accessed.
`Division_Check`	If the denominator of `/`, `rem` and `mod` is zero.
`Index_Check`	If an index or slice is in an array’s range.
`Length_Check`	If two array’s components match.
`Overflow_Check`	If there is numeric overflow.
`Range_Check`	If scalar values are within the base range of their type.
`Tag_Check`	If tags are equal when dispatching.
`Accessibility_Check`	If the accessibility levels of entities or views are correct.
`Allocation_Check`	If the master of a task is not yet completed (or some dependents are not yet completed) for an allocator.
`Elaboration_Check`	If the body of a unit has been elaborated.
`Program_Error_Check`	Other language-defined checks that raise a `Program_Error`.
`Storage_Check`	If space is available for a storage pool, task or subprogram.
`All_Checks`	A union of all the above checks.
`Tasking_Check`	If a task has activated successfully and a called task has not terminated.

There are also checks for certain language features:

Calendar_Assertion_Check (Calendar)
Characters_Assertion_Check (Characters, Wide_Characters and Wide_Wide_Characters)
Containers_Assertion_Check (Containers)
Interfaces_Assertion_Check (Interfaces)
IO_Assertion_Check (Sequential_IO, Direct_IO, Text_IO, Wide_Text_IO, Wide_Wide_Text_IO, Storage_IO, Streams.Stream_IO, and Directories)
Numerics_Assertion_Check (Numerics)
Strings_Assertion_Check (Strings)
System_Assertion_Check (System)

Assertions#

AARM

pragma Assert(My_Boolean);
pragma Assert(My_Boolean, "Assertion message");

-- This is the equivalent of
if not My_Boolean then
   Ada.Exceptions.Assert("Assertion Message");
   -- Which is the same as:
   raise Ada.Exceptions.Assertion_Error with "Assertion message";
end;

Note that excluding the assertion message is not the same as using an empty string. Without an explicit message, the assertion message is implementation defined.

Assertion Policies#

pragma Assertion_Policy(Check);
pragma Assertion_Policy(Ignore);

Only two policies are defined by the language: Check and Ignore. Further policies may be defined by the implementation.

No_Return#

May only be applied to functions from Ada2022.

The No_Return aspect asserts that the subprogram will never return. The implementation will be able to assume that any calls to the subprogram will not return (and may therefore perform optimisations based on this assumption) and control may only leave the subprogram via the propagation of exceptions. A Program_Error is raised if there is an attempt to return and any subprograms that are No_Return may only be overridden by a subprogram that also is.

procedure My_Quit with No_Return;

Elaboration#

The pragmas Elaborate and Elaborate_All may be used to ensure that the bodies of certain packages have been elaborated before proceeding. This may be necessary if a Program_Error is raised or simply to prevent ambiguities. The pragma may be used with private with clauses, but not with limited with clauses. Elaborate_All transitively ensures that all packages needed by the named package are also elaborated before the current one.

use A_Package; pragma Elaborate(A_Package); -- Must be in the context clause

package Current_Package is
   -- ... (using A_Package)
end Current_Package;

Another method is to use the Elaborate_Body aspect to ensure that the package is elaborated immediately after the specification.

package My_Package
   with Elaborate_Body is
   -- ...
end My_Package;

Other aspects relating to elaboration are Preelaborate, Pure, and Preelaborable_Initialization:

Preelaborate means that the unit can be elaborated before the program executes (ie, it is all static data). It is not required that it is elaborated and is up to the implementation to provide this, but it will provide that all units marked Preelaborate are elaborated before those not marked as such. Preelaborate units may only depend on other Preelaborate units.
Pure indicates that the unit is open to Preelaborate and that it also does not contain any state. A package may also be marked as Pure with pragma Pure(My_Package);. Pure units may only depend on other Pure units.
Preelaborable_Initialization is used for private types depended on from another Preelaborate package in order to promise that the type will indeed be able to be Preelaborate.

Language-Defined Pragmas#

AARM

pragma Admission_Policy(policy_identifier);
pragma All_Calls_Remote[(library_unit_name)];
pragma Assert([Check =>] boolean_expression[, [Message =>] string_expression]);
pragma Assertion_Policy(policy_identifier);
pragma Assertion_Policy(assertion_aspect_mark => policy_identifier
                     {, assertion_aspect_mark => policy_identifier});
pragma Asynchronous(local_name);
pragma Atomic(local_name);
pragma Atomic_Components(array_local_name);
pragma Attach_Handler(handler_name, expression);
pragma Conflict_Check_Policy (policy_identifier[, policy_identifier]);
pragma Convention([Convention =>] convention_identifier,[Entity =>] local_name);
pragma CPU(expression);
pragma Default_Storage_Pool(storage_pool_indicator);
pragma Detect_Blocking;
pragma Discard_Names[([On => ] local_name)];
pragma Dispatching_Domain(expression);
pragma Elaborate(library_unit_name{, library_unit_name});
pragma Elaborate_All(library_unit_name{, library_unit_name});
pragma Elaborate_Body[(library_unit_name)];
pragma Export([Convention =>] convention_identifier, [Entity =>] local_name
              [, [External_Name =>] external_name_string_expression]
              [, [Link_Name =>] link_name_string_expression]);
pragma Generate_Deadlines;
pragma Import([Convention =>] convention_identifier, [Entity =>] local_name
              [, [External_Name =>] external_name_string_expression]
              [, [Link_Name =>] link_name_string_expression]);
pragma Independent(component_local_name);
pragma Independent_Components(local_name);
pragma Inline(name{, name});
pragma Inspection_Point[(object_name{, object_name})];
pragma Interrupt_Handler(handler_name);
pragma Interrupt_Priority[(expression);]
pragma Linker_Options(string_expression);
pragma List(identifier);
pragma Locking_Policy(policy_identifier);
pragma No_Return(subprogram_local_name procedure_local_name{, subprogram_local_name procedure_local_name});
pragma Normalize_Scalars;
pragma Optimize(identifier);
pragma Pack(first_subtype_local_name);
pragma Page;
pragma Partition_Elaboration_Policy(policy_identifier);
pragma Preelaborable_Initialization(direct_name);
pragma Preelaborate[(library_unit_name)];
pragma Priority(expression);
pragma Priority_Specific_Dispatching(policy_identifier, first_priority_expression, last_priority_expression);
pragma Profile(profile_identifier{, profile_pragma_argument_association});
pragma Pure[(library_unit_name)];
pragma Queuing_Policy(policy_identifier);
pragma Relative_Deadline(relative_deadline_expression);
pragma Remote_Call_Interface[(library_unit_name)];
pragma Remote_Types[(library_unit_name)];
pragma Restrictions(restriction{, restriction});
pragma Reviewable;
pragma Shared_Passive[(library_unit_name)];
pragma Storage_Size(expression);
pragma Suppress(identifier);
pragma Task_Dispatching_Policy(policy_identifier);
pragma Unchecked_Union(first_subtype_local_name);
pragma Unsuppress(identifier);
pragma Volatile(local_name);
pragma Volatile_Components(array_local_name);

Language-Defined Aspects#

AARM

Aspect	Description
`Address`	Machine address of an entity.
`Aggregate`	Mechanism to define user-defined aggregates.
`Alignment(object)`	Alignment of an object.
`Alignment(subtype)`	Alignment of a subtype.
`All_Calls_Remote`	All indirect or dispatching remote subprogram calls, and all direct remote subprogram procedure calls, should use the Partition Communication Subsystem, even if they are local.
`Allows_Exit`	An indication of whether a subprogram will operate correctly for arbitrary transfers of control.
`Asynchronous`	Remote procedure calls are asynchronous; the caller continues without waiting for the call to return.
`Atomic`	Declare that a type, object, or component is atomic.
`Atomic_Components`	Declare that the components of an array type or object are atomic.
`Attach_Handler`	Protected procedure is attached to an interrupt.
`Bit_Order`	Order of bit numbering in a record_representation_clause.
`Coding`	Internal representation of enumeration literals. Specified by an enumeration_representation_clause, not by an aspect_specification.
`Component_Size`	Size in bits of a component of an array type.
`Constant_Indexing`	Defines function(s) to implement user-defined indexed_components.
`Convention`	Calling convention or other convention used for interfacing to other languages.
`CPU`	Processor on which a given task, or calling task for a protected operation, should run.
`Default_Component_Value`	Default value for the components of an array-of-scalar subtype.
`Default_Initial_Condition`	A condition that will hold true after the default initialization of an object.
`Default_Iterator`	Default iterator to be used in for loops.
`Default_Storage_Pool`	Default storage pool for a generic instance.
`Default_Value`	Default value for a scalar subtype.
`Discard_Names`	Requests a reduction in storage for names associated with an entity.
`Dispatching`	Generic formal parameters used in the implementation of an entity.
`Dispatching_Domain`	Domain (group of processors) on which a given task should run.
`Dynamic_Predicate`	Condition that will must hold true for objects of a given subtype; the subtype is not static.
`Elaborate_Body`	A given package will must have a body, and that body is elaborated immediately after the declaration.
`Exclusive_Functions`	Specifies mutual exclusion behavior of protected functions in a protected type.
`Export`	Entity is exported to another language.
`External_Name`	Name used to identify an imported or exported entity.
`External_Tag`	Unique identifier for a tagged type in streams.
`Full_Access_Only`	Declare that a volatile type, object, or component is full access.
`Global`	Global object usage contract.
`Global'Class`	Global object usage contract inherited on derivation.
`Implicit_Dereference`	Mechanism for user-defined implicit `.all`.
`Import`	Entity is imported from another language.
`Independent`	Declare that a type, object, or component is independently addressable.
`Independent_Components`	Declare that the components of an array or record type, or an array object, are independently addressable.
`Inline`	For efficiency, Inline calls are requested for a subprogram.
`Input`	Function to read a value from a stream for a given type, including any bounds and discriminants.
`Input'Class`	Function to read a value from a stream for a the class-wide type associated with a given type, including any bounds and discriminants.
`Integer_Literal`	Defines a function to implement user-defined integer literals.
`Interrupt_Handler`	Protected procedure may be attached to interrupts.
`Interrupt_Priority`	Priority of a task object or type, or priority of a protected object or type; the priority is in the interrupt range.
`Iterator_Element`	Element type to be used for user-defined iterators.
`Iterator_View`	An alternative type to used for container element iterators.
`Layout(record)`	Layout of record components. Specified by a record_representation_clause, not by an aspect_specification.
`Link_Name`	Linker symbol used to identify an imported or exported entity.
`Machine_Radix`	Radix (2 or 10) that is used to represent a decimal fixed point type.
`Max_Entry_Queue_Length`	The maximum entry queue length for a task type, protected type, or entry.
`No_Controlled_Parts`	A specification that a type and its descendants do not have controlled parts.
`No_Return`	A subprogram procedure will not return normally.
`Nonblocking`	Specifies that an associated subprogram does not block.
`Output`	Procedure to write a value to a stream for a given type, including any bounds and discriminants.
`Output'Class`	Procedure to write a value to a stream for a the class-wide type associated with a given type, including any bounds and discriminants.
`Pack`	Minimize storage when laying out records and arrays.
`Parallel_Calls`	Specifies whether a given subprogram is expected to be called in parallel.
`Parallel_Iterator`	An indication of whether a subprogram may use multiple threads of control to invoke a loop body procedure.
`Post`	Postcondition; a condition that will must hold true after a call.
`Post'Class`	Postcondition that applies to corresponding subprograms of descendant types inherited on type derivation.
`Pre`	Precondition; a condition that is expected to must hold true before a call.
`Pre'Class`	Precondition that applies to corresponding subprograms of descendant types inherited on type derivation.
`Predicate_Failure`	Action to be performed when a predicate check fails.
`Preelaborable_Initialization`	Declares that a type has preelaborable initialization.
`Preelaborate`	Code execution during elaboration is avoided for a given package.
`Priority`	Priority of a task object or type, or priority of a protected object or type; the priority is not in the interrupt range.
`Pure`	Side effects are avoided in the subprograms of a given package.
`Put_Image`	Procedure to define the image of a given type.
`Read`	Procedure to read a value from a stream for a given type.
`Read'Class`	Procedure to read a value from a stream for the class-wide type associated with a given type.
`Real_Literal`	Defines a function or functions to implement user-defined real literals.
`Record layout`	See Layout.
`Relative_Deadline`	Task or protected type parameter used in Earliest Deadline First Dispatching.
`Remote_Call_Interface`	Subprograms in a given package may be used in remote procedure calls.
`Remote_Types`	Types in a given package may be used in remote procedure calls.
`Shared_Passive`	A given package is used to represent shared memory in a distributed system.
`Size(object)`	Size in bits of an object.
`Size(subtype)`	Size in bits of a subtype.
`Small`	Scale factor for a fixed point type.
`Stable_Properties`	A list of functions describing characteristics that usually are unchanged by primitive operations of the type or an individual primitive subprogram.
`Stable_Properties'Class`	A list of functions describing characteristics that usually are unchanged by primitive operations of a class of types or a primitive subprogram for such a class.
`Static`	Specifies that an associated expression function can be used in static expressions.
`Static_Predicate`	Condition that will must hold true for objects of a given subtype; the subtype may be static.
`Storage_Pool`	Pool of memory from which new will allocate for a given access type.
`Storage_Size(access)`	Sets memory size for allocations for an access type.
`Storage_Size(task)`	Size in storage elements reserved for a task type or single task object.
`Stream_Size`	Size in bits used to represent elementary objects in a stream.
`String_Literal`	Defines a function to implement user-defined string literals.
`Synchronization`	Defines whether a given primitive operation of a synchronized interface will must be implemented by an entry or protected procedure.
`Type_Invariant`	A condition that will hold true for all objects of a type.
`Type_Invariant'Class`	A condition that will hold true for all objects in a class of types.
`Unchecked_Union`	Type is used to interface to a C union type.
`Use_Formal`	Generic formal parameters used in the implementation of an entity.
`Variable_Indexing`	Defines function(s) to implement user-defined indexed_components.
`Volatile`	Declare that a type, object, or component is volatile.
`Volatile_Components`	Declare that the components of an array type or object are volatile.
`Write`	Procedure to write a value to a stream for a given type.
`Write'Class`	Procedure to write a value to a stream for a the class-wide type associated with a given type.
`Yield`	Ensures that a callable entity includes a task dispatching point.