SPARK

SPARK Library User Manual

 

 

 

 

 

 

 

 

 

 

 

SLUM

Issue: 3.21

Status: Definitive

28th September 2011

 

DOCTYPE:Praxis title:varchar=title reference:varchar=reference status:varchar=status issue:varchar=issue date:varchar=date projectname:varchar=DocumentSet

Issue 3.15, Definitive, 11th November 2010

000_000 SPARK Library User Manual

 

 

 

Originator

 

 

SPARK Team

 

 

 

Approver

 

 

SPARK Product Manager

 

 

 

 

 

 

 

 

 

 

 

 

 

 

 

 

 

 

 

 

 

 

 

 

 

 

 

 



Copyright

The contents of this manual are the subject of copyright and all rights in it are reserved.  The manual may not be copied, in whole or in part, without the written consent of Altran Praxis Limited.

 

Limited Warranty

Altran Praxis Limited save as required by law makes no warranty or representation, either express or implied, with respect to this software, its quality, performance, merchantability or fitness for a purpose.  As a result, the licence to use this software is sold ‘as is’ and you, the purchaser, are assuming the entire risk as to its quality and performance.

Altran Praxis Limited accepts no liability for direct, indirect, special or consequential damages nor any other legal liability whatsoever and howsoever arising resulting from any defect in the software or its documentation, even if advised of the possibility of such damages.  In particular Altran Praxis Limited accepts no liability for any programs or data stored or processed using Altran Praxis Limited products, including the costs of recovering such programs or data.

SPADE is a registered trademark of Altran Praxis Limited.

Note:  The SPARK programming language is not sponsored by or affiliated with SPARC International Inc. and is not based on SPARC™ architecture.

1          Introduction

2          The SPARK Library

2.1      Types of library package

2.2      Library Package Location and Use

2.3      Correspondence with Ada Library

2.4      The SPARK Library Header

2.5      Summary of Library Units

3          SPARK_IO

3.1      External Files and File Objects

3.2      Text Input-Output

3.3      Types and Constants

3.4      File Management

3.5      Default Input and Output Files

3.6      Specification of Line and Page Lengths

3.7      Operations on Columns, Lines and Pages

3.8      Get and Put Procedures

3.9      Input-Output of Characters and Strings

3.10    Input-Output for Integer Types

3.11    Input-Output for Real Types

3.12    Input-Output for Enumeration Types

3.13    Specification of the Package SPARK_IO

3.14    Exceptions in Input-Output

3.15    Example of Input-Output

Document Control and References

File under

Changes history

Changes forecast


 

Contents

 

 


1                       Introduction

The SPARK language has very few predefined library packages compared with Ada because Ada library packages lack the required SPARK annotations and many use features not permitted in SPARK.

To facilitate the use of the extensive functionality provided by the Ada library packages a SPARK Library has been provided. Several types of library package are supported, such as:

·         Packages predefined by the Ada LRM, including package Ada, its numerous public child packages such as Ada.Characters, Ada.Text_IO and package Interfaces and its children.

·         Packages that are not part of the Ada standard, but are implementation-defined by particular compilers. The most obvious examples in this class are the GNAT.* packages supplied with the GNAT Pro family of Ada compilers.

·         Entirely new packages. Such packages may be written entirely in SPARK and shipped with verification results.

The SPARK Toolset has always included a package called SPARK_IO which has provided some of the functionality of Ada.Text_IO via a SPARK compatible interface. Versions of SPARK_IO are supplied that are compatible with SPARK83 as well as the SPARK95 and SPARK2005 language profiles. This package has always shipped with all versions of the SPARK toolset (but is now superseded by SPARK.Ada.Text_IO). All other packages in the new library use Ada95’s child package mechanism, and so are not compatible with the SPARK83 language profile.

Section 2 of this document provides documentation for the SPARK Library packages in general (excluding SPARK_IO).

Section 3 is specific to SPARK_IO, which has always been supplied with the SPARK Toolset, and is used and documented differently to the rest of the SPARK Library packages.

2                       The SPARK Library

2.1               Types of library package

In SPARK, there are several techniques for making a non-SPARK library package available. This section introduces the terms used to describe each of these techniques:

 

Technique

Description

Example

Synthesized

The specification of these packages is internally synthesized by the Examiner at start-up. There is no “source file” for these packages.

Standard

Shadow

A “Shadow” specification is a SPARK-friendly version of a predefined package specification. An Ada implementation will have its own version of this specification (for compilation) while the shadow specification is submitted to the Examiner for analysis. We use the naming convention of “*.shs” for shadow package specifications.

Interfaces

Thick Binding

A thick binding is a SPARK package specification and an Ada body that “binds” to an underlying package.

SPARK_IO (a thick binding to Ada.Text_IO)

New

A completely new package, not part of the standard Ada library at all. The specification will be SPARK. The body could be SPARK or Ada. If the body is SPARK, then verification evidence might be supplied for such units.

SPARK.Unsigned

2.2               Library Package Location and Use

The SPARK Library packages are provided in source form in /lib/spark/current under the toolset installation directory. With the exception of SPARK_IO they are made visible to the Examiner by using the switch -sparklib so there is no need to list them in index files. The effect of the –sparklib switch depends on whether the user has also specified a user-defined index file.

If no user-defined index file has been specified, then –sparklib has the effect of setting the user-defined index file to /lib/spark/current/sparklib.idx under the toolset installation directory.

If a user-defined index file has been specified, then –sparklib adds the following entries:

       Ada        auxindex is in ada.idx
       Interfaces auxindex is in interfaces.idx
       SPARK      auxindex is in spark.idx

where the index files are to be found in /lib/spark/current/ under the toolset installation directory.

2.3               Correspondence with Ada Library

A SPARK Library binding to an Ada Library package Ada.P will be named SPARK.Ada.P. The SPARK Library binding may consist of several packages, typically:

·         SPARK.Ada.P - the primary package providing the SPARK interface to Ada.P;

·         SPARK.Ada.P.Not_SPARK - a non-SPARK public child providing those aspects of the interface to Ada.P which are not compatible with SPARK.

For a primary SPARK Library package which is a binding to an Ada Library package, the differences will generally be in:

·          The naming, because:

¾       some identifiers are reserved FDL keywords (such as Length and Element);

¾       overloading of identifiers is not supported in SPARK, so for instance, the Ada functions

  function F (X : T1, Y : T2) return T1;
  function F (X : T1; Y : T3) return T1;

would be named

  function F_T2 (X : T1; Y : T2) return T1;
  function F_T3 (X : T1; Y : T3) return T1;

