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=unavailable autolearn_force=no version=3.4.4 Path: eternal-september.org!reader01.eternal-september.org!reader02.eternal-september.org!news.eternal-september.org!mx02.eternal-september.org!feeder.eternal-september.org!news.freedyn.net!news.redatomik.org!nntpfeed.proxad.net!proxad.net!feeder2-2.proxad.net!cleanfeed2-a.proxad.net!nnrp2-1.free.fr!not-for-mail From: Xavier Petit Subject: Re: Ada.Strings.Fixed.Count raises Storage_Error Newsgroups: comp.lang.ada References: <57346ac8$0$4570$426a74cc@news.free.fr> <57707888$0$5274$426a34cc@news.free.fr> <43a09f40-fdea-461e-9b0a-4419b86c1a56@googlegroups.com> X-Mozilla-News-Host: news://news.free.fr Date: Tue, 28 Jun 2016 20:25:54 +0200 User-Agent: Mozilla/5.0 (X11; Linux x86_64; rv:45.0) Gecko/20100101 Icedove/45.1.0 MIME-Version: 1.0 In-Reply-To: <43a09f40-fdea-461e-9b0a-4419b86c1a56@googlegroups.com> Content-Type: text/plain; charset=utf-8; format=flowed Content-Transfer-Encoding: 8bit Message-ID: <5772c133$0$702$426a74cc@news.free.fr> Organization: Guest of ProXad - France NNTP-Posting-Date: 28 Jun 2016 20:25:55 CEST NNTP-Posting-Host: 78.217.21.11 X-Trace: 1467138355 news-1.free.fr 702 78.217.21.11:37496 X-Complaints-To: abuse@proxad.net Xref: news.eternal-september.org comp.lang.ada:30962 Date: 2016-06-28T20:25:55+02:00 List-Id: Le 27/06/2016 à 06:48, rieachus@comcast.net a écrit : > On Sunday, June 26, 2016 at 8:51:21 PM UTC-4, Xavier Petit wrote: > >> Every parameters of a subprogram should be anticipated and produce a >> coherent behavior. It’s hard but Ada is especially here to make it easier. > > Gödel, Escher, Bach: An Eternal Golden Braid, is a 1979 book by Douglas Hofstadter that is now in its 20th edition. > > It tries, among other things to explain the reality revealed by Gödel's proofs. One of those consequences is that you can't build a perfect compiler. In fact, the gnat in Ada Core Technologies logo is a cute reminder that every compiler must have at least one bug. Not, these things are so complex they can never be perfect, but even some very simple software tools are subject to Gödel's findings--no system above a rudimentary complexity (embedding of Peano arithmetic) can be bug-free. > > Worse, the Halting Problem is a very simple proof that you cannot write a program that will perfectly determine whether a given software program will halt. (Or not halt, if you work on embedded systems like I did.) > > So trying for perfection in compilers, programming languages, and even many software programs is a mug's game. You can't do it, you don't know where other corner cases are, and you can't even document all of the bugs. Yes, it is possible to "prove" software correctness for some programs. But for those same programs, you have just moved the target, from perfect software to perfect requirements. > > The Airbus 320 had a major software bug in spite of the correctness proof tools used. If a plane cross the last waypoint before the destination, the flight guidance system would put the airplane in the correct glidepath for the chosen runway as quickly as possible, even if that location was under a few thousand feet of granite. Strasbourg suddenly dove straight down. Oops! Perfect software implementation of a bad requirement. (https://www.flightglobal.com/news/articles/air-france-ceo-jean-cyril-spinetta-defends-rejection-of-gpws-equipment-on-air-inter-a320-fleet-despite-fatal-1992-st-odile-mountainside-crash-210280/ The obfuscation thrown about by Airbus and the French government still continues. But at least the bug in "flight path angle mode" in the flight controller got fixed. This list will show you why I still won't fly on an Airbus 310,20, or 21: https://en.wikipedia.org/wiki/Accidents_and_incidents_involving_the_Airbus_A320_family ) > > Thank you for the very interesting informations and explanations, I think I understand. After tests, as you said the performance penalty is very important (from 5 to 33% depending optimization options) if we do the test inside the loop. But this is not only a special case, it’s a unique case, so the source code solution should be something like : if Source'Last = Positive'Last and then Pattern'Length = 1 then return Boolean'Pos (Source (Source'Last) = Pattern (Pattern'First)); end if; inserted between the empty pattern exception and the loops of Count. A function “Count_Wrapper” that has the specification of Ada.Strings.Fixed.Count and code : if Source'Last = Positive'Last and then Pattern'Length = 1 then return Boolean'Pos (Source (Source'Last) = Pattern (Pattern'First)); else return Ada.Strings.Fixed.Count (Source, Pattern, Mapping); end if; On intel64 & cortex A7 (raspberry pi 2), with(out) options, this function called with Ada.Command_Line.Argument (1) pattern and hundred millions of random size strings sources has no big overhead. Do you think those unique and limit cases are worth a modification ? -- Xavier Petit