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,FREEMAIL_FROM autolearn=unavailable autolearn_force=no version=3.4.4 X-Received: by 10.107.27.136 with SMTP id b130mr10307045iob.35.1523021700709; Fri, 06 Apr 2018 06:35:00 -0700 (PDT) X-Received: by 2002:a9d:554b:: with SMTP id h11-v6mr1454559oti.12.1523021700535; Fri, 06 Apr 2018 06:35:00 -0700 (PDT) Path: eternal-september.org!reader01.eternal-september.org!reader02.eternal-september.org!feeder.eternal-september.org!news.unit0.net!peer01.am4!peer.am4.highwinds-media.com!peer03.iad!feed-me.highwinds-media.com!news.highwinds-media.com!u184-v6no531597ita.0!news-out.google.com!u64-v6ni468itb.0!nntp.google.com!k65-v6no541132ita.0!postnews.google.com!glegroupsg2000goo.googlegroups.com!not-for-mail Newsgroups: comp.lang.ada Date: Fri, 6 Apr 2018 06:35:00 -0700 (PDT) In-Reply-To: Complaints-To: groups-abuse@google.com Injection-Info: glegroupsg2000goo.googlegroups.com; posting-host=87.116.176.31; posting-account=z-xFXQkAAABpEOAnT3LViyFXc8dmoW_p NNTP-Posting-Host: 87.116.176.31 References: <1b44444f-c1b3-414e-84fb-8798961487c3@googlegroups.com> <62ee0aac-49da-4925-b9aa-a16695b3fc45@googlegroups.com> <9879872e-c18a-4667-afe5-41ce0f54559f@googlegroups.com> <17b6d5b9-5909-4f0c-ab25-9b3cf4fd0450@googlegroups.com> User-Agent: G2/1.0 MIME-Version: 1.0 Message-ID: <2be6c759-1a2f-48fc-81b1-ffab1d1c957d@googlegroups.com> Subject: Re: Interesting article on ARG work From: Bojan Bozovic Injection-Date: Fri, 06 Apr 2018 13:35:00 +0000 Content-Type: text/plain; charset="UTF-8" Content-Transfer-Encoding: quoted-printable X-Received-Bytes: 5640 X-Received-Body-CRC: 3113672170 Xref: reader02.eternal-september.org comp.lang.ada:51353 Date: 2018-04-06T06:35:00-07:00 List-Id: On Friday, April 6, 2018 at 12:12:04 AM UTC+2, Randy Brukardt wrote: > "Bojan Bozovic" wrote in message=20 > news:17b6d5b9-5909-4f0c-ab25-9b3cf4fd0450@googlegroups.com... > ... > > Ah I was victim of April the 1st joke! I wasn't joking though. My > > proposal was to add assertions in general to Ada, as something in > > the core language, like exceptions are, or tasks, which would > > function just as "ghost code" you had in mind when > > > > pragma assertion_policy (check); > > > > is used. Maybe not use assertion keyword but use functions with > > ghost? I really can't say which approach wold work best, from the > > point of function, readability and conciseness. That is for ARG to > > decide. >=20 > But what would the point be? A pragma is a first-class part of the langua= ge=20 > (it's not optional!). And a pragma can be used in places that a statement= =20 > cannot be used (that is, with declarations). To get even equivalent=20 > functionality that way would be fairly complex (needing both statements a= nd=20 > declarations). Sounds like a lot of work for very little gain. >=20 > Personally, I don't see a lot of value in pragma Assert in the first plac= e=20 > (as opposed to the other contract assertions). I'm in the camp that=20 > suppressing/ignoring checks ought to be a last resort, only to be used wh= en=20 > performance goals can't be met any other way (using a better algorithm is= =20 > always a better way). As such, "cheap" assertions might as well just be p= art=20 > of the code; I would never want to remove them. Often, the compiler can= =20 > prove that they're true (so there is no cost), and if not, a well-defined= =20 > failure is better than erroneous execution where anything can happen. >=20 > For instance, the Janus/Ada compiler has a lot of code like: > if Node.Solution =3D null then > Internal_Error ("Missing solution"); >=20 > This could have been modeled as an assertion: >=20 > pragma Assert (Node.Solution /=3D null, "Missing solution"); >=20 > but the above modeling allows calling a fairly complex error management= =20 > routine (which, if trace mode is on, gives the user various interactive= =20 > debugging options). And we wouldn't want to remove the check in any case;= =20 > it's much better to detect the problem in a controlled way rather than an= =20 > uncontrolled one (especially if all checking has been suppressed). >=20 > Some assertions are expensive to run, and thus shouldn't run all of the= =20 > time. For those, I generally find that it is best to tie them to the=20 > debugging mode for whatever subsystem that they are related to. (Pretty m= uch=20 > every program I write has a variety of debugging modes, so that one has a= =20 > limited amount of debugging information to look through to find problems.= I=20 > usually write my programs with a substantial amount of debugging from the= =20 > start, and then usually keep any debugging added to find specific problem= s.=20 > Whenever I haven't had substantial debugging, I've always found I've had = to=20 > add it, in order to get any confidence that the code is doing the right= =20 > thing.) Since there are multiple such debugging modes, tying everything t= o a=20 > single "check/ignore" flag is much too coarse for my purposes. So again= =20 > there isn't much use for pragma Assert. >=20 > Randy. If assertions/invariants encompassed type invariants and were used in loops= as well, like in Eiffel, readability would be better in my humble opinion,= while Ada have pragma assert that can be used in loops, and static_predica= te and dynamic_predicate on types. Maybe assertion blocks would work better as in Eiffel for loops? Like excep= tion block in Ada? Eiffel approach must have been discussed by ARG, however readability is sti= ll important for human programmer, even though it isn't important for the c= ompiler.