·          The SPARK binding contains global annotations, derives annotations required for flow analysis, and pre, post and return annotations required for proof (as a minimum for proof of absence of RTE in the calling environment).

Each primary library package specification is intended to be self-documenting (in conjunction with the Ada LRM for a binding to an Ada Library package) and provides the following information:

·          A header defining its fundamental characteristics.

·          If it is a binding for an Ada library unit, for each subprogram which is differently named a comment is given showing the equivalent Ada subprogram specification.

·          If there are differences in behaviour between the Ada library unit and the SPARK binding then this is documented via a comment.

·          If the SPARK Library package is a thick binding or is not related to an Ada Library package, sufficient documentation to use the package is included in its comments.

Where present, the Not_SPARK child package specifications do not have headers or comments because they are copied directly from the Ada LRM and are detailed in that document.

2.4               The SPARK Library Header

The SPARK Library header has the following general form, using SPARK.Ada.Strings.Unbounded as an example:

--------------------------------------------------------------------------------

--                                                                            --

-- SPARK.Ada.Strings.Unbounded                                                --

--                                                                            --

-- Description                                                                --

--   This is a binding to package Ada.Strings.Unbounded                       --

--                                                                            --

-- Language                                                                   --

--   Specification : SPARK                                                    --

--   Private Part  : Ada                                                      --

--   Body          : Ada                                                      --

--                                                                            --

-- Runtime Requirements and Dependencies                                      --

--   Full Ada Runtime                                                         --

--                                                                            --

-- Verification                                                               --

--   N/A                                                                      --

--                                                                            --

-- Exceptions                                                                 --

--   Ada.Strings.Index_Error (Guarded)                                        --

--   Ada.Strings.Pattern_Error (Guarded)                                      --

--                                                                            --

--------------------------------------------------------------------------------

Where:

·          Description: defines whether the package is a binding, a thick binding or unrelated to an Ada library package.  In the above example it is a binding to Ada.Strings.Unbounded.

·          Language: specifies the language of the specification (almost certainly SPARK), the private part and the body of the package. Note that even though the visible part of the specification is in SPARK the private part may be in Ada.

·          Runtime Requirements and Dependencies: documents any runtime dependencies of the package and can take the following values:

¾       Full Ada Runtime

¾       Restricted (possibly giving details of what is required)

¾       ZFP  (the AdaCore GNAT Pro Zero Footprint library)

¾       No Ada Runtime[1]

·          Verification: states the level of formal proof performed. Proofs can only be performed on packages which are entirely (or at least parts of the body) written in SPARK.  The level of proof varies from N/A, for non-SPARK packages, to none, through proof of absence of run-time exceptions to proof of specified properties.

·          Exceptions: This lists the exceptions declared within the underlying Ada library package and adorns each with the level of guarantee that they will not be raised.  The level of guarantee may be

¾       No guarantee: the exception name is unadorned and may be raised by the package.

¾       Guarded: provided the pre-conditions specified for each subprogram in the interface are satisfied when they are called (the SPARK proof system can be used to demonstrate this), then the exception adorned with Guarded should not be raised.  The pre-conditions are determined from the Ada LRM and so, provided the underlying Ada Library component is properly implemented, the corresponding exception should not occur.  However, the underlying Ada Library component is unlikely to be written in SPARK so its implementation cannot be proven not to raise the exception or any other run-time exception.

If the underlying Ada Library package does not declare any exceptions or it is a Library package written in SPARK the list of exceptions will be empty.

Note that any library unit which allocates memory may raise the exception Storage_Error and this cannot be guarded against, nor can it be deduced using the proof system.

2.5               Summary of Library Units

The following table shows each unit supported by the SPARK Library, its technique class, its source file (if there is one), and any other comment regarding its use:

 


Unit

Class

Source file

Comment

Standard

Synthesized

N/A

As per SPARK LRM. Implementation-defined values can be inserted via the configuration file.

System

Synthesized

N/A

As per SPARK LRM. Implementation-defined values can be inserted via the configuration file.

Interfaces

Shadow

interfaces.shs

SPARK-compatible types only. See SPARK.Unsigned for shift and rotate functions.

Interfaces.C

Shadow

interfaces-c.shs

SPARK-compatible types and constants only.

Ada

Synthesized

N/A

As per Ada LRM A.2.

Ada.Characters

Synthesized

N/A

As per Ada LRM A.3.1.

Ada.Characters.Latin_1

Synthesized

N/A

As per Ada LRM A.3.3.

Ada.Characters.Handling

Shadow

ada-characters-handling.shs

SPARK-compatible functions only.

Ada.Interrupts

Synthesized

N/A

Only available when –profile=ravenscar is selected. Implementation-defined values can be inserted via the configuration file.

Ada.Real_Time

Synthesized

N/A

Only available when –profile=ravenscar is selected. Implementation-defined values can be inserted via the configuration file.

Ada.Synchronous_Task_Control

Synthesized

N/A

Only available when –profile=ravenscar is selected. Implementation-defined values can be inserted via the configuration file.

SPARK

New

spark.ads

Empty root package

SPARK.Ada

New

spark-ada.ads

Empty root package

SPARK.Ada.Command_Line

New, thick binding

spark-ada-command_line.ads

Thick binding to Ada.Command_Line

SPARK.Ada.Command_Line.Unbounded_String

New, thick binding

spark-ada-command_line-unbounded_string.ads

Thick binding to Ada.Command_Line using unbounded strings

SPARK.Ada.Containers

New

spark-ada-containers.ads

Types and constants only. Mimics those in Ada.Containers.

SPARK.Ada.Strings

New

spark-ada-strings.ads

Types and constants only. Mimics those in Ada.Strings.

SPARK.Ada.Strings.Not_SPARK

New

spark-ada-strings-not_spark.ads

Non-SPARK elements from Ada.Strings.

SPARK.Ada.Strings.Maps

New, thick binding

spark-ada-strings-maps.ads

Thick binding to Ada.Strings.Maps

SPARK.Ada.Strings.Maps.Not_SPARK

New

spark-ada-strings-maps-not_spark.ads

Non-SPARK elements from Ada.Strings.Maps

SPARK.Ada.Strings.Unbounded

New, thick binding

spark-ada-strings-unbounded.ads

Thick binding to Ada.Strings.Unbounded

SPARK.Ada.Strings.Unbounded.Not_SPARK

New

spark-ada-strings-unbounded-not_spark.ads

Non-SPARK elements from Ada.Strings.Unbounded

SPARK.Ada.Text_IO

