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: 103376,b3f788f59498d3af X-Google-Attributes: gid103376,public,usenet X-Google-Language: ENGLISH,ASCII-7-bit Path: g2news1.google.com!news3.google.com!proxad.net!feeder1-2.proxad.net!newsfeed1.ip.tiscali.net!tiscali!newsfeed2.ip.tiscali.net!news.astraweb.com!newsrouter-eu.astraweb.com!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 From: "Dmitry A. Kazakov" Subject: Re: Exceptions and out procedure arguments (using GNAT GPL) 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: <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> <1182419529.23934.17.camel@kartoffel> Date: Thu, 21 Jun 2007 15:48:59 +0200 Message-ID: <1lyxtgyzyuh8m.yvrov7e73y09.dlg@40tude.net> NNTP-Posting-Date: 21 Jun 2007 15:46:08 CEST NNTP-Posting-Host: 6f61e221.newsspool1.arcor-online.net X-Trace: DXC=ESic==]BZ:af>4Fo<]lROoR1Fl8W>\BH3Y2F?eULYm32D?DNcfSJ;bb[5FCTGGVUmh?4LK[5LiR>kg2GMTnXjL1 On Thu, 21 Jun 2007 11:52:09 +0200, Georg Bauhaus wrote: > On Wed, 2007-06-20 at 22:40 +0200, Dmitry A. Kazakov wrote: >> 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), In which way is it different? I didn't talk about formal correctness or pre-/postconditions, but if you bring this topic in. What is so difficult in: require: ... ... Ptr.all ... ensure: (Ptr=null and Propagated(Constraint_Error)) or ... >> 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. Then I probably understood you wrong. What was your objection? A) to documenting side effects in case of exception propagation, B) to proving formal correctness of a program in the same case, C) to both? A or B or C imply a total ban on any exceptions. Clearly, you need not document anything that cannot happen... >> 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? Yes, if the compiler is broken or else some erroneous execution is underway. > Is erroneous execution correct or incorrect, valid or invalid, and how > does this affect having exceptions a possible values of any type? This question is meaningless. Erroneous execution does not have this property. You should specify a program, be it an application program or then compiler. When the application program enters erroneous execution where ARM allows this, then the compiler used to compile that program is correct. When the specification of the application program allows erroneous execution in the corresponding problem space states, then the program is correct as well. -- Regards, Dmitry A. Kazakov http://www.dmitry-kazakov.de