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.3 required=5.0 tests=BAYES_00,INVALID_MSGID autolearn=no autolearn_force=no version=3.4.4 X-Google-Language: ENGLISH,ASCII-7-bit X-Google-Thread: f891f,9d58048b8113c00f X-Google-Attributes: gidf891f,public X-Google-Thread: 103376,2e71cf22768a124d X-Google-Attributes: gid103376,public X-Google-Thread: 101deb,b20bb06b63f6e65 X-Google-Attributes: gid101deb,public X-Google-Thread: 10cc59,9d58048b8113c00f X-Google-Attributes: gid10cc59,public X-Google-Thread: 1014db,9d58048b8113c00f X-Google-Attributes: gid1014db,public From: dewar@cs.nyu.edu (Robert Dewar) Subject: Re: next "big" language?? (disagree) Date: 1996/06/24 Message-ID: #1/1 X-Deja-AN: 162470182 references: <4ql1fv$5ss@goanna.cs.rmit.EDU.AU> organization: Courant Institute of Mathematical Sciences newsgroups: comp.lang.pascal,comp.lang.c,comp.lang.misc,comp.lang.pl1,comp.lang.ada Date: 1996-06-24T00:00:00+00:00 List-Id: Dale said "Obviously if there are two concepts, then we should have two names. For example (in Ada) we could stick with pragma Assert(x); for the traditional "please check this really is the case" assertion and introduce pragma Fact(x); (or some other name) for the "this really is true, trust me, and make appropriate optimisations" type assertion. Can anyone think of a better name (pragma Declare(x) is not available in Ada) than "Fact"?" Sure this is one approach, but WG9 felt it was over-complex to introduce multiple concepts here, especially when it is essentially impossible to come up with non-confusing names (since assert is the obvious name for all cases). Note too that the pragma Assert in GNAT, which is equivalent to an if statement with a raise, is still not what some people want, since of course the optimizer can and does derive some information from the presence of the Assert. What some people want is an Assert that is guaranteed to be semantically non-intrusive -- a rather slippery concept. Anyway, in practice I think that the assert of GNAT is as far as it is reasonable to go. At least the advantage of the GNAT definition is that its semantics is trivially simple (since it is defined by the equivalent if/raise sequence). There just does not seem to be enough consensus to go further, unless you really go to full annotation, in for example the SPARK style using the Praxis tools. For this pragma Annotate, as recently recommended by the HRG to WG9, and as currently implemented in GNAT, can be used.