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?