Re: SPARK

[Peter Amey <peter.amey@praxis-cs.co.uk>]

programmer wrote:
> 
> I have been to various web sites like www.sparkada.com in an effort
> to research the SPARK language.
> 
> Is SPARK Examiner the only SPARK language tool available?
> 
> What is the cost?
> 
> Are there any open source alternatives?
> 
> I am fascinated by the concept of verifying correctness
> completely at compiler/pre-compile time.
> 
> Answers to my questions and any additional information
> would be greatly appreciated.


Thanks for the interest (and to Hambut who provided some accurate
answers).

There are two aspects to SPARK: the language definition and the analysis
tool (the Examiner).  The ingredients are complementary because it the
tightness of the language definition which permits deep analysis to be
performed in computationally efficient ways.  It also allows the
analysis to be performed on incomplete programs, during development,
which is vital if the approach is to save time and money.

I often characterize SPARK as an "Ada amplifier".  If you think of all
the things like strong typing, constraint checking etc. that makes Ada
efficient at error prevention and early error detection then add in a
whole raft of extra checks ranging from system wide data flow analysis
up to proof of exception freedom then that is SPARK.  (Incidently, to
pick up on another thread in CLA, proof of exception freedom would also
be a proof of invulnerability to buffer overflow attacks without any
run-time overhead.)

The language definition is freely available as is the paper that lays
the foundations of the Examiner's method of data and information flow
analysis.  So, if you are really keen, much of the requirements
specification for an open source alternative to the Examiner exists. 
You should be warned, however, that I have spent most of the last 10
years of my life, with some very high quality help, writing and
improving the Examiner (which BTW is written in SPARK and analyses and
approves of itself) so the task is not one for the faint hearted.

The Barnes book has recently been updated and the publishers have not
done a very good job of telling people about it: if you try and get a
copy and are told it is out of print then tell them they are wrong!  The
demo Examiner is limited only in size; all analysis options are
available.

Finally, those whose appetites have been whetted may like to know that
we are running an open SPARK course in the USA from 24th - 28th
September.  Details on www.sparkada.com

Peter


-- 
---------------------------------------------------------------------------   
      __         Peter Amey,  
        )                    Praxis Critical Systems Ltd
       /                     20, Manvers Street, Bath, BA1 1PX
      / 0        Tel: +44 (0)1225 466991
     (_/         Fax: +44 (0)1225 469006
                 http://www.praxis-cs.co.uk/

--------------------------------------------------------------------------