From mboxrd@z Thu Jan 1 00:00:00 1970 X-Spam-Checker-Version: SpamAssassin 3.4.4 (2020-01-24) on polar.synack.me X-Spam-Level: X-Spam-Status: No, score=-1.9 required=5.0 tests=BAYES_00 autolearn=ham autolearn_force=no version=3.4.4 X-Google-Language: ENGLISH,ASCII-7-bit X-Google-Thread: 103376,dce17094f2aeee50 X-Google-Attributes: gid103376,public X-Google-ArrivalTime: 2001-08-07 07:42:06 PST Path: archiver1.google.com!newsfeed.google.com!newsfeed.stanford.edu!paloalto-snf1.gtei.net!news.gtei.net!enews.sgi.com!newshub2.rdc1.sfba.home.com!news.home.com!news2.POSTED!not-for-mail Message-ID: <3B6FFF1A.6050103@dont.spam.me> From: McDoobie User-Agent: Mozilla/5.0 (X11; U; Linux i586; en-US; rv:0.9.3) Gecko/20010801 X-Accept-Language: en-us MIME-Version: 1.0 Newsgroups: comp.lang.ada Subject: Re: SPARK References: <3B6FA8B9.5842ADCA@praxis-cs.co.uk> Content-Type: text/plain; charset=us-ascii; format=flowed Content-Transfer-Encoding: 7bit Date: Tue, 07 Aug 2001 14:42:05 GMT NNTP-Posting-Host: 24.0.109.49 X-Complaints-To: abuse@home.net X-Trace: news2 997195325 24.0.109.49 (Tue, 07 Aug 2001 07:42:05 PDT) NNTP-Posting-Date: Tue, 07 Aug 2001 07:42:05 PDT Organization: Excite@Home - The Leader in Broadband http://home.com/faster Xref: archiver1.google.com comp.lang.ada:11503 Date: 2001-08-07T14:42:05+00:00 List-Id: 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