[Spark2014-discuss] Plans for I/O

Arnaud Charlet charlet at adacore.com
Sun Jan 27 19:20:52 CET 2013


> Interesting question, of course in practice the answer can be left
> moot, since you need an Ada 2012 compiler for SPARK 2014, and there
> is no prospect of any such compiler other than GNAT in the forseeable
> future. Theoretically the answer should be yes. Note however, that
> in practice we depend on some gnat specific features, e.g. the extended
> handling of intermediate overflow, and a bunch of implementation
> defined aspects. If some other company makes an Ada 2012 compiler
> they would have to implement corresponding stuff in their compiler.
> This seems even *more* unlikely than another Ada 2012 compiler
> appearing.

Right, although some people could still use the proof aspects without the
run-time ones.

Also, the SPARK 2014 toolset will continue to be standalone, like the current
SPARK is, and not requiring GNAT to be installed (of course without
a compiler installed, you will only get partial benefits from SPARK 2014,
i.e. only the proof aspect, and not the run-time/testing aspect).

Arno


More information about the Spark2014-discuss mailing list