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=-2.9 required=5.0 tests=BAYES_00,MAILING_LIST_MULTI autolearn=unavailable autolearn_force=no version=3.4.4 X-Google-Language: ENGLISH,ASCII-7-bit X-Google-Thread: 103376,26f3678b145d23ef,start X-Google-Attributes: gid103376,public X-Google-ArrivalTime: 2003-12-28 11:29:08 PST Path: archiver1.google.com!news2.google.com!newsfeed2.dallas1.level3.net!news.level3.com!crtntx1-snh1.gtei.net!washdc3-snh1.gtei.net!news.gtei.net!ngpeer.news.aol.com!feed2.newsreader.com!newsreader.com!news2.telebyte.nl!news.completel.fr!ircam.fr!freenix!enst.fr!melchior!cuivre.fr.eu.org!melchior.frmug.org!not-for-mail From: "Robert C. Leif" Newsgroups: comp.lang.ada Subject: SPARK in Ada was Re:Certified C compilers for safety-critical embedded Date: Sun, 28 Dec 2003 11:28:52 -0800 Organization: Newport Instruments Message-ID: Reply-To: rleif@rleif.com NNTP-Posting-Host: lovelace.ada-france.org Mime-Version: 1.0 Content-Type: text/plain; charset="us-ascii" Content-Transfer-Encoding: 7bit X-Trace: melchior.cuivre.fr.eu.org 1072639747 575 80.67.180.195 (28 Dec 2003 19:29:07 GMT) X-Complaints-To: usenet@melchior.cuivre.fr.eu.org NNTP-Posting-Date: Sun, 28 Dec 2003 19:29:07 +0000 (UTC) To: "'Ed Falis'" , Return-Path: X-Mailer: Microsoft Office Outlook, Build 11.0.5510 X-MimeOLE: Produced By Microsoft MimeOLE V6.00.2800.1165 Thread-Index: AcPNeFnvyKcgDuWNTD+dqvyz7nkt/Q== X-Virus-Scanned: by amavisd-new-20030616-p5 (Debian) at ada-france.org X-BeenThere: comp.lang.ada@ada-france.org X-Mailman-Version: 2.1.3 Precedence: list List-Id: Gateway to the comp.lang.ada Usenet newsgroup List-Unsubscribe: , List-Post: List-Help: List-Subscribe: , Xref: archiver1.google.com comp.lang.ada:3895 Date: 2003-12-28T11:28:52-08:00 Ed Falis wrote: "I think the subset of Ada used by SPARK is a good counter-example. It's not the only one in use, since Ada provides pragmas that restrict functionality to achieve a higher level of determinism, or to reduce/remove the need for runtime library support." SPARK is to a large extent a subset compiler. Robert Dewar was correct in stating that it was better to permit subseting of a complete compiler than create a compiler consisting of a subset of the language. Since GNAT and other Ada compilers have ASIS, many of the assertions required by SPARK could be generated by ASIS and included into the sources as useful and informative comments or better yet assertions(Ada'0? and GNAT). A compiler switch could be used for this. These assertions and others added by the user could then be checked by some of the present and all future versions of Ada. This would immediately have the advantage over the present version of SPARK of permitting the use of both generics that are instantiated at compile time and class-wide subprogram calls that are also known at compile time. Essentially, this would provide an Ada executable that either did not require or use a heap or only required the use of a heap for arrays that are created at run-time. This use of the heap could also be eliminated by the use of bounded arrays where the maximum size of the array is specified and the array can be created to be any size up to the maximum. Bounded strings would then be a special case of this new type of array. Bob Leif