New, thick binding

spark-ada-text_io.ads

Thick binding to Ada.Text_IO using type String

SPARK.Ada.Text_IO.Not_SPARK

New

spark-ada-text_io.ads

Non-SPARK elements from Ada.Text_IO

SPARK.Ada.Text_IO.Unbounded_String

New, thick binding

spark-ada-text_io.ads

Thick binding to Ada.Text_IO using unbounded strings

SPARK.Unsigned

New, shadow

spark-unsigned.shs (SPARK shadow)
spark-unsigned.ads (for compiler)

Provides a SPARK-compatible, efficient binding to the Shift and Rotate functions provided by Ada’s Interfaces package.

SPARK_IO

Thick binding

spark_io.ads

Thick binding to Ada.Text_IO. See section 3.

 


3                       SPARK_IO

Note that SPARK_IO is provided for backward compatibility but it is now superseded by the SPARK.Ada.Text_IO packages.

SPARK_IO is a package which defines operations for file manipulation and input-output of the predefined types Character, String, Integer and Float. There are two versions of this package, one for SPARK 95 and one for SPARK 2005. If required, facilities for input-output of new integer and floating point types, fixed point types and enumeration types may be provided by the user, based on procedures in SPARK_IO, whose specification and body are supplied in machine-readable form with the SPARK Toolset.

The specification of the package SPARK_IO obeys the rules of SPARK and can be used with other packages written in SPARK.  Its subprograms, implemented as in the supplied version of the package body, will not raise unhandled exceptions.

SPARK_IO is made available for use by the Examiner by listing the path names of SPARK_IO package specification and body in the Examiner index file; see the Index File section in the Examiner User Manual.  The location of the SPARK_IO library files is dependent on your installation but will be under the subdirectory lib/spark.

As well as providing input-output facilities, SPARK_IO also serves as a practical example of how to construct a SPARK interface to non-SPARK software, including use of the SPARK hide directive.

3.1               External Files and File Objects

Values input from the external environment of the program, or output to the environment, are considered to occupy external files.  An external file can be anything external to the program that can produce a value or receive a value to be written.  An external file is identified by a string - the name.  A second string — the form  — gives further system-dependent characteristics that may be associated with the file.

Input and output operations are expressed as operations on objects of some file type, rather than directly in terms of the external files.  In the remainder of this chapter, the term file is always used to refer to a file object; the term external file is used otherwise.  The values transferred for a given file must all be of one type.

The SPARK_IO package declares three own variables Inputs, Outputs and State. Inputs represents the set of external input files used by a program and Outputs represents the set of external output files.  State represents the internal essential state of the SPARK_IO package.  The file SPARK_IO.Standard_Input is considered to be a member of Inputs, while SPARK_IO.Standard_Output is considered to be a member of Outputs.  A variable of type SPARK_IO.File_Type is used to identify a particular file within the set of input or output files (just as an index is used to identify a particular element in an array); this variable does not represent the file itself.

The use of three own variables prevents unwanted coupling of outputs with inputs and complies with the guidelines in the INFORMED method for SPARK design.

Before performing any operation on an external file the file must have been opened (by one of the Open procedures if the file already exists or by one of the Create procedures if not). An open file has a current mode which is a value of the enumeration type

type File_Mode is (In_File, Out_File, Append_File);

Before reading from a file (with one of the Get operations), the file must have been opened for input (mode In_File).  Before writing to a file (with one of the Put operations), the file must have been opened for output (mode Out_File or Append_File).

The standard Ada input-output routines generate exceptions if error conditions are encountered, but exceptions are not allowed in SPARK.  Instead, where appropriate a routine has a status parameter, whose returned value indicates whether an error condition has arisen.  (If this status is not checked by a program, after every call of the routine, the Examiner will report the existence of data-flow anomalies - specifically the updating without subsequent reading of the status variable).

If a status variable indicates that an error has occurred, any other returned values are undefined, and the onus is on the programmer to organise appropriate recovery actions.  For routines which do not return status information, the programmer should establish that their pre-conditions are always satisfied.

3.2               Text Input-Output

This section describes the facilities provided by the package SPARK_IO for input and output in human-readable form.  The package SPARK_IO replaces the predefined Ada package Ada.Text_IO.

3.3               Types and Constants

SPARK_IO declares a number of types, constants and functions used throughout the package.  These are as follows:

type File_Type is private;

type File_Mode is (In_File, Out_File, Append_File);

type File_status is (Ok, Status_Error, Mode_Error, Name_Error,

                     Use_Error, Device_Error, End_Error, Data_Error,

                     Layout_Error, Storage_Error, Program_Error);

 

subtype Number_Base is Integer range 2 .. 16;

 

function Standard_Input return File_Type;

--# global in Inputs;

function Standard_Output return File_Type;

--# global in Outputs;

Null_File : constant File_Type;

3.4               File Management 

The procedures and functions described in this section provide for the control of external files.

procedure Create(File          :    out File_Type;

                 Name_Of_File  : in     String;

                 Form_Of_File  : in     String;

                 Status        :    out File_Status)

--# global in out State;

--# derives File,

--#         State,

--#         Status from Form_Of_File,

--#                     Name_Of_File,

--#                     State;

--# declare delay;

 

procedure Create_Flex(File          :    out File_Type;

                      Name_Length   : in     Natural;

                      Name_Of_File  : in     String;

                      Form_Of_File  : in     String;

                      Status        :    out File_Status)

--# global in out State;

--# derives File,

--#         State,

--#         Status from Form_Of_File,

--#                     Name_Length,

--#                     Name_Of_File,

--#                     State;

--# declare delay;

If File does not identify a file within Outputs a new file is added to Outputs and File will be set to identify it.  A new external file is created, with the given name and form.  This external file is then associated with the file within Outputs identified by File.  The external file is opened.

The current mode of the specified file is set to Out_File and the page length and line length are unbounded.  The current column, the current line and the current page numbers are set to one.

A null string for Name_Of_File  specifies an external file that is not accessible after the completion of the main program (a temporary file). A null string for Form_Of_File  specifies the use of the default options of the implementation for the external file.

In Create_Flex the length of the actual file name is flexible and does not necessarily occupy the entire Name_Of_File string (although it must start at position 1). The actual length is given by the parameter Name_Length.

The Status parameter is set to Ok if no error condition is encountered. It is set to Status_Error if the specified file is already open, to Name_Error if the string given as Name does not allow the identification of an external file, or to Use_Error if, for the specified mode, the environment does not support creation of an external file with the given name (in the absence of Name_Error) and form.

