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 01:36:59 PST Path: archiver1.google.com!newsfeed.google.com!newsfeed.stanford.edu!news.tele.dk!130.133.1.3!fu-berlin.de!uni-berlin.de!193.114.91.187!not-for-mail From: Peter Amey Newsgroups: comp.lang.ada Subject: Re: SPARK Date: Tue, 07 Aug 2001 09:37:13 +0100 Organization: Praxis Critical Systems Message-ID: <3B6FA8B9.5842ADCA@praxis-cs.co.uk> References: NNTP-Posting-Host: 193.114.91.187 Mime-Version: 1.0 Content-Type: text/plain; charset=us-ascii Content-Transfer-Encoding: 7bit X-Trace: fu-berlin.de 997173418 5846845 193.114.91.187 (16 [69815]) X-Mailer: Mozilla 4.73 [en] (Windows NT 5.0; U) X-Accept-Language: en Xref: archiver1.google.com comp.lang.ada:11467 Date: 2001-08-07T09:37:13+01:00 List-Id: 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/ --------------------------------------------------------------------------