[Spark2014-discuss] Plans for I/O

John McCormick mccormick at cs.uni.edu
Fri Jan 25 20:46:53 CET 2013

Let me see if I understand everything that has been said in this 
discussion on I/O.  The following program is legal SPARK 2014:

with Ada.Text_IO;
procedure P is
    type Dozen is range 0 .. 12;
    package Dozen_IO is new Ada.Text_IO.Integer_IO (Dozen);
    Egg : Dozen;
    Dozen_IO.Get (Egg);
    Ada.Text_IO.Put ("Egg = ");
    Dozen_IO.Put (Egg, 1);
end P;

However, without aspects for Text_IO, we cannot perform a data flow 
analysis, information flow analysis, or verification of freedom from 
exceptions on this program.

We can add a "shadow" file with the aspects for Text_IO (with no need to 
modify Text_IO) that will allow us to perform a data flow analysis, 
information flow analysis, and verification of freedom from 
exceptions.   Of course this example cannot be guaranteed exception free.

So that leaves us with the need for a "shadow" file for Text_IO. Peter 
suggested that this file could be prepared by a third party. I propose 
that the "shadow" file for Text_IO be included in the SPARK 2014 
distribution. That way we have a standard Text_IO for SPARK 2014.  It 
would also be a nice example from which to learn.

Perhaps the SPARK 2014 distribution could include "shadow" files for 
other packages in Ada 2012.   I would think that the bounded containers 
would be prime candidates for augmentation with aspects.


More information about the Spark2014-discuss mailing list