14. Predefined Language Environment (Annex A)

This chapter describes how SPARK 2014 treats the Ada predefined language environment and standard libraries, corresponding to appendices A through H of the Ada RM.

SPARK 2014 programs are able to use much of the Ada predefined language environment and standard libraries. The standard libraries are not necessarily mathematically, formally proven in any way, unless specifically stated, and should be treated as tested code.

In addition many standard library subprograms have checks on the consistency of the actual parameters when they are called. If they are inconsistent in some way they will raise an exception. It is strongly recommended that each call of a standard library subprogram which may raise an exception due to incorrect actual parameters should be immediately preceded by a pragma Assert to check that the actual parameters meet the requirements of the called subprogram. Alternatively the called subprogram may be wrapped in a user defined subprogram with a suitable precondition. Examples of these approaches are given in The Package Strings.Maps (A.4.2).

No checks or warnings are given that this protocol is followed. The onus is on the user to ensure that a library subprogram is called with consistent actual parameters.

14.1. The Package Standard (A.1)

SPARK 2014 supports all of the types, subtypes and operators declared in package Standard. The predefined exceptions are considered to be declared in Standard, but their use is constrained by other language restrictions.

14.2. The Package Ada (A.2)

No additions or restrictions.

14.3. Character Handling (A.3)

14.3.1. The Packages Characters, Wide_Characters, and Wide_Wide_Characters (A.3.1)

No additions or restrictions. As in Ada, the wide character sets provided are SPARK 2014 tool, compiler and platform dependent.

14.3.2. The Package Characters.Handling (A.3.2)

No additions or restrictions.

14.3.3. The Package Characters.Latin_1 (A.3.3)

No additions or restrictions.

14.3.4. The Package Characters.Conversions (A.3.4)

No Additions or restrictions.

14.3.5. The Package Wide_Characters.Handling (A.3.5)

No additions or restrictions.

14.3.6. The Package Wide_Wide_Characters.Handling (A.3.6)

No additions or restrictions.

14.4. String Handling (A.4)

No additions or restrictions.

14.4.1. The Package Strings (A.4.1)

No additions or restrictions.

The predefined exceptions are considered to be declared in Stings, but their use is constrained by other language restrictions.

14.4.2. The Package Strings.Maps (A.4.2)

  1. The type declaration Character_Mapping_Function is not in SPARK 2014 and cannot be referenced within SPARK 2014 program text.

The function To_Mapping may raise the exception Translation_Error if its actual parameters are inconsistent. To guard against this exception each call of To_Mapping should be immediately preceded by an assert statement checking that the actual parameters are correct.

Examples

--  From the Ada RM for To_Mapping: "To_Mapping produces a
--  Character_Mapping such that each element of From maps to the
--  corresponding element of To, and each other character maps to
--  itself. If From'Length /= To'Length, or if some character is
--  repeated in From, then Translation_Error is propagated".

--  Each call should be preceded with a pragma Assert, checking the
--  actual parameters, of the form:
pragma Assert (Actual_From'Length = Actual_To'Length and then
                 (for all I in Actual_From'Range =>
                    (for all J in Actual_From'Range =>
                       (if I /= J then Actual_From (I) /= Actual_From (J)))));
CM := To_Mapping (From => Actual_From,
                  To   => Actual_To);

--  Alternatively To_Mapping could be wrapped in a user defined
--  subprogram with a suitable precondition and used to call
--  To_Mapping indirectly.  For example:
function My_To_Mapping (From, To : in Character_Sequence)
                       return Character_Mapping
  with Pre => (From'Length = To'Length and then
                 (for all I in From'Range =>
                    (for all J in From'Range =>
                       (if I /= J then From (I) /= From (J)))));
is
begin
   return Ada.Strings.Maps.To_Mapping (From, To);
end My_To_Mapping;

14.4.3. Fixed-Length String Handling (A.4.3)

  1. Translate (with Maps.Character_Mapping_Function formal parameter) is not callable from SPARK 2014 as it has a an access to function type parameter.

