Re: Operation can be dispatching in only one type

["Dmitry A. Kazakov" <mailbox@dmitry-kazakov.de>]

On Wed, 02 Dec 2009 07:35:39 -0500, John B. Matthews wrote:

> In article <1jcbtmi5rztyp$.norvlhez9i9$.dlg@40tude.net>,
>  "Dmitry A. Kazakov" <mailbox@dmitry-kazakov.de> wrote:
> 
> Georg Bauhaus wrote:
> 
>>>  From the Java point of view, there are no false positives
>>> or negatives.
>> 
>> Of course there are, because it is a halting problem. So you need 
>> some optimistic or pessimistic estimation of:
>> 
>> if False then
>>    Print (X.Tire); -- Is this illegal? If yes, that is a false positive
>> end if;
> 
> It would be indeterminate but for doing "a specific conservative flow 
> analysis." In the specific cases of boolean constant expressions and if 
> statements,
> 
>   if (true) { spare = new Tire(); } // spare assigned
>   if (1 == 1) { spare = new Tire(); } // spare assigned
>   if (false) { spare = new Tire(); } // spare unassigned
>   if (1 == 2) { spare = new Tire(); } // spare unassigned
>   if (always()) { spare = new Tire(); } // spare unassigned
> 
>   static boolean always() { return true; }
> 
> In particular, spare remains unassigned even though the function 
> always() is always true.
> 
> In Ada, a certain compiler may warn 'variable "N" is assigned but never 
> read' for the following:
> 
> N : Integer;
> if False then N := 1; end if;
> 
> I'm not especially advocating applying the Java rules to Ada, but I like 
> the warning.

Yes, warning is nice.

The problem is with making it an error as Georg suggests (and Java does).
An error (and its complement "no error") require much more careful
definition. "Initialized" is too shaky for that, but for all I find
"unassigned" inconsistent with strong typing. A typed object is always
assigned because it cannot have any values other than of its type. If we
wanted an object to have *certain* values, e.g. "any value different from
the default one", then a naive analysis a-la Java is too little to me. I
would prefer full blown pre-, postconditions and invariants for such a
case.

-- 
Regards,
Dmitry A. Kazakov
http://www.dmitry-kazakov.de