gudeman@cs.arizona.edu (David Gudeman) (07/26/90)
Whenever you do compile-time analysis to either optimize programs or
to try to catch errors early, you run the risk (actually the
necessity) of changing the semantics of the program slightly. The
recent complaint on this group of how lazy evaluation changes an error
condition is an example. What I mean by "catch errors early" is to
do a static analysis that something that determines when a run-time
error is guaranteed to occur. Here is a semantics that I think would
solve these problems.
Define a subset of the semantic domain that includes all "error"
results. Call this the error set (it probably should be a domain,
but I'm not sure...). Let "<=" be the "less-defined-than" relation,
and define this relation over error elements in the following way:
(1) a sequence x ending with error is less defined than a sequence z
ending with error if x is a prefix of z and the error ending x is
less (or equal to) than the error ending z.
.EQ
x e1 <= x y e2 iff e1 <= e2
.EN
(2) an error message is less defined than the same message with more
information about the error occurrence.
.EQ
error(msg) < error(msg,file-name)
error(msg,file-name) < error(msg,file-name,line-number)
error(msg,file-name) < error(msg,file-name,offending-value)
.EN etc.
The language is defined such that all errors give the most amount of
information possible, and such that that errors occur as late as
possible. But program transformations can, by definition, change any
error result into another error result that is less defined than the
correct one. Bottom is _not_ an error result, so a program
transformation is not allowed to change a terminating program into a
non-terminating program.
Eg: static type checking in a dynamically typed language:
The normal error result for mis-using a type is
.EQ
<sequence of results before error>
error("type error", file-name, line-number, operation, offending-value)
.EN
but type inference and static type checking might change this into
.EQ
error("type error", file-name, line-number, operation)
.EN
that is, no initial sequence, and no knowledge of what value caused
the error.
--
David Gudeman
Department of Computer Science
The University of Arizona gudeman@cs.arizona.edu
Tucson, AZ 85721 noao!arizona!gudeman