Flow Typing Specification Elements

[DavePearce]

This doesn't type check, but looks technically legit (Reference_Valid_39):

type List is &{int data, null|List next }

method fill(List l, int v)
ensures l->data == v
ensures (l->next is List) ==> *(l->next) == old(*(l->next)):
    l->data = v

The problem is that it won't retype l, even though it makes sense to do so in this context.

[DavePearce]

I did manage to workaround this with a property:

property unchanged2({int data, null|List next} node)
// My data is unchanged
where node.data == old(node.data)
// Everything else is also unchanged
where unchanged(node.next)