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: 103376,b3f788f59498d3af X-Google-Attributes: gid103376,public,usenet X-Google-Language: ENGLISH,ASCII-7-bit Path: g2news1.google.com!news2.google.com!border1.nntp.dca.giganews.com!nntp.giganews.com!newsfeed00.sul.t-online.de!t-online.de!newsfeed.freenet.de!news.teledata-fn.de!newsfeed.arcor.de!newsspool3.arcor-online.net!news.arcor.de.POSTED!not-for-mail Date: Wed, 20 Jun 2007 21:16:11 +0200 From: Georg Bauhaus Organization: # User-Agent: Thunderbird 1.5.0.12 (Macintosh/20070509) MIME-Version: 1.0 Newsgroups: comp.lang.ada Subject: Re: Exceptions and out procedure arguments (using GNAT GPL) References: <79c673pq5htg508nkoi935n3udqg5ps7r8@4ax.com> <1182181497.595409.300500@a26g2000pre.googlegroups.com> <1182238493.512406.168820@o61g2000hsh.googlegroups.com> <1182266486.650797.262430@a26g2000pre.googlegroups.com> <4678c6a0$0$23135$9b4e6d93@newsspool1.arcor-online.net> <1o6rnwgzezcr2$.mv31ct5mmmso$.dlg@40tude.net> <1182329193.7759.30.camel@kartoffel> <1182334409.7759.39.camel@kartoffel> <1mhmyqf4l1lzn$.42eeylu5yrjk.dlg@40tude.net> <1182349018.7759.51.camel@kartoffel> <1d3hk782jujgz$.182e58lrsup7s.dlg@40tude.net> In-Reply-To: <1d3hk782jujgz$.182e58lrsup7s.dlg@40tude.net> Content-Type: text/plain; charset=ISO-8859-1; format=flowed Content-Transfer-Encoding: 7bit Message-ID: <46797c40$0$23133$9b4e6d93@newsspool1.arcor-online.net> NNTP-Posting-Date: 20 Jun 2007 21:13:04 CEST NNTP-Posting-Host: cde56cc8.newsspool1.arcor-online.net X-Trace: DXC=7l6QZQD:A2985[]]\]T081ic==]BZ:af>4Fo<]lROoR1Fl8W>\BH3Y2BoHXG0>QL@oPPgDLKK8HA\73caJ Dmitry A. Kazakov wrote: > On Wed, 20 Jun 2007 16:16:58 +0200, Georg Bauhaus wrote: > >> On Wed, 2007-06-20 at 14:58 +0200, Dmitry A. Kazakov wrote: >>> On Wed, 20 Jun 2007 12:13:29 +0200, Georg Bauhaus wrote: >>> >>>> On Wed, 2007-06-20 at 11:29 +0200, Dmitry A. Kazakov wrote: >>>>> On Wed, 20 Jun 2007 10:46:33 +0200, Georg Bauhaus wrote: >>>>> >>>>>>>> And can you document all side effects on by reference (or global) >>>>>>>> variables at all, in the presence of exceptions? >>>>>>> That depends on the meaning of "all." Certainly, we cannot control >>>>>>> side-effects on the CPU's cache or on the green gas emission caused by >>>>>>> consuming electricity during subprogram execution... >>>>>> Yes, no need repeating the absurd. So what is the meaning of "all >>>>>> side effects"? >>>>> Language-distinguishable sets of program states corresponding the >>>>> identified elements of the problem space. >>>> Rephrasing the notion won't help defining it. >>> OK, give your definition of [side] effect of program execution so that we >>> could discuss your point. >> A side effect of a subprogram P is a possible update of an object >> (in some partition) that is not mentioned in P's parameter profile. > > 1. What is "object"? Defined for Ada. > 2. What is "update"? Assignment. > 3. Why this does not include "objects" mentioned in the parameter profile? Because parameters and returns are better described by "effect of P", not side effect of P. Reasoning/annotations/... will include them, for sure. (cf. # global in SPARK.) > 4. Which "updates" are you suggesting not to document? I'm not suggesting to document or not to document. I'm suggesting that documenting all effects (wrt program state) of a subprogram, including non-local goto is quite ambitious. Can the idea be made more than a vague hint. > 6. When? In principle. Can we have a definition of a correct outcome of P that includes exceptions raised by P, not handled by P, within the Ada language framework? If not, can you describe the extensions needed? > 7. Why? Because you said it would be possible, or at least that is what I had understood. Is it possible, and if you say yes, then how would we do this in Ada?