A problem that frequently arises in writing functions is the need to constrain a local variable with an invariant. In particular, we often want to use a local variable to track some knowledge about volatile shared state. Today, the only way we can do this is to create a new claim every time we update the local variable. Moreover, using the claim only couples the volatile state to the value of the local at the point at which the claim was formed; using the claim in a later state requires the second (and often expensive) reasoning step of connecting the value of the local at that state to its current value.

A similar issue occurs when we want to squirrel away ownership of some local variables for a type into an object, to avoid the information about these variables from polluting the reasoning between the point at which the information is gathered and when it has to be used. Again, we would like to put this information into an object, wrap it up, and expose it only when necessary. But doing this for local variables means putting them into the heap, which is a huge concession. Moreover, the object type declaration has to be made outside of the function body, rather than where it is used.

One possible way around these difficulties is to extend the group concept to function bodies. The idea is to introduce a group object as a local variable, and to make as part of its declaration both the set of variables that are "in" the group when it is closed, and the invariants of the group. The groups would be lexically scoped. Multiple groups could mention the same variable; if two groups with overlapping scope list the same variable, wrapping either requires checking that the other is open. Within the scope of a group, updates to variables in the group undergo a check that the group is open or the variable is volatile and the group invariant is maintained.