Re: SPARK

[McDoobie <chris@dont.spam.me>]

Peter Amey wrote:
> 
> 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
> 
> 
> 

This is something I'd certainly like to get my hands on. The problem is 
that it costs too damn much!

But, perhaps, instead of re-creating the entire Spark toolchain, one(or 
a group) could create a new toolchain, or an Open Source(or Free 
Software) subset of Spark geared around things that Open Source 
programmers use most often.
I'm sure Praxis could reap a bundle of they were to put together a 
package geared(and priced) towards individual developers, in addition to 
the huge Corporate and Military systems they work with right now. Even 
just a small, but carefully chosen subset of the Spark system, priced 
right, and sitting on the shelf at CompUSA would not only make them 
loads of money(assuming they market it properly), but would likely 
attract large numbers of developers to Ada in general. Not to mention 
making at least a small percentage of overall improvement in the types 
of software being developed today.

Just a thought. Maybe it's wishful thinking.

I would jump at the chance to develop a similar LGPLd package. The 
problem is that I dont have the amount of experience doing actual 
engineering that would be required to develop anything worthwhile. 
However, I'd certainly be glad to work under someone who does.

Thoughts? Possibilities? Potential?

What do the SPARK guys think?

McDoobie
chris@dont.spam.me