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.3 required=5.0 tests=BAYES_00, REPLYTO_WITHOUT_TO_CC autolearn=no 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!news4.google.com!feeder1.cambriumusenet.nl!feed.tweaknews.nl!193.141.40.65.MISMATCH!npeer.de.kpn-eurorings.net!npeer-ng0.de.kpn-eurorings.net!newsfeed.arcor.de!newsspool2.arcor-online.net!news.arcor.de.POSTED!not-for-mail From: "Dmitry A. Kazakov" Subject: Re: Operation can be dispatching in only one type Newsgroups: comp.lang.ada User-Agent: 40tude_Dialog/2.0.15.1 MIME-Version: 1.0 Content-Type: text/plain; charset="us-ascii" Content-Transfer-Encoding: 7bit Reply-To: mailbox@dmitry-kazakov.de Organization: cbb software GmbH 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> Date: Wed, 2 Dec 2009 14:35:45 +0100 Message-ID: NNTP-Posting-Date: 02 Dec 2009 14:35:45 CET NNTP-Posting-Host: 58673b94.newsspool4.arcor-online.net X-Trace: DXC=NdH5]Lg3N>CC4i^e1BZ=_H4IUKO3K>:?k`AXcA X-Complaints-To: usenet-abuse@arcor.de Xref: g2news1.google.com comp.lang.ada:8284 Date: 2009-12-02T14:35:45+01:00 List-Id: On Wed, 02 Dec 2009 07:35:39 -0500, John B. Matthews wrote: > In article <1jcbtmi5rztyp$.norvlhez9i9$.dlg@40tude.net>, > "Dmitry A. Kazakov" wrote: > > Georg Bauhaus wrote: > >>> From the Java point of view, there are no false positives >>> or negatives. >> >> Of course there are, because it is a halting problem. So you need >> some optimistic or pessimistic estimation of: >> >> if False then >> Print (X.Tire); -- Is this illegal? If yes, that is a false positive >> end if; > > It would be indeterminate but for doing "a specific conservative flow > analysis." In the specific cases of boolean constant expressions and if > statements, > > if (true) { spare = new Tire(); } // spare assigned > if (1 == 1) { spare = new Tire(); } // spare assigned > if (false) { spare = new Tire(); } // spare unassigned > if (1 == 2) { spare = new Tire(); } // spare unassigned > if (always()) { spare = new Tire(); } // spare unassigned > > static boolean always() { return true; } > > In particular, spare remains unassigned even though the function > always() is always true. > > In Ada, a certain compiler may warn 'variable "N" is assigned but never > read' for the following: > > N : Integer; > if False then N := 1; end if; > > I'm not especially advocating applying the Java rules to Ada, but I like > the warning. Yes, warning is nice. The problem is with making it an error as Georg suggests (and Java does). An error (and its complement "no error") require much more careful definition. "Initialized" is too shaky for that, but for all I find "unassigned" inconsistent with strong typing. A typed object is always assigned because it cannot have any values other than of its type. If we wanted an object to have *certain* values, e.g. "any value different from the default one", then a naive analysis a-la Java is too little to me. I would prefer full blown pre-, postconditions and invariants for such a case. -- Regards, Dmitry A. Kazakov http://www.dmitry-kazakov.de