Note that trying to use either Standard_Input or Standard_Output as the File parameter is not allowed.  By the rules of Ada, a function cannot be used as an “out” parameter.

procedure Open(File          :    out File_Type;

               Mode_Of_File  : in     File_Mode;

               Name_Of_File  : in     String;

               Form_Of_File  : in     String;

               Status        :    out File_Status)

--# global in out State;

--# derives File,

--#         State,

--#         Status from Form_Of_File,

--#                     Mode_Of_File,

--#                     Name_Of_File,

--#                     State;

--# declare delay;

 

procedure Open_Flex(File          :    out File_Type;

                    Mode_Of_File  : in     File_Mode;

                    Name_Length   : in     Natural;

                    Name_Of_File  : in     String;

                    Form_Of_File  : in     String;

                    Status        :    out File_Status)

--# global in out State;

--# derives File,

--#         State,

--#         Status from Form_Of_File,

--#                     Mode_Of_File,

--#                     Name_Length,

--#                     Name_Of_File,

--#                     State;

--# declare delay;

 

If File does not identify a file within Inputs or Outputs a new file is added to the appropriate set and File will be set to identify it.   The external file, of the given name, is then associated with the file within Inputs or Outputs identified by File.  The external file is opened.

In Open_Flex the length of the actual file name is flexible and does not necessarily occupy the entire Name_Of_File string (although it must start at position 1). The actual length is given by the parameter Name_Length.

The current mode of the specified file is set to the given access mode.  If the current mode of the specified file is Out_File the page length and line length are unbounded.  The current column, the current line and the current page numbers are set to one.

The Status parameter is set to Ok if no error condition is encountered. It is set to Status_Error if the specified file is already open, to Name_Error if the string given as Name does not allow the identification of an external file (in particular if no external file with the given name exists), or to Use_Error if, for the specified mode, the environment does not support opening of an external file with the given name (in the absence of Name_Error) and form.

Note that trying to use either Standard_Input or Standard_Output as the File parameter is not allowed.  By the rules of Ada a function cannot be used as an “out” parameter.

procedure Close(File   : in out File_Type;

                Status :    out File_Status)

--# global  in out State;

--# derives State,

--#         Status from File,

--#                     State &

--#         File  from ;

--# declare delay;

The association between the file in Inputs or Outputs identified by File and its associated external file is severed. The specified file is closed.

If the file has current mode Out_File or Append_File, has the effect of calling New_Page, unless the current page is already terminated; then outputs a file terminator.

The Status parameter is set to Ok if no error condition is encountered. It is set to Status_Error if the specified file is not open.  It is set to Use_Error if File is Standard_Input or Standard_Output.

procedure Delete(File   : in out File_Type;

                 Status :    out File_Status)

--# global  in out State;

--# derives State,

--#         Status from File,

--#                     State &

--#         File   from ;

--# declare delay;

The external file associated with the file in Inputs or Outputs identified by File is deleted. The specified file is closed and the external file ceases to exist.

The Status parameter is set to Ok if no error condition is encountered. It is set to Status_Error if the given file is not open or to Use_Error if deletion of the external file is not supported by the environment or if File is Standard_Input or Standard_Output.

procedure Reset(File         : in out File_Type;

                Mode_Of_File : in     File_Mode;

                Status       :    out File_Status);

--# derives File,

--#         Status from File,

--#                     Mode_Of_File;

--# declare delay;

The file identified by File is reset so that reading from or writing to its elements can be restarted from the beginning of the file. 

If the file has the current mode Out_File or Append_File, has the effect of calling New_Page, unless the current page is already terminated; then outputs a file terminator. If the new file mode is Out_File or Append_File, the page and line lengths are unbounded. The current column, line and page numbers are set to one.

The Status parameter is set to Ok if no error condition is encountered. It is set to Status_Error if the specified file is not open and to Use_Error if the environment does not support resetting for the external file or if the environment does not support resetting to the specified mode for the external file.

Note that trying to use either Standard_Input or Standard_Output as the File parameter is not allowed.  By the rules of Ada a constant cannot be used as an “in out” parameter.

function Valid_File(File : File_Type) return Boolean;

-- This is a potentially blocking function.

-- DO NOT CALL THIS FUNCTION FROM A PROTECTED OPERATION.

This function checks that File is a valid identification for a file and returns the result of the check.  It is a potentially blocking function call and should not be called from within a protected object in RavenSPARK.

function Mode(File : File_Type) return File_Mode;

-- This is a potentially blocking function.

-- DO NOT CALL THIS FUNCTION FROM A PROTECTED OPERATION.

Returns the current mode of the file identified by File. If the specified file is not open the result is undefined.  It is a potentially blocking function call and should not be called from within a protected object in RavenSPARK.

procedure Name(File         : in     File_Type;

               Name_Of_File :    out String;

               Stop         :    out Natural);

--# derives Name_Of_File,

--#         Stop         from File;

--# declare delay;

If File is currently valid and open, copies into Name_Of_File  a string which uniquely identifies the external file currently associated with the file identified by File (and may thus be used in an Open operation). If an environment allows alternative specifications of the name (for example, abbreviations), the string copied should correspond to a full specification of the name.  If Name_Of_File  is not big enough to hold the string, the string is truncated and Stop is set to Name_Of_File 'LENGTH + 1. Otherwise Stop is set to the length of the string copied into Name_Of_File .

If the specified file is not open or is invalid then the result is undefined.

procedure Form (File         : in     File_Type;

                Form_Of_File :    out String;

                Stop         :    out Natural);

--# derives Form_Of_File,

--#         Stop         from File;

--# declare delay;

If File is valid and open, copies into Form_Of_File  the form string for the external file currently associated with the file in Inputs or Outputs identified by File.  If an environment allows alternative specifications of the form (for example, abbreviations using default options), the string copied should correspond to a full specification (that is, it should indicate explicitly all options selected, including default options). If Form_Of_File  is not big enough to hold the string, the string is truncated and Stop is set to Form_Of_File'Length + 1. Otherwise Stop is set to the length of the string copied into Form_Of_File .

If the specified file is invalid or not open then the result is undefined.

function Is_Open(File : File_Type) return Boolean;

--# global State;

-- This is a potentially blocking function.

-- DO NOT CALL THIS FUNCTION FROM A PROTECTED OPERATION.

Returns True if the file identified by File is open (that is, if it is associated with an external file), otherwise returns False.  The function is potentially blocking and it should not be called from within a protected object in RavenSPARK.

3.5               Default Input and Output Files

