14. Predefined Language Environment (Annex A)
This chapter describes how SPARK treats the Ada predefined language environment and standard libraries, corresponding to appendices A through H of the Ada RM.
SPARK 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 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 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 Strings, but their use is constrained by other language restrictions.
14.4.2. The Package Strings.Maps (A.4.2)
Preconditions and postconditions are added to subprograms. Preconditions prevent all exceptions specified in the corresponding part of the Ada RM to be raised.
14.4.3. Fixed-Length String Handling (A.4.3)
Preconditions and postconditions are added to subprograms. Preconditions on subprograms prevent all exceptions specified in the corresponding part of the Ada RM to be raised, except for procedures Move, Replace_Slice, Insert, Overwrite, Head, and Tail. These have incomplete contracts and may raise an exception if they are called with inconsistent actual parameters. Each call of these procedures should be preceded with a pragma Assert to check that the actual parameters are consistent. Postconditions on subprograms, when present, fully detail their effect.
14.4.4. Bounded-Length String Handling (A.4.4)
Global, preconditions and postconditions are added to subprograms. Preconditions prevent all exceptions specified in the corresponding part of the Ada RM to be raised.
14.4.5. Unbounded-Length String Handling (A.4.5)
The type String_Access and the procedure Free are not in SPARK as they require non-owning access types and cannot be denoted in SPARK program text.
Global, preconditions and postconditions are added to subprograms. Preconditions prevent all exceptions specified in the corresponding part of the Ada RM to be raised.
14.4.6. String-Handling Sets and Mappings (A.4.6)
No additions or restrictions.
14.4.7. Wide_String Handling (A.4.7)
The types Wide_String_Access and Wide_Character_Mapping_Function are not in SPARK nor are the subprograms which have formal parameters of these types and cannot be denoted in SPARK 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)
The types Wide_Wide_String_Access and Wide_Wide_Character_Mapping_Function are not in SPARK nor are the subprograms which have formal parameters of these types and cannot be denoted in SPARK 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 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)
All functions are annotated with preconditions that guard against exceptions being raised. The following functions may produce infinite results for some inputs which satisfy their preconditions (if any). For SPARK, this is just as bad as propagating an exception. Both are events that can invalidate SPARK proofs because proofs may rely on an assumption that these events do not occur. Thus, the onus is on the user to avoid such inputs:
function Exp returns +infinite on large values of argument X
function ** returns +infinite on large values of arguments Left and Right
functions Cot of one argument, as well as functions Tan and Cot with arguments X and Cycle, may return an infinite on values of X that are close to their singularity points
functions Sinh and Cosh return an infinite on larges values of argument X
function Coth returns an infinite on small values of argument X close to zero
functions Arctanh and Arccoth return an infinite on values of argument X close to one
Interestingly, function Tan of one argument never returns an infinite result for any input value, both in 32-bits and 64-bits floating-points. This is due to all floating-point approximations of its singularity points being too far from the singularity (all values that are a multiple of \(\pi\) away from \(\pi / 2\)).
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 but the functions have side effects and should not be called from SPARK 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 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 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 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 except for the type File_Access, a generalized access type, thus preventing Ada.Text_IO from being declared with SPARK_Mode On explicitly in the visible part. The following subprograms are explicitly marked as SPARK_Mode Off:
The functions Current_Input, Current_Output, Current_Error, Standard_Input, Standard_Output and Standard_Error because they create aliasing, by returning the corresponding file.
The procedures Set_Input, Set_Output and Set_Error because they also create aliasing, by assigning a File_Type variable to respectively Current_Input, Current_Output or Current_Error.
Functions Get_Line because they have a side effect of reading data from a file and updating its file pointers.
The abstract state File_System declared in Ada.Text_IO is used to model the memory on the system and the file handles (Line_Length, Col, etc.). This is made necessary by the fact that almost every procedure in Text_IO that actually modifies attributes of its File_Type parameter takes it as an in parameter.
All functions and procedures are annotated with Global, and Pre/Post when possible. The Global contracts are typically In_Out for File_System, even in Put or Get procedures that update the current column and/or line. Functions have an Input global contract. The only functions with Global => null are the functions Get and Put in the generic packages that have the same behavior as sprintf and sscanf.
Preconditions are not always complete, as not all conditions leading to run-time exceptions can be effectively modelled in SPARK:
Status_Error (due to a file already open/not open) is fully modelled
Mode_Error (due to a violation of the internal state machine) is fully modelled
Layout_Error is partially modelled
Use_Error is not modelled (it is related to the external environment)
Name_Error is not modelled (it would require checking availability on disk beforehand)
End_Error is not modelled (it is raised when a file terminator is read while running the procedure)
In the exceptional cases that are not fully modelled, it is possible that SPARK tools do not issue a possible precondition failure message on a call, yet an exception can be raised at run-time. See the spec files for the exact contracts.
14.10.2. Text File Management (A.10.2)
The possibility of errors related to the actual content or limitations of the file system are not modelled (e.g. when trying to create an already existing file, or open a file that does not exist).
Preconditions and postconditions are added to describe other constraints.
14.10.3. Default Input, Output and Error Files (A.10.3)
Apart from procedure Flush, all other subprograms are explicitly marked as SPARK_Mode Off, as described above, because they create aliasing.
14.10.4. Specification of Line and Page Lengths (A.10.4)
Global, preconditions and postconditions are added to subprograms.
14.10.5. Operations on Columns, Lines and Pages (A.10.5)
Global, preconditions and postconditions are added to subprograms.
14.10.6. Get and Put Procedures (A.10.6)
Global, preconditions and postconditions are added to subprograms.
14.10.7. Input-Output of Characters and Strings (A.10.7)
Functions Get_Line are explicitly marked as SPARK_Mode Off, as described above, because they have side effects.
Global, preconditions and postconditions are added to other subprograms.
14.10.8. Input-Output for Integer Types (A.10.8)
Global, preconditions and postconditions are added to subprograms.
14.10.9. Input-Output for Real Types (A.10.9)
Global, preconditions and postconditions are added to subprograms.
14.10.10. Input-Output for Enumeration Types (A.10.10)
Global, preconditions and postconditions are added to subprograms.
14.10.11. Input-Output for Bounded Strings (A.10.11)
An instantiation of Bounded_IO will ostensibly be in SPARK 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 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 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 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 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 but the exceptions cannot be handled in SPARK program text.
14.14. File Sharing (A.14)
File sharing is not permitted in SPARK, since it may introduce an alias.
14.15. The Package Command_Line (A.15)
The package Command_Line is in SPARK 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 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 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.
14.18. Containers (A.18)
The standard Ada container libraries are not supported in SPARK.
An implementation may choose to provide alternative container libraries whose specifications are in SPARK 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, covering facilities offered by Ada’s Annex B.
Package Interfaces can be used in SPARK, including its
intrinsic “Shift” and “Rotate” functions.
Other packages are not directly supported.
14.21. Systems Programming (Annex C)
This section describes features for systems programming in SPARK, covering facilities offered by Ada’s Annex C.
Almost all of the facilities offered by this Annex are out of scope for SPARK and so are not supported.
14.21.1. Pragma Discard_Names (C.5)
Pragma Discard_Names is not permitted in SPARK, since its use can lead to implementation defined behaviour at run time.
14.22. Real-Time Systems (Annex D)
SPARK supports the parts of the real-time systems annex that comply with the Ravenscar or Jorvik profiles (see Ada RM D.13). See section Tasks and Synchronization.
14.23. Distributed Systems (Annex E)
SPARK does not support the distributed systems annex.
14.24. Information Systems (Annex F)
The Machine_Radix aspect and attribute are permitted in SPARK.
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.
14.25. Numerics (Annex G)
This section describes features for numerical programming in SPARK, covering facilities offered by Ada’s Annex G.
Packages declared in this Annex are usable in SPARK, 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 fully supports the requirements of Ada’s Annex H.