On Wednesday, 16 September 2015 at 18:01:29 UTC, Marc Schütz
wrote:
typestate(alias owner) {
this.owner := owner; // re-alias operator
this.owner.refcount++;
}
I don't think this is possible to establish in the general case.
Wouldn't this require a full theorem prover? I think the only way
for that to work is to fully unroll all loops and hope that a
theorem prover can deal with it. Either that or painstakingly
construct a proof manually (Hoare logic).
Like, how can you statically determine if borrowed references
stuffed into a queue are all released? To do that you must prove
when the queue is empty for borrowed references from a specific
object, but it could be interleaved with references to other
objects.