Since SPARK does not allow overloading or default parameters, file parameters cannot be omitted from input-output operations which require them.  Hence, SPARK_IO does not support the concept of default input and output files and no routines are provided for their manipulation.

3.6               Specification of Line and Page Lengths

SPARK_IO does not currently support the setting of line and page lengths. Therefore, files of mode Out_File or Append_File always have unbounded line and page lengths (that is, they have the conventional value zero).  New lines and new pages are only started when explicitly called for.

3.7               Operations on Columns, Lines and Pages

The subprograms described in this section provide for explicit control of line and page structure.  Currently SPARK_IO does not support page operations on files of mode In_File.

procedure New_Line(File      : in   File_Type;

                   Spacing   : in   Positive);

--# global in out Outputs;

--# derives Outputs from File,

--#                      Outputs,

--#                      Spacing;

--# declare delay;

Operates on a file of mode Out_File.

For a Spacing of one: Outputs a line terminator and sets the current column number to one. Then increments the current line number by one, except in the case that the current line number is already greater than or equal to the maximum page length, for a bounded page length; in that case a page terminator is output, the current page number is incremented by one, and the current line number is set to one.

For a Spacing greater than one, the above actions are performed Spacing times.

No action is performed if the mode of the file identified by File is not Out_File or File is not a valid file identifier.

procedure Skip_Line(File      : in   File_Type;

                    Spacing   : in   Positive);

--# global in out Inputs;

--# derives Inputs from File,

--#                     Inputs,

--#                     Spacing;

--# declare delay;

Operates on a file of mode In_File.

For a Spacing of one: Reads and discards all characters until a line terminator has been read, and then sets the current column number to one.  If the line terminator is not immediately followed by a page terminator, the current line number is incremented by one. Otherwise, if the line terminator is immediately followed by a page terminator, then the page terminator is skipped, the current page number is incremented by one, and the current line number is set to one.

For a Spacing greater than one, the above actions are performed Spacing times, or until a file terminator is reached.

No action is performed if the mode of the file identified by File is not In_File, an attempt is made to read a file terminator or File is not a valid file identifier.

procedure New_Page (File : in   File_Type);

--# global in out Outputs;

--# derives Outputs from File,

--#                      Outputs;

--# declare delay;

Operates on a file of mode Out_File.

Outputs a line terminator if the current line is not terminated, or if the current page is empty (that is, the current column and line numbers are both equal to one). Then outputs a page terminator, which terminates the current page. Adds one to the current page number and sets the current column and line numbers to one.

No action is performed if the mode of the file identified by File is not Out_File or File is not a valid file identifier.

function End_Of_Line(File : File_Type) return Boolean;

--# global  Inputs;

-- This is a potentially blocking function.

-- DO NOT CALL THIS FUNCTION FROM A PROTECTED OPERATION.

Operates on a file of mode In_File.

Returns True if File is a valid identifier of an open file of mode In_File and a line terminator or a file terminator is next; Returns False if File is a valid identifier of an open file of mode In_File and a line terminator or a file terminator is not next; otherwise the result is undefined.  The function is potentially blocking and it should not be called from within a protected object in RavenSPARK.

function End_Of_File(File : File_Type) return Boolean;

--# global Inputs;

-- This is a potentially blocking function.

-- DO NOT CALL THIS FUNCTION FROM A PROTECTED OPERATION.

Operates on a file of mode In_File.

Returns True if File is a valid identifier of an open file of mode In_File and a file terminator is next, or if the combination of a line and/or a page terminator followed by a file terminator is next; Returns False if File is a valid identifier of an open file of mode In_File and a line terminator is not next, or if the combination of a line and/or a page terminator followed by a file terminator is not next; otherwise the result is undefined.  The function is potentially blocking and it should not be called from within a protected object in RavenSPARK.

procedure Set_In_File_Col(File   : in   File_Type;

                          Posn   : in   Positive);

--# global in out Inputs;

--# derives Inputs from File,

--#                     Inputs,

--#                     Posn;

--# declare delay;

--# pre Mode (File) = In_File;

Reads (and discards) individual characters, line terminator, and page terminators, until the next character to be read has a column number that equals the value specified by Posn; there is no effect if the current column number already equals this value. Each transfer of a character or terminator maintains the current column, line and page numbers in the same way as a Get procedure. (Short lines will be skipped until a line is reached that has a character at the specified column position.)   No action is performed if an attempt is made to read a file terminator.

procedure Set_Out_File_Col(File : in File_Type;

                           Posn : in Positive);

--# global in out Outputs;

--# derives Outputs from File,

--#                      Outputs,

--#                      Posn;

--# declare delay;

--# pre Mode (File) = Out_File or

--#     Mode (File) = Append_File;

If the value specified by Posn is greater than the current column number, outputs spaces, adding one to the current column number after each space, until the current column number equals the specified value. If the value specified by Posn is less than the current column number, has the effect of calling New_Line (with a spacing of one), then outputs (Posn - 1) spaces, and sets the current column number to the specified value.

No action is performed if the value specified by Posn exceeds the line length when the line length is bounded (that is, when it does not have the conventional value zero).

function In_File_Col(File : File_Type) return Positive;

--# global Inputs;

--# pre Mode (File) = In_File;

-- This is a potentially blocking function.

-- DO NOT CALL THIS FUNCTION FROM A PROTECTED OPERATION.

If File is a valid identifier of an open file then returns the current column number; otherwise the result is undefined.  The function is potentially blocking and it should not be called from within a protected object in RavenSPARK.

function Out_File_Col(File : File_Type) return Positive;

--# global Outputs;

--# pre Mode (File) = Out_File or

--#     Mode (File) = Append_File;

-- This is a potentially blocking function.

-- DO NOT CALL THIS FUNCTION FROM A PROTECTED OPERATION.

If File is a valid identifier of an open file then returns the current column number; otherwise the result is undefined.  The function is potentially blocking and it should not be called from within a protected object in RavenSPARK.

function In_File_Line(File : File_Type) return Positive;

--# global Inputs;

--# pre Mode (File) = In_File;

-- This is a potentially blocking function.

-- DO NOT CALL THIS FUNCTION FROM A PROTECTED OPERATION.

If File is a valid identifier of an open file then returns the current line number; otherwise the result is undefined.  The function is potentially blocking and it should not be called from within a protected object in RavenSPARK.

function Out_File_Line(File : File_Type) return Positive;

--# global Outputs;

--# pre Mode (File) = Out_File or

--#     Mode (File) = Append_File;

-- This is a potentially blocking function.

-- DO NOT CALL THIS FUNCTION FROM A PROTECTED OPERATION.

