Re: Finding out parameters which are not written

[fjh@murlibobo.cs.mu.OZ.AU (Fergus Henderson)]

kilgallen@eisner.decus.org (Larry Kilgallen) writes:

>Gerhard Radatz <gerhard.radatz@aut.alcatel.at> writes:
>> Does anyone know about a tool which can detect such situations as the
>> following:
>> 
>> 	procedure xxx (result: out INTEGER) is
>>         begin
>> 	     if <<condition>> then
>> 	         result := 0;
>>              end if;
>>         end;
>> 
>> Obviously, this proc is erroneous and result will not be written if
>> <<condition>> is FALSE.
>> However, my Ada-Compiler (DEC-ADA for VMS) does not detect this problem,
>> because result is written "at least once" in the body of xxx.
>> 
>> Is there any tool which can provide help ???
>
>Such a tool could not [...]

I would just like to point out that such a tool _can_ work, and is
indeed very useful for detecting errors.  I know this because I wrote
just such a tool -- we call it a mode checker -- as part of the Mercury
compiler.  Mode checking is in fact an integral feature of the Mercury
language.  I and the rest of the Mercury group have used it for
developing well over 100 thousand lines of Mercury code.  Mode checking
works very well in our experience.

>Such a tool could not handle the case where <<condition>> depended on
>some input determined outside the scope of the current compilation.  A
>static analysis that only works for the simple cases would seem to be
>unattractive since those are precisely the cases where humans can best
>spot the error.

The idea is that the tool and the programmers cooperate to achieve the
desired effect.  Static analysis alone is either limited or limiting,
but static analysis in combination with some runtime checking works
extremely well.

The tool should only allow programs which it can prove will have no mode
errors.   So for the code above, since it cannot prove that <<condition>>
will always succeed, it would report an error.

The programmer will then rewrite the code as

 	     if <<condition>> then
 	         result := 0;
	     else
		 raise Some_Appropriate_Exception;
             end if;

which _will_ be accepted by the tool.

>Consider a long series of conditional tests each depending on different
>arcane input.  If no condition results in setting the output, it would
>seem that cannot be determined at compile time.  Run time detection is
>a different matter, of course.

Such cases where the program depends on complex assertions (such as the
assertion that at least one of "a long series of conditional tests each
depending on different arcane input" will succeed) are exactly the
sorts of cases which programmers often get wrong, or which easily get
broken during maintentance.  Hence it is extremely useful to include
runtime error detection for these cases.  During the development of the
Mercury compiler, it has often been the case that sanity checks of this
nature which we added only to satisfy the mode checker have later
failed for some obscure test case.  Adding the sanity checks ensures
that the bug is caught (rather than the program just producing bogus
results) and makes it much easier to debug.

So, to summarize:
	1.  Mode checking does work well in practice.
	2.  Mode checking has two benefits for program reliability:
	    - the immediate benefit is the static detection of a significant
	      class of errors;
	    - the other benefit is that it strongly encourages
	      programmers to include code to perform runtime checking
	      of complex (and hence error-prone) assertions that cannot
	      be verified by static analysis.

--
Fergus Henderson <fjh@cs.mu.oz.au>   |  "I have always known that the pursuit
WWW: <http://www.cs.mu.oz.au/~fjh>   |  of excellence is a lethal habit"
PGP: finger fjh@128.250.37.3         |     -- the last words of T. S. Garp.