Re: alternative to "trashed"


> This is intriging, but let me point out one potential problem.
> Usually, we state requirements that can be checked at the point of a call.
> It is not clear how to interpret last_use at the point of the call.

As you point out, discharging the proof obligation "last_use(x)" at the point
of call requires some different techniques.  One way to do it is to show that
x is not reachable from the live variables at the point of call.  (Andy
Hisgen proposed this approach in his thesis, CMU 1985, but didn't give a
formal semantics.)  Standard data flow analysis suffices to identify the live
variables identifiers, but deterimining reachability requires help from
data type specifications.

A point that I was trying to make in my earlier message is that
specifications of reachability are useful for other things, too.  I use them
to deduce a conservative estimate for the modifies clause of a procedure that
isn't specified.  Thus, the cost of giving semantics to "trashed" or
"last_use" can be amortized in other ways.


P.S. Perhaps we should continue this discussion offline?