Re: Uninitialized "out" parameters

[ok@goanna.cs.rmit.edu.au (Richard A. O'Keefe)]

dewar@cs.nyu.edu (Robert Dewar) writes:
>Yes, but Ada is not dyunamically typed, it uses a decidable static type
>system, and there are VERY good reasons why comparable static systems
>cannot be designed for dealing with the uninitialized variable problem
>(please reread carefully my example of the 2 gig array in an allocate
>on demand environment -- and response to how your decidable system
>would accomodate this requirement).

In my experience of marking student C programs, trying to use uninitialised
variables is the commonest non-syntactic error.  I have found the program
'lclint' _extremely_ useful when marking because it does a very good job of
noticing possible uninitialised variables.  It even manages on occasion to
do a useful (not perfect) job with arrays.  On one student program it
reported 62 such warnings, and I thought it was crying wolf, but on closer
inspection every single warning (most of the involving arrays) was right.

I note that SPARCompiler Pascal, which I do not otherwise care for, has
a "-Rw" command line option for extending uninitialised variable tracking
into records (but not arrays).

Over the last year I have been coming to the conclusion that the ability to
use uninitialised variables is one of those programming language features
that I am better off without.  I mean, ever since "A Discipline of
Programming" I thought it was a good idea, but I also thought I was a hot
enough programmer not to need such a crutch.

Then I started using lclint, and it started finding mistakes that I hadn't
noticed.

True, Ada is so designed that sound and complete compile-time detection
of using uninitialised variables is impossible ('separate' probably
contributes something to this).  It's also worth noting that the change
to 'out' parameters in Ada 95 doesn't make it noticably harder for a
compiler that *tries* to do a *useful* amount of checking, as for example
gcc -O2 -Wall does.

But some day Ada will have a successor.  And I can see no reason why that
successor should not do a better job than Ada in this respect.

I mentioned lclint.  lclint does something rather interesting:  it tracks
the allocation state of pointers, via annotations.  In effect, it uses a
richer type language than C, in which it is possible to express things
like "this is a non-null pointer to an object having no other pointers";
just as Dijkstra's notation tracks "obligation to initialise" in the
type system, so lclint tracks "obligation to free" in the type system.

Fergus Henderson has posted in this thread.  He's involved in the
Mercury project, and Mercury, in addition to "types" uses something
called "modes" which in effect enrich the type system so that the
programmer can say
	"this procedure takes a record in which the x and y fields
	 are initialised and the z and w fields aren't, and
	 initialises the w field"
and the compiler can *prove* at compile time that no uninitialised
variable access is possible.

There has been other work done on including state and effects in type
systems, but lclint and Mercury are practical tools you can FTP today.

In the short term, the array problem can be handled the way Dijkstra's
notation does:  by having dynamic bounds, so that the initialised part
of an array is the part within the dynamic bounds, and the rest of the
array acts as if it didn't exist.  SPARCompiler Pascal has
	varying [n] of char
as its type for strings; this is the same idea as Dijkstra's arrays
except that the lower bound is frozen at 1.  Such a string may have
*room* for 100000 characters, but if it was last assigned a string of
5 characters, those 5 are the only ones you can access.

What does that mean for Ada?  It means that the use of abstract container
types like queues and APL/Fortran-90/Torrix-style "whole array" operations
are not just a clearer way to say what you mean, they are a good way to
avoid a class of errors.

-- 
Fifty years of programming language research, and we end up with C++ ???
Richard A. O'Keefe; http://www.cs.rmit.edu.au/~ok; RMIT Comp.Sci.