All other subprograms may be called but the subprograms Move, Index, Count (with a mapping formal parameter), Find_Token, Replace_Slice, Insert, Overwrite, Head (with Justify formal parameter), Tail (with Justify formal parameter) may raise an exception if they are called with inconsistent actual parameters. Each call of these subprograms should be preceded with a pragma Assert to check that the actual parameters are consistent.

14.4.4. Bounded-Length String Handling (A.4.4)

  1. The subprograms Index, Count and Translate with Maps.Character_Mapping_Function formal parameters are not callable from SPARK 2014.

The other subprograms in Bounded-Length String Handling are callable from SPARK 2014 program texts but many of them may raise an exception if they are called with inconsistent actual parameters. Each call of these subprograms should be preceded with a pragma Assert to check that the actual parameters are consistent.

14.4.5. Unbounded-Length String Handling (A.4.5)

  1. The type String_Access and the procedure Free are not in SPARK 2014 as they require access types and cannot be denoted in SPARK 2014 program text.
  1. The subprograms Index, Count and Translate with Maps.Character_Mapping_Function formal parameters are not callable from SPARK 2014.

The function and procedure Unbounded_Slice both may propagate Index_Error if Low > Length(Source)+1 or High > Length(Source) and so every call to each of these subprograms should be immediately preceded by a pragma Assert of the form:

pragma Assert (Actual_Low  <= Length (Actual_Source) and
               Actual_High <= Length (Actual_Source));

14.4.6. String-Handling Sets and Mappings (A.4.6)

No additions or restrictions.

14.4.7. Wide_String Handling (A.4.7)

  1. The types Wide_String_Access and Wide_Character_Mapping_Function are not in SPARK 2014 nor are the subprograms which have formal parameters of these types and cannot be denoted in SPARK 2014 program texts.

Each call of a subprogram which may raise an exception if it is called with inconsistent actual parameters should be immediately preceded by a pragma Assert checking the consistency of the actual parameters.

14.4.8. Wide_Wide_String Handling (A.4.8)

  1. The types Wide_Wide_String_Access and Wide_Wide_Character_Mapping_Function are not in SPARK 2014 nor are the subprograms which have formal parameters of these types and cannot be denoted in SPARK 2014 program texts.

Each call of a subprogram which may raise an exception if it is called with inconsistent actual parameters should be immediately preceded by a pragma Assert checking the consistency of the actual parameters.

14.4.9. String Hashing (A.4.9)

No additions or restrictions.

14.4.10. String Comparison (A.4.10)

No additions or restrictions.

14.4.11. String Encoding (A.4.11)

The subprograms of this package are callable from SPARK 2014 but those that may raise an exception due to inconsistent parameters should have a pragma Assert confirming that the actual parameters are consistent immediately preceding each call of such a subprogram.

14.5. The Numerics Packages (A.5)

No additions or restrictions

14.5.1. Elementary Functions (A.5.1)

Most of the elementarty functions may raise an exception. The functions have no preconditions to guard against an exception being raised. The functions should be treated as tested code and call of an elementary function should be immediately preceded by a pragma assert in lieu of a precondition.

For instance a call to Log (X, Base) should be immediately preceded by the assert statement:

pragma Assert (X > 0  and Base > 1);

Even with such a guard certain elementary functions may raise a constraint error. The onus is on the user to ensure this does not happen or is handled in non-SPARK 2014 text in a manner compatible with SPARK 2014.

14.5.2. Random Number Generation (A.5.2)

The package Ada.Numerics.Float_Random and an instantiation of package Ada.Numerics.Discrete_Random is ostensibly in SPARK 2014 but the functions have side effects and should not be called from SPARK 2014 text.

14.6. Input-Output (A.6)

No additions or restrictions.

14.7. External Files and File Objects (A.7)

No additions or restrictions.

14.8. Sequential and Direct Files (A.8)

No additions or restrictions.

14.8.1. The Generic Package Sequential_IO (A.8.1)

