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=-0.9 required=5.0 tests=BAYES_00,FORGED_GMAIL_RCVD, FREEMAIL_FROM autolearn=no autolearn_force=no version=3.4.4 X-Google-Thread: 103376,b03962e55f213a92 X-Google-NewGroupId: yes X-Google-Attributes: gida07f3367d7,domainid0,public,usenet X-Google-Language: ENGLISH,CP1252 Path: g2news2.google.com!postnews.google.com!5g2000yqz.googlegroups.com!not-for-mail From: Phil Thornley Newsgroups: comp.lang.ada Subject: Re: What is SPARK about? Date: Sat, 12 Jun 2010 01:30:45 -0700 (PDT) Organization: http://groups.google.com Message-ID: References: NNTP-Posting-Host: 80.177.171.182 Mime-Version: 1.0 Content-Type: text/plain; charset=windows-1252 Content-Transfer-Encoding: quoted-printable X-Trace: posting.google.com 1276331445 31737 127.0.0.1 (12 Jun 2010 08:30:45 GMT) X-Complaints-To: groups-abuse@google.com NNTP-Posting-Date: Sat, 12 Jun 2010 08:30:45 +0000 (UTC) Complaints-To: groups-abuse@google.com Injection-Info: 5g2000yqz.googlegroups.com; posting-host=80.177.171.182; posting-account=Fz1-yAoAAACc1SDCr-Py2qBj8xQ-qC2q User-Agent: G2/1.0 X-HTTP-UserAgent: Mozilla/4.0 (compatible; MSIE 8.0; Windows NT 6.1; WOW64; Trident/4.0; SLCC2; .NET CLR 2.0.50727; .NET CLR 3.5.30729; .NET CLR 3.0.30729; Media Center PC 6.0),gzip(gfe) Xref: g2news2.google.com comp.lang.ada:12627 Date: 2010-06-12T01:30:45-07:00 List-Id: On 11 June, 21:32, Claude wrote: > Ada is a formal language to software engineering. > > What is SPARK about? SPARK is an annotated sublanguage of Ada, intended for use in high- integrity applications. An important property of the language is that it is unambiguous - every valid SPARK program, when compiled by a conforming Ada compiler, has one and only one meaning. Therefore it becomes practicable to reason about the behaviour of a SPARK program based solely on the analysis of the program text. > > I means since SPARK is restricted to the best of Ada, is SPARK better > than Ada to resolving complex engineering applications, or SPARK a > better choice than C/C++ to address leaner systems? =A0(in terms of > compliance to early drafts of DO-178C - certification levels C to A). > > Indeed, the successful applications of SPARK bring to results that are > rather difficult to compare. > > =93The formal design of Tokeneer ID Station (TIS) shows the TIS system > to be a purely sequential system.=94 - =A0(INFORMED design, at section > 2.2, Identification of the SPARK boundary) Support for concurrent programs (RavenSPARK) was added in 2003. > > =93We believe part of the success of proof on SHOLIS is due to the > simple system architecture. =85 > Some large-scale SPARK reasoning are also needed, including support > for abstract proof, before the technology can be extensively used at > the highest level of large systems.=94 - (Is Proof More Cost Effective > Than Testing =96 Section 8, Summary). Support for abstract proof was added in 2000. > > Beyond any theory or academic project, 10 years later, from all the > past SPARK projects=92 experiences, does it happen that SPARK can > address =93purely sequential systems=94 or that SPARK =93can be extensive= ly > used at the highest level of large systems=94? An example of a large, concurrent SPARK program is iFACTS - described by the UK National Air Traffic Service as "the biggest change in air traffic control since radar". > > Claude Cheers, Phil