Re: Operation can be dispatching in only one type

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

Dmitry A. Kazakov schrieb:
> On Tue, 01 Dec 2009 16:02:21 +0100, Georg Bauhaus wrote:
> 
>> Dmitry A. Kazakov schrieb:
>>> On Tue, 01 Dec 2009 13:13:29 +0100, Georg Bauhaus wrote:
>>>
>>>> Then we could rely on the language: compilers will detect
>>>> uninitialized variables provided these do not have a pragma/keyword/...
>>>> to say that uninitialized is what the programmer wants.
>>>> Some fancy means to tell the compiler that this variable
>>>> does indeed have a good first value like pragma Import.
>>>>
>>>>    X : [constant] Car; -- default init,
>>> The error is here!
>>>>                        -- undefined,
>>>>                        -- junk bits. Doesn't matter
>>>>    --  *no* pragma Import (Ada, X);
>>>>
>>>> begin
>>>>
>>>>    Spare := X.Tire (5); -- would become illegal,
>>> Not here!
>> Why?
> 
> Because X is illegal right after begin:
> 
> IF accessing X is illegal THEN the corresponding operation does not belong
> to the type of X THEN the type of X is not Car. q.e.d.

But the implications of this proof are purely formal,
and not relevant before X is used.
There is no way to perform an operation involving X in
its own declaration.

The difference in views would be that your laws say Don't
create objects that could be used illegally if there
were uses that can't be there, though, but for formal reasons.
Whereas Java's ruling says (at compile time) Your program
cannot be accepted because this object cannot be in
a legal state here. The variable may not have been assigned
a value.


> (Provided, we are talking about a typed language)

I think there is more in what you say than what is covered
by the words "typed language"?

>>> -------------------------
>>> Anyway, you cannot do that because:
>>>
>>>    if HALT (P) then
>>>      X := Z;
>>>    end if;
>>>    Y := X;  -- Is this legal?
>> (HALT is a run-time issue that has no impact here.)
> 
> If you cannot decide if X is "initialized",

But I can decide whether (and when!) X is "initialized"!
The compiler does not need to run HALT in order
to see that X may not have been initialized when the condition
is not true.  The program is not accepted because it may lack
an assignment to X before Y := X for much simpler reasons.

In fact, SPARK marks it as error.  I made a simple example,
a procedure that does or does not assign depending
on an unknown Boolean Condition parameter:


   1  package body Asgn is
   2
   3     procedure Exmpl (Condition: Boolean; Result : out Integer) is
   4        X : Integer;
   5     begin
   6        if Condition then
   7           X := 42;
   8        end if;
   9
  10        Result := X / 2;
                      ^1
??? (  1)  Flow Error        :501: Expression contains reference(s) to
variable X,
           which may have an undefined value.

  11     end Exmpl;

??? (  2)  Flow Error        :602: The undefined initial value of X may be
used in
           the derivation of Result.

  12
  13  end Asgn;

What the new rule would do is merge the two messages into one
message about X that may not have a value yet: An "undefined
initial value" MUST not be used like it is used on line 10.
The (different) Ada language rule will forbid.


>> While this snippet would not be legal as is (on purpose!),
>> Ada's case coverage rules can make the programmer write a
>> legal program easily: write an else branch!
> 
> And this one:
> 
> procedure Foo (X : in out Car);
>    ...
> begin
>    Foo (X);
>    Y := X; -- Is this legal?

Yes, this is legal, because Foo is called with X having been
assigned a value.  It cannot be otherwise, the recursion has to
start somewhere.  It can only start with an actual parameter
that has a value (again, the compiler can check this).


> And if Foo were declared as
> 
> procedure Foo (X : out Car);


We'd have roughly the same as this:

    X : Car;
begin
    X := Foo_as_function;  -- now X can be used

I see no operational problem.  Is there one?


>>>> Does the phrase "first value" make sense?
>>> An object shall not have invalid values. All values are valid if the
>>> language is typed. Enforcing user-defined construction including
>>> prohibition of certain kinds of construction (e.g. per default constructor)
>>> is a different story. 
>> If you feed this to a Java compiler you will see how it is done.
>> The Java compiler will not accept a reference to a variable's
>> component when the variable may not have been initialized.
> 
> I consider this model wrong. It is better not to introduce inappropriate
> values rather than trying to catch them later.

The Java rule works at compile time. No value is introduced at any
time during compilation.  Nothing to catch.  A reference to a
variable in source text is permitted if and only if the compiler can show,
by following simple compile time rules, that a value has been assigned
to the variable or constant prior to referencing.  It need not evaluate
calls (i.e. run the program) to arrive at a decision.

> Java does not have
> constrained types, so I can understand why they go this way.

Ehm, I don't see the connection here.  Which one is it?

When I declare

   X : Some_Type(Some_Constraint);
begin
   -- X may need further "initilization", and assigments, since
   -- Some_Type is an "open minded" type of a varying nature,
   -- not a fixed value. Its objects accumulate values.

> I also think that forward uninitialized declarations represent bad
> style, e.g.:
> 
> function Foo (...) return Bar is
>    Result : Bar;
> begin
>    ...
>    if ... then
>       raise Baz;
>    end if;
>    ...
>    Result := ...;
>    ...
>    return Result;
> end Foo;
> 
> I understand the motivation to declare Result uninitialized (because we
> could leave Foo via an exception), but I don't like this.
> 

But assigning the first value when declaring X won't help
when the initialization can raise exceptions.  How could this change?

When the body of Foo gradually operates on Result to produce
its final state (in a safe way because no reference can be
made to Result or its parts without prior assignments), why
should I pretend that any valid initial value for Result,
provided by an initialization expression, is
better than its default value?  (Assuming that I cannot
refer to "invalid" components of objects because the compiler
will simply reject a program that might try.)