Efficient Runtime Assertion Checking of Assignable Clauses With Datagroups

Run-time assertion checking is useful for debugging programs and specifications. Existing tools check invariants as well as method pre- and post-conditions, but mostly ignore assignable (or modifies) clauses, which specify the heap locations a method is allowed to assign to. A way to abstract from implementation details is to specify assignable clauses using datagroups, which represent sets of concrete memory locations. Efficient Run-time checking of assignable clauses with datagroups is difficult because the members of a datagroup may change over time and because datagroups may get very large, especially for recursive data structures.