An instantiation of Sequential_IO will ostensibly be in SPARK 2014 but in use it may give rise to flow-errors as the effect of reads and writes is not captured in the subprogram contracts. Calls to its subprograms may raise IO_Exceptions based on external events.

14.8.2. File Management (A.8.2)

No additions or restrictions.

14.8.3. Sequential Input-Output Operations (A.8.3)

No additions or restrictions.

14.8.4. The Generic Package Direct_IO (A.8.4)

An instantiation of Direct_IO will ostensibly be in SPARK 2014 but in use it may give rise to flow-errors as the effect of reads and writes is not captured in the subprogram contracts. Calls to its subprograms may raise IO_Exceptions based on external events.

14.8.5. Direct Input-Output Operations (A.8.5)

No additions or restrictions.

14.9. The Generic Package Storage_IO (A.9)

An instantiation of Storage_IO will ostensibly be in SPARK 2014 but in use it may give rise to flow-errors as the effect of reads and writes is not captured in the subprogram contracts. Calls to its subprograms may raise IO_Exceptions based on external events.

14.10. Text Input-Output (A.10)

No additions or restrictions.

14.10.1. The Package Text_IO (A.10.1)

Ada.Text_IO is ostensibly in SPARK 2014 except for the type File_Access and the functions which return this type. The use Ada.Text_IO may give rise to flow-errors as the effect of reads and writes is not captured in the subprogram contracts. The Ada.Text_IO.Get_Line functions should not be called as they have a side effect of reading data from a file and updating its file pointers. The subprograms Set_Input, Set_Output and Set_Error should not be called as they introduce an alias to the file passed as a parameter. Calls to the subprograms of Ada.Text_IO may raise IO_Exceptions based on external events.

14.10.2. Text File Management (A.10.2)

No additions or restrictions.

14.10.3. Default Input, Output and Error Files (A.10.3)

The subprograms Ada.Text_IO.Set_Input, Ada.Text_IO.Set_Output and Ada.Text_IO.Set_Error should not be called from SPARK 2014 program text as they introduce an alias of the file parameter.

14.10.4. Specification of Line and Page Lengths (A.10.4)

No additions or restrictions.

14.10.5. Operations on Columns, Lines and Pages (A.10.5)

No additions or restrictions.

14.10.6. Get and Put Procedures (A.10.6)

No additions or restrictions.

14.10.7. Input-Output of Characters and Strings (A.10.7)

The functions Ada.Text_IO.Get_Line should not be called from SPARK 2014 program text as the functions have a side effect of reading from a file.

14.10.8. Input-Output for Integer Types (A.10.8)

No additions or restrictions.

14.10.9. Input-Output for Real Types (A.10.9)

No additions or restrictions.

14.10.10. Input-Output for Enumeration Types (A.10.10)

No additions or restrictions.

14.10.11. Input-Output for Bounded Strings (A.10.11)

An instantiation of Bounded_IO will ostensibly be in SPARK 2014 but in use it may give rise to flow-errors as the effect of reads and writes is not captured in the subprogram contracts. Calls to its subprograms may raise IO_Exceptions based on external events.

14.10.12. Input-Output of Unbounded Strings (A.10.12)

Ada.Text_IO.Unbounded_IO is ostensibly in SPARK 2014 but in use it may give rise to flow-errors as the effect of reads and writes is not captured in the subprogram contracts. Calls to its subprograms may raise IO_Exceptions based on external events.

The functions Ada.Text_IO.Unbounded_IO.Get_Line should not be called from SPARK 2014 program text as the functions have a side effect of reading from a file.

14.11. Wide Text Input-Output and Wide Wide Text Input-Output (A.11)

These packages have the same constraints as was discussed for Ada.Text_IO.

14.12. Stream Input-Output (A.12)

Stream input and output is not supported by SPARK 2014 and the use of the package Ada.Streams.Stream_IO and the child packages of Ada.Text_IO concerned with streams is not permitted in SPARK 2014 program text.

14.13. Exceptions in Input-Output (A.13)

