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,FREEMAIL_FROM autolearn=ham autolearn_force=no version=3.4.4 X-Google-Language: ENGLISH,ASCII-7-bit X-Google-Thread: f849b,b8d52151b7b306d2 X-Google-Attributes: gidf849b,public X-Google-Thread: 103376,a00006d3c4735d70 X-Google-Attributes: gid103376,public X-Google-ArrivalTime: 2003-12-28 18:43:07 PST Path: archiver1.google.com!news1.google.com!sn-xit-02!sn-xit-01!sn-xit-08!supernews.com!small1.nntp.aus1.giganews.com!border1.nntp.aus1.giganews.com!intern1.nntp.aus1.giganews.com!nntp.giganews.com!nntp.comcast.com!news.comcast.com.POSTED!not-for-mail NNTP-Posting-Date: Sun, 28 Dec 2003 20:43:05 -0600 Date: Sun, 28 Dec 2003 21:43:04 -0500 From: "Robert I. Eachus" User-Agent: Mozilla/5.0 (Windows; U; Windows NT 5.0; en-US; rv:1.4) Gecko/20030624 Netscape/7.1 (ax) X-Accept-Language: en-us, en MIME-Version: 1.0 Newsgroups: comp.arch.embedded,comp.lang.ada Subject: Re: Certified C compilers for safety-critical embedded systems References: <3fe00b82.90228601@News.CIS.DFN.DE> <3FE026A8.3CD6A3A@yahoo.com> <$km9afA3DB7$EAYO@phaedsys.demon.co.uk> <3feda44e_3@mk-nntp-1.news.uk.worldonline.com> <3fedbbf0_3@mk-nntp-1.news.uk.worldonline.com> <3fef5f9b_2@mk-nntp-1.news.uk.worldonline.com> In-Reply-To: <3fef5f9b_2@mk-nntp-1.news.uk.worldonline.com> Content-Type: text/plain; charset=us-ascii; format=flowed Content-Transfer-Encoding: 7bit Message-ID: NNTP-Posting-Host: 24.34.214.193 X-Trace: sv3-kBqTGSEF46GEXSxNh55f5S/o2ktyY2B/rdSKpVtqHb5lNgO5XL+ioNAAlgOi+Ok5SzzLF/doGjPKflL!AaUjku5Pw2bJkuHuiIhocbcb1uUJo10v3Zq0oI+wYxC+d7YqIi+aBuF1KtML3w== X-Complaints-To: abuse@comcast.net X-DMCA-Complaints-To: dmca@comcast.net X-Abuse-and-DMCA-Info: Please be sure to forward a copy of ALL headers X-Abuse-and-DMCA-Info: Otherwise we will be unable to process your complaint properly X-Postfilter: 1.1 Xref: archiver1.google.com comp.arch.embedded:6253 comp.lang.ada:3908 Date: 2003-12-28T21:43:04-05:00 List-Id: Ian Bell wrote: > So are you basically saying that Ada requires the function return type to be > bounded and can simply check this against the array bound? No. He is saying that Ada types and subtypes typically contain information about expected values that will be checked at compile time or run time as appropriate. If the subtypes "statically match", which does not mean that the bounds are static, it can be determined at compile time that no run-time check will be necessary. And of course, that means you don't have to worry about what happens if the check fails. In fact, years ago in Ada 83, I had a nice tool that detected every place that a run-time bound was tested by the compiler. About one-third of the cases were cases where rearranging the code would allow the compiler to eliminate the check, one-third were really needed, and the rest were bugs. Today I use the SPARK analyzer or other (ASIS) tools to do essentially the same checking. You are not required to use subtypes which are correctly bounded in Ada. But it is a big help to (static) debugging and program correctness if you do. And in another thread on comp.lang.ada we are discussing that it is a VERY useful property of Ada, not just because it makes it more likely that the program will correctly implement the requirements. It also often results in missed requirements being detected. I have lost track of the number of times when a "simple question" about the right way to declare a subtype or assign a default value in Ada, has gone back to the design team to write a new requirement, as soon as they figured out what it should be. My favorite example of this came from a project which was doing a flight control system for a fighter aircraft. They wanted to know if it was possible to implement the system as a round-robin scheduler in Ada. I sent back a template of what the final code would look like, and a set of questions that needed to be answered before the code could be written--or the question answered. A month or so later I called back and asked whether that had solved their problem. The answer was that they had resolved fifteen of the seventeen questions I had asked and they only had two left! Eventually, they used hard-deadline scheduling because that way they could resolve the remaining questions. Notice that the questions in one sense had nothing to do with Ada. Ada had made the need for answers obvious, but the questions could be stated in terms that were actually independent of programming language and hardware. "If the tracking of incoming missles exceeds its time slot should it be aborted or allowed to delay the navigation function?" "If the aircraft state update takes longer than expected--read time-outs on status inquiries due to damage--should it restart where it left off in the next time-slot, continue execution at low-priority, or reset to the beginning for the next time slot but skip the failed check?" These are not easy questions, and there may be no "right" answer in the sense of one that will always save the aircraft. But choosing the best answer may save some aircraft that would otherwise be lost. -- Robert I. Eachus "The war on terror is a different kind of war, waged capture by capture, cell by cell, and victory by victory. Our security is assured by our perseverance and by our sure belief in the success of liberty." -- George W. Bush