SPARK in Ada was Re:Certified C compilers for safety-critical embedded

SPARK in Ada was Re:Certified C compilers for safety-critical embedded

[Robert C. Leif]

Ed Falis wrote:
"I think the subset of Ada used by SPARK is a good counter-example.  It's 
not the only one in use, since Ada provides pragmas that restrict 
functionality to achieve a higher level of determinism, or to 
reduce/remove the need for runtime library support."

SPARK is to a large extent a subset compiler. Robert Dewar was correct in
stating that it was better to permit subseting of a complete compiler than
create a compiler consisting of a subset of the language. Since GNAT and
other Ada compilers have ASIS, many of the assertions required by SPARK
could be generated by ASIS and included into the sources as useful and
informative comments or better yet assertions(Ada'0? and GNAT). A compiler
switch could be used for this. These assertions and others added by the user
could then be checked by some of the present and all future versions of Ada.
This would immediately have the advantage over the present version of SPARK
of permitting the use of both generics that are instantiated at compile time
and class-wide subprogram calls that are also known at compile time.
Essentially, this would provide an Ada executable that either did not
require or use a heap or only required the use of a heap for arrays that are
created at run-time. This use of the heap could also be eliminated by the
use of bounded arrays where the maximum size of the array is specified and
the array can be created to be any size up to the maximum.  Bounded strings
would then be a special case of this new type of array.

Bob Leif