Re: Interesting article on ARG work

[Bojan Bozovic <bozovic.bojan@gmail.com>]

On Thursday, April 5, 2018 at 12:30:46 AM UTC+2, Randy Brukardt wrote:
> "Dan'l Miller" <optikos@verizon.net> wrote in message 
> news:9879872e-c18a-4667-afe5-41ce0f54559f@googlegroups.com...
> >On Tuesday, April 3, 2018 at 5:33:47 PM UTC-5, Randy Brukardt wrote:
> >> I'm not sure what your idea is. The pragma Assert exists already, what is 
> >> it
> >> that you can't do with it that you need?
> ...
> >> "Bojan Bozovic" wrote in message
> >> > Pragma assert(condition,message);
> >> > Construct
> >> > Assertion name is condition with message;
> >
> >Randy, despite your humor in the original posting, I think that he is 
> >(seriously) proposing ...
> 
> I presumed he was serious, I just didn't understand what he was proposing...
> 
> >...that assertions optionally be named so that the named condition and
> >message pair is defined in one place and then utilized at the (numerous)
> >places where the assertion appears, so that the condition & message do
> >not vary due to the drift of time, forgetfulness, and whim of different
> >programmers.  ...
> 
> Humm, I suppose that could have been it. Or it could be that that is 
> something you want...
> 
> There is a much more general proposal for Ada 2020 called "ghost code" - a 
> silly name for code and declarations intended only to be used by assertions. 
> (The idea being that if it is marked and enforced as such, it can be removed 
> when the Assertion_Policy is Ignore.)
> 
> Using that (which may or may not make it into Ada 2020 -- we haven't yet 
> discussed it at a meeting), one could use a ghost function for this purpose:
> 
>       function My_Assertion (...) return Boolean is
>           (if Condition then raise Assertion_Error with Message else True)
>           with Ghost;
> 
>      pragma Assert (My_Assertion (...));
> 
> (Note: The "..." here is any objects that Condition needs to be evaluated.)
> 
> This works now (without the "ghost") and is more general in that one can 
> pass parameters if needed which would be a problem with the syntax proposed.
> 
> >... there is no MetaAda that declares all language principles (preferably
> > in code that compiler vendors would take as input when writing a
> >compiler, instead of taking in English prose).  "Everything shall be
> >able to be named; that name shall be utilizable to assure uniformity at
> >each point of usage to the named declaration." would be one of those
> >statements in MetaAda, most likely stated in something resembling a
> >language isomorphic to symbolic logic instead of quick-&-dirty English
> >prose here.
> 
> I suspect it would be a huge job to get consensus on such MetaAda rules. 
> While I tend to agree with your rule, it's clear that the Ada 95 designers 
> did not. In particular, anonymous access types have various capabilities not 
> available to their named counterparts (going back to Ada 95 anonymous access 
> parameters). This has gotten worse with each new version. I've spent some 
> time complaining about that, but there is only so much that any one person 
> can do.
> 
>                          Randy.

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.