Path: utzoo!utgpu!news-server.csri.toronto.edu!cs.utexas.edu!asuvax!ncar!elroy.jpl.nasa.gov!swrinde!zaphod.mps.ohio-state.edu!uakari.primate.wisc.edu!crdgw1!uunet!mcsun!ukc!pyrltd!tetrauk!rick
From: rick@tetrauk.UUCP (Rick Jones)
Newsgroups: comp.object
Subject: Re: A Hard Problem for Static Type Systems
Message-ID: <1158@tetrauk.UUCP>
Date: 3 May 91 14:18:34 GMT
References: <1991Apr20.010347.28984@leland.Stanford.EDU> <554@eiffel.UUCP> <1991Apr26.203642.17387@leland.Stanford.EDU> <556@eiffel.UUCP> <1146@tetrauk.UUCP> <2479@m1.cs.man.ac.uk>
Reply-To: rick@tetrauk.UUCP (Rick Jones)
Organization: Tetra Ltd., Maidenhead, UK
Lines: 81

In article <2479@m1.cs.man.ac.uk> mario@cs.man.ac.uk (Mario Wolczko) writes:
>In article <1146@tetrauk.UUCP>, rick@tetrauk.UUCP (Rick Jones) writes:
>> [ ... ]  However, var's implicit type is also a supertype of A.
>> Provided no object is ever attached to var which is a supertype of var's
>> IMPLICIT type, then the system is type-safe.  
>
>> This analysis is statically feasible, and is what GTA sets out to do.
>  ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
>
>Nonsense.  It is easy to construct a program which is type-safe by
>your definition but cannot be verified as type-correct by static
>analysis.  If you could verify all such programs, you would have
>solved the Halting Problem.

This is true, and static analysis will always be pessimistic.  What GTA does do
is to establish whether there are any assigments of objects in the whole
program, which could (directly or indirectly) result in an object which does
not support some feature being attached to a variable which calls the feature.
This ignores run-time branches, so there is an implicit assumption that every
possible branch combination may at some time be executed.  Thus your example:

>	var X;
>	if predicate1
>	then X := L1;  /* L1 is an object that has feature F */
>	else X := L2;  /* L2 is an object that does not have feature F */
>	fi
>	X.F;

will be rejected.  However, for normal, well-designed programs, this is not a
problem.  A program such as this example is inherently unreliable, even though
thorough testing and use may never have produced the conditions required for
failure.  A safer version would be:

>	var X;
>	if predicate1
>	then X := L1;  /* L1 is an object that has feature F */
>	else X := L2;  /* L2 is an object that does not have feature F */
>	fi
>	if predicate1
>	then X.F;
>	fi

but this is not good object oriented design.  The program is making branch
decisions based (indirectly) on the object's actual type.  Good OO design uses
abstraction and polymorphism to produce code which is independent of the
object's actual type.  A checkably safe version is:

>	var X, Y;
>	if predicate1
>	then Y := L1;  /* L1 is an object that has feature F */
>	     Y.F;
>	     X := Y;
>	else X := L2;  /* L2 is an object that does not have feature F */
>	fi

Feature F has been safely applied to object L1 via Y, subsequently feature F
may not be applied via X, since X may or may not refer to object L1.  Although
this appears to make a simple program more complex, the example is artificial.
It is more likely that the equivalent assignments are across different modules,
where there would have to be separate declarations of X and Y anyway.  If the
situation of the first example existed, but distributed across different source
modules, the unreliability would go unnoticed.  If the second existed in the
same way, it would be very clumsy code.  GTA would pick up both these,
suggesting a more robust or cleaner design should be used.

I maintain that a well designed program which avoids branch decisions based on
type will check correctly under the rules of GTA.  I do not believe even the
pessimistic checking of GTA is possible in a dynamically typed language - it
requires explicit type declarations, and a conventional (e.g. inheritance
based) mechanism for defining basic type conformance as a starting point.  I
cannot produce a rigorous justification of this viewpoint, though.

The theory of this type-checking system was discussed quite thoroughly by
Bertrand Meyer in the article he posted last year.  If you don't have it and
would like a copy (it's about 1500 lines), I can email it to you.

-- 
Rick Jones, Tetra Ltd.  Maidenhead, Berks, UK
rick@tetrauk.uucp

Any fool can provide a solution - the problem is to understand the problem