If File is a valid identifier of an open file then returns the current line number; otherwise the result is undefined.  The function is potentially blocking and it should not be called from within a protected object in RavenSPARK.

3.8               Get and Put Procedures

To avoid overloading, a set of get and put procedures is provided (for example Get_Char, Put_Char, Get_String, Put_String).  Features that are common to these procedures are described in this section.

Most of the Get and Put procedures operate on files and so they have a file parameter, written first. (The exceptions are the “get from string” and “put to string” procedures).  Unlike Ada.Text_IO, in SPARK_IO this file parameter cannot be omitted.  The Get procedures operate on a file of mode In_File and the Put procedures operate on a file of mode Out_File or Append_File.

The Get and Put procedures maintain the current column, line and page numbers of the specified file, in the same way as Ada.Text_IO.

3.9               Input-Output of Characters and Strings

For an item of type Character or String the following procedures are provided.

procedure Get_Char(File : in     File_Type;

                   Item :    out Character);

--# global in out Inputs;

--# derives Inputs,

--#         Item    from File,

--#                      Inputs;

--# declare delay;

Operates on a file of mode In_File.

After skipping any line terminators and any page terminators, reads the next character from the specified input file and returns the value of this character in the out parameter Item.

If an attempt is made to skip a file terminator, no action is performed and the value of Item is undefined.

procedure Get_Char_Immediate (File   : in     File_Type;

                              Item   :    out Character;

                              Status :    out File_Status);

--# global in out Inputs;

--# derives Inputs,

--#         Item,

--#         Status from File,

--#                     Inputs;

--# declare delay;

Operates on a file of mode In_File.  Only the variant of Get_Immediate that waits for a character to become available is supported.

On return Status is one of Ok, Mode_Error or End_Error. See ALRM A.10.7

Item is set to Character'First if Status /= Ok

 

procedure Put_Char(File   : in   File_Type;

                   Item   : in   Character);

--# global in out Outputs;

--# derives Outputs from File,

--#                      Item,

--#                      Outputs;

--# declare delay;

Operates on a file of mode Out_File or Append_File.

If the line length of the specified output file is bounded (that is, does not have the conventional value zero), and the current column number exceeds it, has the effect of calling New_Line with a spacing of one. Then, or otherwise, outputs the given character to the file.

procedure Get_String(File : in     File_Type;

                     Item :    out String;

                     Stop :    out Natural);

--# global in out Inputs;

--# derives Inputs,

--#         Item,

--#         Stop     from File,

--#                       Inputs;

--# declare delay;

Operates on a file of mode In_File.

