Shared mutable objects pose challenges in reasoning, especially for data abstraction and modularity. We present a logic for error-avoiding partial correctness of programs featuring shared mutable objects. Using a first order assertion language, the logic provides heap-local reasoning about mutation and separation, via ghost fields and variables of type “region” (finite sets of object references). A new form of modifies clause specifies write, read, and allocation effects using region expressions; this supports a frame rule that allows a command to read state on which the framed predicate depends. We show the logic in use in proving the correctness of design patterns such as the composite pattern, the verification of which has been proposed as a challenge problem for specification and verification of sequential object-based programs. Joint work with: David A. Naumann and Stan Rosenberg