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-Thread: 103376,e646052dc594401f X-Google-NewGroupId: yes X-Google-Attributes: gida07f3367d7,domainid0,public,usenet X-Google-Language: ENGLISH,ASCII-7-bit Path: g2news2.google.com!news3.google.com!feeder3.cambriumusenet.nl!feed.tweaknews.nl!138.195.8.3.MISMATCH!news.ecp.fr!news.jacob-sparre.dk!pnx.dk!not-for-mail From: "Randy Brukardt" Newsgroups: comp.lang.ada Subject: Re: Strategies with SPARK which does not support exceptions Date: Tue, 29 Jun 2010 15:05:50 -0500 Organization: Jacob Sparre Andersen Message-ID: References: <93966134-a285-41c5-a7f6-8c59151718a7@k39g2000yqb.googlegroups.com> NNTP-Posting-Host: static-69-95-181-76.mad.choiceone.net X-Trace: munin.nbi.dk 1277841952 1066 69.95.181.76 (29 Jun 2010 20:05:52 GMT) X-Complaints-To: news@jacob-sparre.dk NNTP-Posting-Date: Tue, 29 Jun 2010 20:05:52 +0000 (UTC) X-Priority: 3 X-MSMail-Priority: Normal X-Newsreader: Microsoft Outlook Express 6.00.2900.5843 X-MimeOLE: Produced By Microsoft MimeOLE V6.00.2900.5579 X-RFC2646: Format=Flowed; Original Xref: g2news2.google.com comp.lang.ada:12964 Date: 2010-06-29T15:05:50-05:00 List-Id: "Claude" wrote in message news:d90f60dd-b74f-4eff-b9d8-803ebb64c9d2@z8g2000yqz.googlegroups.com... > >Exceptions are not the best way to process error. (i.e., Not just a >SPARK topic). There is an extra "not" in your statement. :-) You must have meant "Exceptions are the best way to process error." Result codes are dangerous, as ignoring of result codes is one of the major problems in programming, and the resulting bugs are very, very hard to find. (That's because of the difficulty of finding errors of omission.) Perhaps you are too young to remember, but early versions of Windows (3.0, 3.1) had a reputation for being unstable and crashing often. But the problems were mostly not with Windows but rather with programs that tended to ignore the error returns from the Windows API. As such, they tended to continue running but using non-existent Windows handles and the like. Given the lack of memory protection on 16-bit computers, these errors tended to take the entire Windows subsystem with them. We developed a "middle-level" binding for programming Windows, which used exceptions rather than error codes, and programs developed with it tended to be much more stable than the commercial programs we were using at the time --- probably because even when they failed, they didn't take the entire OS with them (just popped up a message box and terminated properly). I understand the problems with safety-critical systems and the need to test to check exceptions, but I believe that the proper solution to those problems is on the line of exception contracts and proving exception absence when necessary to fufill those contracts. In particular, if a routine is declared to not propagate Constraint_Error, then the routine is incorrect if it in fact could propagate that exception. (I'm mildly annoyed that we didn't have time in Ada 2012 to pursue those sorts of contracts seriously.) There is no technical reason that tools like SPARK couldn't support exceptions if they wanted to do so. Compiler optimizers are a form of proof tool, and they have no problem dealing with exceptions. (That's because the control flow caused by exceptions is quite limited, and is generally out of blocks -- outbound flow has little effect on proofs within a block). Returning to the dark ages of programming (that is BE - Before Exceptions) and reintroducing all of the problems of early C code just because of inadequate tools seems like a horrible step backwards to me. This is exactly why I'm not much interested in SPARK itself: because it forces programs back into the style that I originally learned for Fortran IV in 1976: no dynamic allocation, no dynamic calls, no exceptions -- no interest! I'm interested in what SPARK brings to the table in proof capabilities, but I see no reason to give up 3/4rds of Ada to get it. (Remember that Ada allocators, Ada O-O dispatching, Ada access-to-subprogram calls, are all type-safe and provide plenty of opportunity for reasoning). Randy Brukardt.