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=0.4 required=5.0 tests=BAYES_00,FORGED_MUA_MOZILLA autolearn=no autolearn_force=no version=3.4.4 X-Google-Thread: 103376,ea5071f634c2ea8b X-Google-NewGroupId: yes X-Google-Attributes: gida07f3367d7,domainid0,public,usenet X-Google-Language: ENGLISH,ASCII-7-bit Received: by 10.68.36.6 with SMTP id m6mr1679079pbj.4.1322005945385; Tue, 22 Nov 2011 15:52:25 -0800 (PST) Path: lh20ni7016pbb.0!nntp.google.com!news1.google.com!goblin2!goblin.stu.neva.ru!news.internetdienste.de!news.tu-darmstadt.de!news.belwue.de!newsfeed.arcor.de!newsspool3.arcor-online.net!news.arcor.de.POSTED!not-for-mail Date: Wed, 23 Nov 2011 00:52:23 +0100 From: Georg Bauhaus User-Agent: Mozilla/5.0 (Macintosh; Intel Mac OS X 10.6; rv:7.0.1) Gecko/20110929 Thunderbird/7.0.1 MIME-Version: 1.0 Newsgroups: comp.lang.ada Subject: Re: Generic-Package Elaboration Question / Possible GNAT Bug. References: <7bf9bc32-850a-40c6-9ae2-5254fe220533@f29g2000yqa.googlegroups.com> <4295dc09-43de-4557-a095-fc108359f27f@y42g2000yqh.googlegroups.com> <3snehoqgs8ia$.1nobjem6g6hx6$.dlg@40tude.net> <128rdz2581345$.c4td19l7qp9z$.dlg@40tude.net> <16ipwvpdavifr$.17bxf7if7f6kh$.dlg@40tude.net> <4ecb78b1$0$6643$9b4e6d93@newsspool2.arcor-online.net> <1iofgbqznsviu$.phvidtvxlyj4$.dlg@40tude.net> <4ecbb96e$0$6581$9b4e6d93@newsspool3.arcor-online.net> <4ecbdfdb$0$6629$9b4e6d93@newsspool2.arcor-online.net> <12hfiflyf7pr5$.l3pkpgoid8xt$.dlg@40tude.net> In-Reply-To: <12hfiflyf7pr5$.l3pkpgoid8xt$.dlg@40tude.net> Message-ID: <4ecc35b8$0$7628$9b4e6d93@newsspool1.arcor-online.net> Organization: Arcor NNTP-Posting-Date: 23 Nov 2011 00:52:24 CET NNTP-Posting-Host: a33e9f04.newsspool1.arcor-online.net X-Trace: DXC=I;1PlN52li3=FQB?mjjV50ic==]BZ:af>4Fo<]lROoR1<`=YMgDjhg2\M8Q7Z_Bh2=PCY\c7>ejV81:G4`DH3cX<4VeYWCAo^8? X-Complaints-To: usenet-abuse@arcor.de Xref: news1.google.com comp.lang.ada:19045 Content-Type: text/plain; charset=ISO-8859-1; format=flowed Content-Transfer-Encoding: 7bit Date: 2011-11-23T00:52:24+01:00 List-Id: On 22.11.11 20:15, Dmitry A. Kazakov wrote: >> Meyer: "Programming is a human activity". >> Programmers are led towards a solution during the process of programming. >> Depending on the characteristics of the process, then, >> programmers will produce different results. > > I see no word "debugging" there. A debugging aid is a means of finding mistakes when developing programs. Trying to write assertions pre/post/inv for types and their primitive operations is a means of finding mistakes (bugs) at a number of stages during program development. At one stage, I will state the intended effect of operations on visible object state. At another stage, I might want to know why a subprogram has failed to establish its postcondition and raised. Answering the questions revolves around the very same subject. (It will be cool to make "permissible input" to a subprogram a consequence of 'Valid; is it practical?) Then, evaluation of the conditionals may or may not happen (depending on settings like Assertion_Policy). The intent is to prod programmers into trying harder with one specific goal: to render the conditionals a *consequence* of the program (without assertions), a redundancy, rather than a part of it. A non-trivial consequence that reflects the intent. A non-trivial consequence of a suitable corrected program. When this is achieved, assertions not only will not negatively affect any execution of the program, they also document programmers' intent which is otherwise lost in mere implications, obscure comments, unspoken. > >> DbC (TM), as a characteristic of a process, leads to products >> that lend themselves to proving them correct more than others, >> provided this is possible. > > I suppose drinking coffee does that as well. No, coffee is not known to yield better manifestations of intended subprogram behavior in source text, certainly not better than specifying conditions (program states) framing possible executions. Coffee can have rather obfuscating long term effects, in particular when spilt. > I my experience at least 40% of my debugging > efforts in Ada 95 was spent on catching accessibility checks faults. Ada > 2005 improved that greatly. To me this is a vivid example why dynamic > checks are evil. One may prefer static checks and still want dynamic checks for cases where static checks are not within reach of any tool known to man. > You have to specify the failures you are going to notice. DbC (TM) suggests that you specify the set of states that a program can reach if both the program (a) is started from some state in a set of given states and (b) if all goes well. You do not specify what happens if not both (a) and (b). (Hence, trying alternatives, organized panic, or hoping for false alarm if not both (a) and (b). Rescue clauses are a there to assist the brave only.) > Once > you do qualify them, you would easily be able to avoid them. Yes. > Note that all > the buzz is about noticing something unanticipated. If a description of possible program states in not exhaustive, then, nevertheless, this description establishes a non-empty set of states, and another non-empty set, its complement. When a state is found to be in the complement, then I'd like to know this, even when this knowledge just teaches me that my original attempt at specifying conditions was wrong. I'm told by way of an exception raised. >>> The software which behavior is unknown shall never be executed. >> >> But this is impossible, in general! > > I see the point, since it is impossible do right, you are going to do it > wrong. I am not arguing for or against your or Meyer's motivations. I only > state that it is wrong. You do use compilers, and since it is impossible to know their behavior in general, are you doing wrong? There is no right or wrong in most programs. There is only I/O that satisfies users. I can try to do it right, locally. I'll try to make programs as good as possible. As part of this effort, I can state my expectations of how the subprograms should behave. This may be universally wrong, improved types might be better, but should I do nothing because something is wrong in principle? At least I'm not allowed to follow that path because of deadlines. :-)