Re: I'm a noob here.

[Brian Drummond <brian3@shapes.demon.co.uk>]

On Mon, 05 May 2014 05:43:50 -0700, Dan'l Miller wrote:

> In brief, what the OP is asking is:  precisely how does a SPARK compiler
> actually utilize the meta-information annotations?  E.g., precisely how
> does a SPARK compiler make logical inferences regarding correctness of
> Ada-subset source code to verify that the imperative code does what the
> annotations have declared?

There is no such thing as a "SPARK compiler" (at least yet). Every SPARK 
program is a valid Ada program (but not vice-versa) so SPARK is simply 
compiled with an Ada compiler.

What the SPARK tools do is - not compilation - but proving the 
"correctness" of the program - for example, proving that any errors that 
could cause integer overflow are simply not present in the source code.

Or, failing that, pointing out the unprovable parts so that either the 
proof can be completed, or the error preventing proof can be eliminated.

A very large system is unlikely to be suitable for SPARK, but a good 
candidate for Ada. 

Where SPARK comes in is if you can design the system such that a 
relatively small kernel handles the most critical information (security, 
encryption, or arbitrary precision fixed point arithmetic) and cleanly 
interfaces to the rest of the system. That kernel can be formally proven 
using SPARK; the rest of the system is implemented in conventional Ada.

- Brian