[Spark2014-discuss] Plans for I/O
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:
procedure P is
type Dozen is range 0 .. 12;
package Dozen_IO is new Ada.Text_IO.Integer_IO (Dozen);
Egg : Dozen;
Ada.Text_IO.Put ("Egg = ");
Dozen_IO.Put (Egg, 1);
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