RAII-like unfolding of predicates

[pieter-bos]

It would be nice if you could use unfolding as a statement, which is folded when a scope is exited. In this example, we need to unfold state, and refold it on method exit:

    private Object search(Node x, int key, int ht) {
        //@ unfolding x.state();
        Entry[] children = x.children;

        // leaf
        if (ht == 0) {
            for (int j = 0; j < x.m; j++) {
                if (key == children[j].key) return children[j].val /* <== */;
            }
        }

        // internal node
        else {
            for (int j = 0; j < x.m; j++) {
                if (j+1 == x.m || key < children[j+1].key)
                    return search(children[j].childNode, key, ht-1) /* <== */;
            }
        }
        return null; /* <== */
    }

This requires specifying at each arrow that we refold the predicate. It would be nice if this is automatic. It could rely on the try/finally encoding we already have.

[pieter-bos]

If we expand our notion of pure methods, this would also make precise what should happen when an unfold or fold occurs in a method. (That is: fold and unfold are out, but unfolding seems to be fine)