From mboxrd@z Thu Jan 1 00:00:00 1970 X-Spam-Checker-Version: SpamAssassin 3.4.4 (2020-01-24) on polar.synack.me X-Spam-Level: X-Spam-Status: No, score=-1.3 required=5.0 tests=BAYES_00,INVALID_MSGID autolearn=no autolearn_force=no version=3.4.4 X-Google-Language: ENGLISH,ASCII-7-bit X-Google-Thread: 103376,3f280e3f1e97f305 X-Google-Attributes: gid103376,public From: fjh@murlibobo.cs.mu.OZ.AU (Fergus Henderson) Subject: Re: Finding out parameters which are not written Date: 1997/08/17 Message-ID: <5t734c$91p@mulga.cs.mu.OZ.AU>#1/1 X-Deja-AN: 265404147 References: <33F02867.322D@aut.alcatel.at> <1997Aug12.070728.1@eisner> Organization: Comp Sci, University of Melbourne Newsgroups: comp.lang.ada Date: 1997-08-17T00:00:00+00:00 List-Id: kilgallen@eisner.decus.org (Larry Kilgallen) writes: >Gerhard Radatz writes: >> Does anyone know about a tool which can detect such situations as the >> following: >> >> procedure xxx (result: out INTEGER) is >> begin >> if <> then >> result := 0; >> end if; >> end; >> >> Obviously, this proc is erroneous and result will not be written if >> <> 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 <> 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 <> will always succeed, it would report an error. The programmer will then rewrite the code as if <> 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 | "I have always known that the pursuit WWW: | of excellence is a lethal habit" PGP: finger fjh@128.250.37.3 | -- the last words of T. S. Garp.