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: a07f3367d7,dbbbb21ed7f581b X-Google-Attributes: gida07f3367d7,public,usenet X-Google-NewGroupId: yes X-Google-Language: ENGLISH,ASCII-7-bit Path: g2news1.google.com!news3.google.com!feeder.news-service.com!newsfeed.freenet.de!217.188.199.168.MISMATCH!takemy.news.telefonica.de!telefonica.de!newsfeed.arcor.de!newsspool4.arcor-online.net!news.arcor.de.POSTED!not-for-mail Date: Thu, 03 Dec 2009 12:24:43 +0100 From: Georg Bauhaus User-Agent: Thunderbird 2.0.0.23 (Macintosh/20090812) MIME-Version: 1.0 Newsgroups: comp.lang.ada Subject: Re: Operation can be dispatching in only one type References: <025105f2-5571-400e-a66f-ef1c3dc9ef32@g27g2000yqn.googlegroups.com> <0f177771-381e-493b-92bb-28419dfbe4e6@k19g2000yqc.googlegroups.com> <1nbcfi99y0fkg.1h5ox2lj73okx$.dlg@40tude.net> <59acf311-3a4a-4eda-95a3-22272842305e@m16g2000yqc.googlegroups.com> <4b150869$0$6732$9b4e6d93@newsspool2.arcor-online.net> <18vlg095bomhd.8bp1o9yysctg$.dlg@40tude.net> <4b152ffe$0$7615$9b4e6d93@newsspool1.arcor-online.net> <19nhib6rmun1x$.13vgcbhlh0og9$.dlg@40tude.net> <4b1557d0$0$7623$9b4e6d93@newsspool1.arcor-online.net> <4b15bf2b$0$7623$9b4e6d93@newsspool1.arcor-online.net> <1jcbtmi5rztyp$.norvlhez9i9$.dlg@40tude.net> In-Reply-To: Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 7bit Message-ID: <4b179ffb$0$6591$9b4e6d93@newsspool3.arcor-online.net> Organization: Arcor NNTP-Posting-Date: 03 Dec 2009 12:24:43 CET NNTP-Posting-Host: 2c1f199e.newsspool3.arcor-online.net X-Trace: DXC=D>=PJ]EhG;dj5k5aEF7ISmMcF=Q^Z^V3h4Fo<]lROoRa8kFjLh>_cHTX3jm=G[;M;=bM`a X-Complaints-To: usenet-abuse@arcor.de Xref: g2news1.google.com comp.lang.ada:8298 Date: 2009-12-03T12:24:43+01:00 List-Id: Randy Brukardt schrieb: > "Dmitry A. Kazakov" wrote in message > news:1jcbtmi5rztyp$.norvlhez9i9$.dlg@40tude.net... > ... >> No the problem is whether to treat a call to the body as legal. The >> problem >> is that you could not rely on its contract (out Car), in order to be able >> to decide whether this call would "initialize" the object. > [...] > This is not at all a simple topic, and the sort of simple rule used > by Java does little other than give a false sense of security (and a lot of > annoying errors in code that has no problems). After reading your recent hints to compatibility and single pass compilation preventing flow analysis for legality decisions, I noticed the possibility of a restrictions pragma, too. Is it really annoying when programmers are forced to state, explicitly, what they seem to be knowing? That is, for example, "I know that no ELSE is missing in the following code, therefore I have omitted a no-op else branch" X : Some_Type; begin if I_Know_What_This_Does (P) then X := Assign_It; end if; Use_It := Involve (X); When I try to change a program, I find it annoying to *not* see an ELSE branch that does then become a missing ELSE branch. The desired change turns a one-way flow into a blind alley... The code typically looks like this: X : Some_Type; begin if Has_Worked_For_Me (P) then X := Assign_it; end if; I_Can_Use_It := Involve (X); -- (formally fine in Ada, though not in Java or SPARK) The incompleteness of information here can be avoided, to some extent I think, and that's the reason I find the Java rule to be helpful, or the Ada warning, or the pragma which you have suggested. Not really annoying. I can no longer like seeing only half of the cases of Boolean covered in an IF, explicitly. To me, SPARK is not an annoyance when it refuses to accept the above code, since flow analysis reveals the possibility of missing initilization. The Ada programmer may well have decided the halting question for I_Know_What_This_Does or Has_Worked_For_Me. However, I'd sure like to be hinted to his reasons and not just take inspiration from a missing ELSE branch. Could a compiler make some good use of code like the following as a minimal way to express the programmer's valuable knowledge? Or some less intrusive (annoying?) pragma or syntax or ...? X : Some_Type; begin if Whatever (P) then X := Assign_it; else -- Stupid Ada configuration requires this. -- Yeah, X is valid because ... -- ... Whatever (P) is always true, you know. pragma Assert (Some_Type'Valid (X)); null; end if;