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!news4.google.com!proxad.net!feeder1-2.proxad.net!news.tele.dk!news.tele.dk!small.news.tele.dk!lnewsinpeer00.lnd.ops.eu.uu.net!bnewsinpeer00.bru.ops.eu.uu.net!emea.uu.net!newsfeed.arcor.de!newsspool3.arcor-online.net!news.arcor.de.POSTED!not-for-mail Newsgroups: comp.lang.ada Subject: Re: Exceptions and out procedure arguments (using GNAT GPL) From: Georg Bauhaus In-Reply-To: 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> <46797c40$0$23133$9b4e6d93@newsspool1.arcor-online.net> Content-Type: text/plain Content-Transfer-Encoding: 7bit Message-ID: <1182419529.23934.17.camel@kartoffel> Mime-Version: 1.0 X-Mailer: Evolution 2.10.1 Date: Thu, 21 Jun 2007 11:52:09 +0200 Organization: Arcor NNTP-Posting-Date: 21 Jun 2007 11:52:04 CEST NNTP-Posting-Host: 23e26b4f.newsspool2.arcor-online.net X-Trace: DXC=::\OXU9[SY0_A0jCfgHO6>A9EHlD;3Yc24Fo<]lROoR18kF On Wed, 2007-06-20 at 22:40 +0200, Dmitry A. Kazakov wrote: > On Wed, 20 Jun 2007 21:16:11 +0200, Georg Bauhaus wrote: > > > 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. [I'm cutting out your questions because they give details about the very things I'm kindly asking you to provide. I'm curious about your exact formal, writable, specifications so that programmers can write expressions detailed at a level that is on a par with, say, parameter profiles, or assertions.] > >> 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. > > I don't know how often you are using global variables, but if documenting > side effects looks ambitious, then you should probably review your > programming guidelines. I'm not taking this as an argument when your offer is that there exists a LRM that says "dynamic semantics". We cannot just squeeze a copy of the LRM a bit and expect to have a formal apparatus for expressing formal expectations in your *Different-from-DbC* *states-plus-exceptions* approach (IIUC), together with a way to mechanically checking our assumptions (which is part of why we have high level programming languages, and compilers.) > See any part of ARM which defines "dynamic semantics" of an operation. I think I fail to express myself clearly, as IMHO you talk evasively around the real question: What is your formal documentation language, with set-of-words = {program variables, pre/post/inv, ...} such that a compiler/translator/analysis program can be used as a programmer's aid in demonstrating correctness of a program. > For the operation ".all" the *only* correct outcome with the parameter null > is propagation Constraint_Error. Note that this also presumes no side > effects like: > > X := 4; > Ptr := null; > .. Ptr.all ...; -- Surprise, this shall not change X! > > Is it ambitious to require? Will it change Ptr.all? > For the > things which may have unpredictable side effects ARM uses the notion of > erroneous execution. Is erroneous execution correct or incorrect, valid or invalid, and how does this affect having exceptions a possible values of any type?