Determines the length of the given string and attempts that number of Get_Char operations for successive characters of the string. If characters are read, returns in Stop the index value such that Item(Stop) is the last character replaced (the index of the first character replaced is Item'FIRST).  If no characters are read returns in Stop an index value which is one less than Item'FIRST.

 

procedure Put_String(File : in   File_Type;

                     Item : in   String;

                     Stop : in   Natural);

--# global in out Outputs;

--# derives Outputs from File,

--#                      Item,

--#                      Outputs,

--#                      Stop;

--# declare delay;

Operates on a file of mode Out_File or Append_File.

If Stop is zero determines the length of the given string and attempts that number of Put_Char operations for successive characters of the string. If Stop is less than or equal to Item'Last then characters from Item'First up to and including Stop are output.  If Stop is larger than Item'Last then all characters in Item are output, followed by spaces up to and including the width specified by Stop.

procedure Get_Line(File : in     File_Type;

                   Item :    out String;

                   Stop :    out Natural)

--# global in out Inputs;

--# derives Inputs,

--#         Item,

--#         Stop    from File,

--#                      Inputs;

--# declare delay;

Operates on a file of mode In_File.

Replaces successive characters of the specified string by successive characters read from the specified input file. Reading stops if the end of the line is met, in which case the procedure Skip_Line is then called (in effect) with a spacing of one; reading also stops if the end of the string is met. Characters not replaced are left undefined.

If characters are read, returns in Last the index value such that Item(Last) is the last character replaced (the index of the first character replaced is Item'FIRST). If no characters are read, returns in Last an index value that is one less than Item'FIRST. This value is also returned if an attempt is made to skip a file terminator.

procedure Put_Line(File : in    File_Type;

                   Item : in    String

                   Stop : in    Natural);

--# global in out Outputs;

--# derives Outputs from File,

--#                      Item,

--#                      Outputs,

--#                      Stop;

--# declare delay;

Operates on a file of mode Out_File or Append_File.

Calls the procedure Put_String for the given string, and then the procedure New_Line with a spacing of one.

3.10          Input-Output for Integer Types

Since SPARK does not support generic packages, input-output routines are only provided for the predefined integer type Integer.

Values are output as decimal or based literals, without underline characters or exponent and preceded by a minus sign if negative.  The format is specified by a non-negative field width parameter.  Values of bases are of the Integer subtype Number_base,

subtype Number_base is Integer range 2 .. 16;

 

Since SPARK does not allow the specification of default parameters there is no default field width or base.

procedure Get_Integer(File  : in     File_Type;

                      Item  :    out Integer;

                      Width : in     Natural;

                      Read  :    out Boolean);

--# global in out Inputs;

--# derives Inputs,

--#         Item,

--#         Read    from File,

--#                      Inputs,

--#                      Width;

--# declare delay;

Operates on a file of mode In_File.

If the value of the parameter Width is zero, skips any leading blanks, line terminators, or page terminators, then reads a plus or a minus sign if present, then reads according to the syntax of an integer literal (which may be a based literal). If a non-zero value of Width is supplied, then exactly Width characters are input, or the characters (possibly none) up to a line terminator, whichever comes first; any skipped leading blanks are included in the count.

If successful sets Read to True and returns, in the parameter Item, the Integer that corresponds to the sequence input.  Otherwise sets Read to False and the value of Item is undefined.

procedure Put_Integer(File  : in    File_Type;

                      Item  : in    Integer;

                      Width : in    Natural;

                      Base  : in    Number_base);

--# global in out Outputs;

--# derives Outputs from Base,

--#                      File,

--#                      Item,

--#                        Outputs,

--#                        Width;

--# declare delay;

Operates on a file of mode Out_File or Append_File.

Outputs the value of the parameter Item as an integer literal, with no underlines, no exponent, and no leading zeros (but a single zero for the value zero), and a preceding minus sign for a negative value.

If the resulting sequence of characters to be output has fewer than Width characters, then leading spaces are first output to make up the difference.

Uses the syntax for decimal literal if the parameter Base has the value ten; otherwise, uses the syntax for based literal, with any letters in upper case.

procedure Get_Int_From_String(Source  : in     String;

                              Item    :    out Integer;

                              Start_Pos: in    Positive;

                              Stop    :    out Natural);

--# derives Item,

--#         Stop from Source,

--#                   Start_Pos;

--# declare delay;

Reads an integer value from the beginning at Source(Start_Pos) from the given string, following the same rules as the Get_Integer procedure, but treating the end of the string as a file terminator. Returns, in the parameter Item, the Integer that corresponds to the sequence input. Returns in Stop the index value such that Source(Stop) is the last character read.

If the sequence input does not have the required syntax then Stop is one less than Start_Pos and the value of Item is undefined.

procedure Put_Int_To_String(Dest      : in out String;

                            Item      : in     Integer;

                            Start_Pos : in     Positive;

                            Base      : in     Number_Base);

--# derives Dest from Base,

--#                   Dest,

--#                   Item,

--#                   Start_Pos;

--# declare delay;

Outputs the value of the parameter Item to the given string such that the first digit (or sign) is at Dest(Start_Pos), following the same rule as for output to a file, using Dest'Last - Start_Pos + 1 as the value for Width.

3.11          Input-Output for Real Types

Since SPARK does not support generic packages, input-output routines are only provided for the predefined real type Float.

Values are output as decimal literals without underline characters.  The format of each value consists of a Fore field, a decimal point, an Aft field, and (if a nonzero Exp parameter is supplied) the letter E and an Exp field.

Since SPARK does not allow the specification of default parameters there is no default Fore, Aft or Exp.

procedure Get_Float(File  : in     File_Type;

                    Item  :    out Float;

                    Width : in     Natural;

                    Read  :    out Boolean);

--# global in out Inputs;

--# derives Inputs,

--#         Item,

--#         Read   from File,

--#                     Inputs,

--#                     Width;

--# declare delay;

Operates on a file of mode In_File.

If the value of the parameter Width is zero, skips any leading blanks, line terminators, or page terminators, then reads a plus or a minus sign if present, then reads according to the syntax of a float literal (which may be a based literal). If a non-zero value of Width is supplied, then exactly Width characters are input, or the characters (possibly none) up to a line terminator, whichever comes first; any skipped leading blanks are included in the count.

If successful sets Read to True and returns, in the parameter Item, the Float that corresponds to the sequence input.  Otherwise sets Read to False and the value of Item is undefined.

procedure Put_Float(File  : in    File_Type;

                    Item  : in    Float;

                    Fore  : in    Natural;

                    Aft   : in    Natural;

                    Exp   : in    Natural);

--# global in out Outputs;

--# derives Outputs from Aft,

--#                      Exp,

--#                      File,

--#                      Fore,

--#                      Item,

--#                      Outputs;

--# declare delay;

Operates on a file of mode Out_File or Append_File.

Outputs the value of the parameter Item as a Float literal, with the format defined by Fore, Aft and Exp.  If the value is negative, a minus sign is included in the integer part.  If Exp has the value zero, then the integer part to be output has as many digits as are needed to represent the integer part of the value of Item, overriding Fore if necessary, or consists of the digit zero if the value of Item has no integer part.

procedure Get_Float_From_String

                           (Source    : in     String;

                            Item      :    out Float;

                            Start_Pos : in    Positive;

                            Stop      :    out Natural);

--# derives Item,

--#         Stop  from Source,

--#                    Start_Pos;

--# declare delay;

Reads a Float value starting at Source(Start_Pos) from the given string, following the same rules as the Get_Float procedure, but treating the end of the string as a file terminator. Returns, in the parameter Item the value that corresponds to the sequence input. Returns in Stop the index value such that Source(Stop) is the last character read.

If the sequence input does not have the required syntax then Stop is one less than Start_Pos and the value of Item is undefined.

procedure Put_Float_To_String(Dest      : in out String;

                              Item      : in     Float;

                              Start_Pos : in     Positive;

                              Aft       : in     Natural;

                              Exp       : in     Natural);

--# derives Dest from Aft,

--#                   Dest,

--#                   Exp,

--#                   Item,

--#                   Start_Pos;

--# declare delay;

Outputs the value of the parameter Item to the given string starting at Dest(Start_Pos), following the same rule as for Put_Float to a file, using the Dest'Last - Start_Pos + 1 as the value for Fore.

3.12          Input-Output for Enumeration Types

SPARK_IO contains no predefined routines for the support of input-output for enumeration types.

3.13          Specification of the Package SPARK_IO

There are two versions of SPARK_IO one for SPARK 95 and one for SPARK 2005.  Unfortunately it has not been possible to provide a single package which is compatible with both.  The packages are in customer/lib/spark under the toolset installation directory.  The specification for SPARK_IO for SPARK 95 is in the file spark_io.ads and the specification for SPARK_IO_05 for SPARK 2005 is in the file spark_io_05.ads.  The only difference between the two specifications is the name of the package and the content of the private parts.

3.14          Exceptions in Input-Output

The standard Ada input-output routines generate exceptions if error conditions are encountered, but exceptions are not allowed in SPARK.  Instead, where appropriate a routine has a status parameter, whose returned value indicates whether an error condition has arisen.  The status parameter is of the following type.

type File_Status is (Ok, Status_Error, Mode_Error,

                     Name_Error, Use_Error,

                     Device_Error, End_Error,

                     Data_Error, Layout_Error,

                     Storage_Error, Program_Error);

If a status variable indicates that an error has occurred, any other returned values are undefined, and the onus is on the programmer to organise appropriate recovery actions.  For routines which do not return status information, the programmer should establish that their pre-conditions are always satisfied.

3.15          Example of Input-Output

package Inventory

--# own         Content;

--# initializes Content;

is

 

   Max_Size : constant Integer := 100;

 

   type Inventories is limited private;

   type Part_Numbers is range 1000 .. 9999;

 

   procedure Add(Part   : in     Part_Numbers;

                 Number : in     Positive;

                 Full   :    out Boolean);

   --# global  in out Content;

   --# derives Content from Part, Number, Content &

   --#         Full    from Part, Content;

 

   procedure Look_Up(Part   : in     Part_Numbers;

                     Number :    out Natural);

   --# global  in Content;

   --# derives Number from Part, Content;

 

private

 

   type Sizes is range 0 .. Max_Size;

   subtype Indices is Sizes range 1 .. Sizes'Last;

   type Items is

          record

             Part_Number : Part_Numbers;

             Amount      : Positive;

             Empty       : Boolean;

          end record;

   type  Inventories is array (Indices) of Items;

end Inventory;

 

with SPARK_IO, Inventory;

--# inherit SPARK_IO, Inventory;

--# main_program

procedure Dialogue

--# global  in out SPARK_IO.Inputs

--#                SPARK_IO.Outputs, Inventory.Content;

--# derives SPARK_IO.Inputs,

--#         Inventory.Content from * &

--#         SPARK_IO.Outputs from *, SPARK_IO.Inputs;

is

   Number : Inventory.Part_Numbers;

   Amount : Natural;

 

   procedure Set_Up_Inventory

   --# global  in out Inventory.Content;

   --# derives Inventory.Content from Inventory.Content;

   is

      Unused : Boolean;

   begin

      Inventory.Add(6520, 20,  Unused);

      Inventory.Add(2718, 17,  Unused);

      Inventory.Add(6046, 43,  Unused);

      Inventory.Add(9214, 10,  Unused);

      Inventory.Add(4933, 28,  Unused);

      Inventory.Add(4179, 173, Unused);

      Inventory.Add(7294, 87,  Unused);

   end Set_Up_Inventory;

 

   procedure Enter_Part(Number : out Inventory.Part_Numbers)

   --# global  in out SPARK_IO.Inputs,

   --#                SPARK_IO.Outputs;

   --# derives SPARK_IO.Inputs   from * &

   --#         SPARK_IO.Outputs  from *, SPARK_IO.Inputs &

   --#         Number            from SPARK_IO.Inputs;

   is

      Number_Read : Integer;

      Ok : Boolean;

   begin

      loop

         SPARK_IO.Put_String(SPARK_IO.Standard_Output,

                             "Part number? ", 0);

         SPARK_IO.Get_Integer(SPARK_IO.Standard_Input,

                              Number_Read, 0,Ok);

         exit when Ok and then

           (Number_Read >=

               Integer(Inventory.Part_Numbers'FIRST) and

            Number_Read <=

               Integer(Inventory.Part_Numbers'Last));

         SPARK_IO.Put_Line(SPARK_IO.Standard_Output,

                   "Invalid part number, try again", 0);

         SPARK_IO.New_Line(SPARK_IO.Standard_Output, 1);

      end loop;

      Number := Inventory.Part_Numbers(Number_Read);

   end Enter_Part;

 

begin -- Dialogue

   Set_Up_Inventory;

   loop

      Enter_Part(Number);

      Inventory.Look_Up(Number, Amount);

      SPARK_IO.Set_Col(SPARK_IO.Standard_Output, 5);

      SPARK_IO.Put_String(SPARK_IO.Standard_Output,

                          "Part Number: ", 0);

      SPARK_IO.Put_Integer(SPARK_IO.Standard_Output,

                           Integer(Number),

                           0, 10);

      SPARK_IO.Put_String(SPARK_IO.Standard_Output,

                        " - Items available:", 0);

      SPARK_IO.Set_Out_File_Col(SPARK_IO.Standard_Output, 50);

      if Amount = 0 then

         SPARK_IO.Put_Line(SPARK_IO.Standard_Output,

                           " NONE", 0);

         SPARK_IO.New_Line(SPARK_IO.Standard_Output, 1);

      else

         SPARK_IO.Put_Integer(SPARK_IO.Standard_Output,

                              Amount, 5, 10);

         SPARK_IO.New_Line(SPARK_IO.Standard_Output, 2);

      end if;

 

      exit when False; -- syntactic exit point for analysis

                       -- purposes

   end loop;

end Dialogue;

 

 

Example of an interaction (characters typed by the user are italicized) :

 

Part number? 450

Invalid part number, try again

Part number? 3456

      Part Number: 3456 - Items available:         NONE

Part number? 9214

      Part Number: 9214 - Items available:           10

Document Control and References

Altran Praxis Limited, 20 Manvers Street, Bath BA1 1PX, UK.

Copyright Altran Praxis Limited 2011.  All rights reserved.

File under

SVN:trunk/userdocs/SPARK_Library_UM.doc

Changes history

Issue 0.1 (15th January 1998) Initial draft based on S.P0468.73.25

Issue 1.0 (21st January 1998) After formal review

Issue 1.1 (13th July 2000) Updated for Release 5.0

Issue 2.0 (19th July 2000) Definitive issue following review

Issue 2.1 (18th Nov 2002) New issue updated and corrected to accompany new edition of the SPARK Book and Examiner release 6.3.

Issue 3.0 (18th Nov 2002) Definitive issue following review S.P0468.79.78.

Issue 3.1  (9 June 2003) Conversion to new document format

Issue 3.2 (22 July 2004)  Added Get_Char_Immediate

Issue 3.3 (1st December 2004) Company name changed, no other changes made.

Issue 3.4 (5th January 2005) Definitive issue following review S.P0468.79.88.

Issue 3.5 (22nd November 2005) Line Manager change.

Issue 3.6 (24th November 2006) Updated specification of Delete and Close procedures.

Issue 3.7 (29th January 2009) Renamed from SPARK95_IO to SPARK_IO.

Issue 3.8 (2nd February 2009) Modify copyright notice.

Issue 3.9 (4th February 2010) Rebrand to Altran Praxis Limited

Issue 3.10 (8th February 2010) Changed title and introduction to reflect advent of SPARK 2005.

Issue 3.11 (21st April 2010) Updated to be compatible with Ada 2005.

Issue 3.12 (22nd April 2010) Incorporated changes related to RavenSPARK.

Issue 3.13 (22nd April 2010) Addressed review comments.

Issue 3.14 (12th October 2010): Correct references to the Examiner.

Issue 3.15 (11th November 2010): Rename to SPARK Library User Manual and extend to cover library.

Issue 3.16 (15th November 2010): Updates following review of new SPARK Library material.

Issue 3.17 (15th November 2010): Further updates following review.

Issue 3.18 (14th February 2011): Updated to add packages Interfaces, Ada.Characters.Handling, SPARK.Unsigned. Re-write section 2 and add summary table for all library packages. [K128-014].

Issue 3.19 (13th May 2011): Updated to add SPARK.Ada.Text_IO [K413-009].

Issue 3.20 (19th May 2011): Added SPARK.Ada.Command_Line [K413-009].

Issue 3.21 (28th September 2011); Added SPARK.Ada.Containers [K927-073].

Changes forecast

None.



[1] The no Ada runtime requirement is based on the AdaCore GNAT compilers. For other compilers the runtime requirements would have to be checked with the vendor.