comp.lang.ada
 help / color / mirror / Atom feed
From: Xavier Petit <xpetit@becoast.fr>
Subject: Re: Ada.Strings.Fixed.Count raises Storage_Error
Date: Tue, 28 Jun 2016 20:25:54 +0200
Date: 2016-06-28T20:25:55+02:00	[thread overview]
Message-ID: <5772c133$0$702$426a74cc@news.free.fr> (raw)
In-Reply-To: <43a09f40-fdea-461e-9b0a-4419b86c1a56@googlegroups.com>

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


  reply	other threads:[~2016-06-28 18:25 UTC|newest]

Thread overview: 29+ messages / expand[flat|nested]  mbox.gz  Atom feed  top
2016-05-12 11:36 Ada.Strings.Fixed.Count raises Storage_Error Xavier Petit
2016-05-12 15:22 ` Tero Koskinen
2016-05-12 22:05 ` Georg Bauhaus
2016-06-26 21:18   ` Victor Porton
2016-06-26 23:23     ` rieachus
2016-06-27  0:21       ` Jeffrey R. Carter
2016-06-27  4:00         ` rieachus
2016-06-27  0:51       ` Xavier Petit
2016-06-27  4:48         ` rieachus
2016-06-28 18:25           ` Xavier Petit [this message]
2016-06-29 18:49           ` Niklas Holsti
2016-06-29 19:40             ` Jeffrey R. Carter
2016-06-29 19:57             ` Dmitry A. Kazakov
2016-07-01 11:48               ` rieachus
2016-07-01 13:08                 ` Dmitry A. Kazakov
2016-06-27  8:29       ` Simon Wright
2016-06-27  8:41         ` Georg Bauhaus
2016-06-29  8:15       ` Niklas Holsti
2016-06-29  9:13         ` J-P. Rosen
2016-06-29 17:43           ` Niklas Holsti
2016-06-29 18:19             ` J-P. Rosen
2016-06-29 20:30             ` Robert A Duff
2016-06-30  5:38               ` Niklas Holsti
2016-07-01 10:40                 ` rieachus
2016-07-01 10:55                   ` J-P. Rosen
2016-07-01 12:17                     ` rieachus
2016-07-01 12:55                       ` G.B.
2016-06-27 12:52     ` Victor Porton
2016-05-12 22:56 ` Randy Brukardt
replies disabled

This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox