On Wednesday, 16 September 2015 at 18:41:33 UTC, Ola Fosheim
Grøstad wrote:
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.
For example:
Object<ready> obj = create();
for ... {
(Object<lend#> obj, Ref<Object,lend#> r) = obj.borrow();
queue.push(r);
dostuff(queue);
}
On the other hand if you have this:
for i=0..2 {
(Object<lend#> obj, Ref<Object,lend#> r[i]) = obj.borrow();
dostuff(r);
}
then you can unwind it as (hopefully):
(Object<lend1234> obj, Ref<Object,lend1234> r[0]) =
obj.borrow();
(Object<lend4324> obj, Ref<Object,lend4324> r[1]) =
obj.borrow();
(Object<lend5133> obj, Ref<Object,lend5133> r[2]) =
obj.borrow();
x += somepurefunction(r[0]);
x += somepurefunction(r[1]);
x += somepurefunction(r[2]);
r[0].~this(); // r[0] proven unmodified, type is
Ref<Object,lend1234>
r[1].~this(); // r[1] proven to be Ref<Object,lend4324>
r[2].~this(); // r[2] proven to be Ref<Object,lend5133>
r.~this();
If the lend IDs always are unique then you sometimes can prove
that all constructors have a matching destructor... Or something
like that...
?
