Dedicated to the memory of Stephen L. Bloom (1940--2010). Shared mutable objects pose grave challenges in reasoning, especially for information hiding and modularity. This article presents a novel technique for reasoning about error-avoiding partial correctness of programs featuring shared mutable objects, and investigates the technique by formalizing a logic. 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 frame condition 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. Soundness is proved using a standard program semantics. The logic facilitates heap-local reasoning about object invariants, as shown here by examples. Part II of this article extends the logic with second-order framing which formalizes the hiding of data invariants.

This paper provides a way to specify expressive declassification policies, in particular, when, what, and where policies that include conditions under which downgrading is allowed. Secondly, an end-to-end semantic property is introduced, based on a model that allows observations of intermediate low states as well as termination. An attacker's knowledge only increases at explicit declassification steps, and within limits set by policy. Thirdly, static enforcement is provided by combining type-checking with program verification techniques applied to the small subprograms that carry out declassifications. Enforcement is proved sound for a simple programming language and the extension to object-oriented programs is described.