Re: Operation can be dispatching in only one type

[Georg Bauhaus <rm.dash-bauhaus@futureapps.de>]

Randy Brukardt schrieb:
> "Dmitry A. Kazakov" <mailbox@dmitry-kazakov.de> wrote in message 
> news:1jcbtmi5rztyp$.norvlhez9i9$.dlg@40tude.net...
> ...
>> No the problem is whether to treat a call to the body as legal. The 
>> problem
>> is that you could not rely on its contract (out Car), in order to be able
>> to decide whether this call would "initialize" the object.
> [...]
> This is not at all a simple topic, and the sort of simple rule used 
> by Java does little other than give a false sense of security (and a lot of 
> annoying errors in code that has no problems).

After reading your recent hints to compatibility and single
pass compilation preventing flow analysis for legality decisions,
I noticed the possibility of a restrictions pragma, too.

Is it really annoying when programmers are forced to state,
explicitly, what they seem to be knowing?  That is, for example,
"I know that no ELSE is missing in the following code,
therefore I have omitted a no-op else branch"

    X : Some_Type;
begin
    if I_Know_What_This_Does (P) then
       X := Assign_It;
    end if;

    Use_It := Involve (X);

When I try to change a program, I find it annoying to
*not* see an ELSE branch that does then become a missing ELSE
branch.  The desired change turns a one-way flow into a blind alley...

The code typically looks like this:

    X : Some_Type;
begin
    if Has_Worked_For_Me (P) then
        X := Assign_it;
    end if;

    I_Can_Use_It := Involve (X);
        -- (formally fine in Ada, though not in Java or SPARK)

The incompleteness of information here can be avoided,
to some extent I think, and that's the reason I find
the Java rule to be helpful, or the Ada warning, or the
pragma which you have suggested.
Not really annoying.  I can no longer like seeing only half
of the cases of Boolean covered in an IF, explicitly.

To me, SPARK is not an annoyance when it refuses to accept
the above code, since flow analysis reveals the possibility
of missing initilization.  The Ada programmer may well have decided
the halting question for I_Know_What_This_Does or Has_Worked_For_Me.
However, I'd sure like to be hinted to his reasons and not just take
inspiration from a missing ELSE branch.

Could a compiler make some good use of code like the following
as a minimal way to express the programmer's valuable knowledge?
Or some less intrusive (annoying?) pragma or syntax or ...?

    X : Some_Type;
begin
    if Whatever (P) then
        X := Assign_it;
    else
        -- Stupid Ada configuration requires this.
        -- Yeah, X is valid because ...
        -- ... Whatever (P) is always true, you know.
        pragma Assert (Some_Type'Valid (X));
        null;
    end if;