The exceptions declared in package Ada.IO_Exceptions which are raised by the Ada input-output subprograms are in SPARK 2014 but the exceptions cannot be handled in SPARK 2014 program text.

14.14. File Sharing (A.14)

File sharing is not permitted in SPARK 2014, since it may introduce an alias.

14.15. The Package Command_Line (A.15)

The package Command_Line is in SPARK 2014 except that the function Argument may propagate Constraint_Error. To avoid this exception each call to Argument should be immediately preceded by the assertion:

pragma Assert (Number <= Argument_Count);

where Number represents the actual parameter to the function Argument.

14.16. The Package Directories (A.16)

The package Directories is ostensibly in SPARK 2014 but in use it may give rise to flow-errors as the effect of reads and writes is not captured in the subprogram contracts. Calls to its subprograms may raise IO_Exceptions based on external events.

14.17. The Package Environment_Variables (A.17)

The package Environment_Variables is ostensibly mostly in SPARK 2014 but in use it may give rise to flow-errors as the effect of reads and writes is not captured in the subprogram contracts. Calls to its subprograms may raise IO_Exceptions based on external events.

The procedure Iterate is not in SPARK 2014.

14.18. Containers (A.18)

The standard Ada container libraries are not supported in SPARK 2014.

An implementation may choose to provide alternative container libraries whose specifications are in SPARK 2014 and are intended to support formal verification.

14.19. The Package Locales (A.19)

No additions or restrictions.

14.20. Interface to Other Languages (Annex B)

This section describes features for mixed-language programming in SPARK 2014, covering facilities offered by Ada’s Annex B.

Package Interfaces can be used in SPARK 2014, including its intrinsic “Shift” and “Rotate” functions.

Other packages are not directly supported.

The pragma Unchecked_Union is not permitted in SPARK 2014.

14.21. Systems Programming (Annex C)

This section describes features for systems programming in SPARK 2014, covering facilities offered by Ada’s Annex C.

Almost all of the facilities offered by this Annex are out of scope for SPARK 2014 and so are not supported.

14.21.1. Pragma Discard_Names (C.5)

Pragma Discard_Names is not permitted in SPARK 2014, since its use can lead to implementation defined behaviour at run time.

14.21.2. Shared Variable Control (C.6)

The following restrictions are applied to the declaration of volatile types and objects in SPARK 2014:

Legality Rules

  1. A volatile representation aspect may only be applied to an object_declaration or a full_type_declaration.
  1. A type which is not effectively volatile shall not have a volatile subcomponent.
  1. A discriminant shall not be volatile.
  1. Neither a discriminated type nor an object of such a type shall be volatile.
  1. Neither a tagged type nor an object of such a type shall be volatile.
  1. An effectively volatile object shall only be declared at library-level.

14.22. Real-Time Systems (Annex D)

SPARK 2014 supports the parts of the real-time systems annex that comply with the Ravenscar profile (see Ada RM D.13) or the Extended Ravenscar profile (see docs.adacore.com/gnathie_ug-docs/html/gnathie_ug/gnathie_ug/the_predefined_profiles.html#the-extended-ravenscar-profiles). See section Tasks and Synchronization.

14.23. Distributed Systems (Annex E)

SPARK 2014 does not support the distributed systems annex.

14.24. Information Systems (Annex F)

The Machine_Radix aspect and attribute are permitted in SPARK 2014.

The package Ada.Decimal may be used, although it declares constants whose values are implementation defined.

The packages Ada.Text_IO.Editing and its “Wide” variants are not directly supported in SPARK 2014.

14.25. Numerics (Annex G)

This section describes features for numerical programming in SPARK 2014, covering facilities offered by Ada’s Annex G.

Packages declared in this Annex are usable in SPARK 2014, although many details are implementation defined.

Implementations (both compilers and verification tools) should document how both strict mode and relaxed mode are implemented and their effect on verification and performance.

14.26. High Integrity Systems (Annex H)

SPARK 2014 fully supports the requirements of Ada’s Annex H.