Re: More extensive (variable) style checking

On 3/08/2013, at 6:55 AM, Alan Baljeu wrote:

>>     t :-
>>       (   hello(X)
>>       ;   world
>>       ),
>>       writeln(X).

[world might throw an exception, so the use of X in the last line
 might not be reachable.]

I'm with Alan Baljeu on this one.  Before throw, I used to use 'abort'
this way, although in the form
	( hello(X) -> true ; world ),
	write(X), nl.

(I find the Pascal-inspired 'writeln' horribly confusing,
because it combines 'write' with 'nl', not with the nonexistent 'ln'.)

Ulrich Neumerkel has recently suggested that portable
programs wanting to throw a standard error(Error_Term, Imp_Def)
ball but unable, because Imp_Def is implementation defined, to
provide any specific value for Imp_Def, should use _.  So one
might have

hurl(Error_Term) :-
    (  on_system_x -> system_x_imp_def(Imp_Def)
    ;  on_system_y -> system_y_imp_def(Imp_Def)
    ;  /* don't know what to do on other systems */
    ),
    throw(error(Error_Term, Imp_Def)).

might actually be reasonable code to write.


>> I find spurious information to be deleterious to development

Here I _almost_ part company with Alan.
I am willing to tolerate a small proportion of false positives
from a checking tool *IF* I get a high rate of true positives.

For example, FindBugs applied to Java code warns about stores
to dead variables.  However, the Java compiler itself generates
such stores.  The FindBugs team say they can do nothing about
this.  I don't understand why not, the variable names in such
cases are invariably reported as beginning with a dollar sign.
Why can't they just shut up about '$14' and the like?
But I put up with FindBugs as it stands because it finds a
huge number of genuine problems in other people's Java.  The
true positive rate is so high that about a 5% false positive
rate is tolerable.

It's an empirical question what the false positive rate for this
particular check would be.  Maybe it would be low enough that I'd
be happy.

What the example _does_ show is the weakness of a variable tracker
that has no idea of what predicates other than a handful of
built-in predicates actually do.

I'd quite like to be able to declare my intentions about predicates.
(But not to be forced to declare them.)
This predicate _must_ terminate by throwing,
that predicate _must_ terminate by throwing or failing,
this predicate may refer to at most these dynamic predicates,
that predicate may alter at most those dynamic predicates,
...

 -