Type systems offer a lightweight way to specify and check information flow, but can reject secure programs owing to conservative approximations. Moreover, many policies involve declassification (and its dual) under conditions that may involve access permissions, event histories, cryptographic operations, etc. It has proved difficult to find expressive type systems to encompass a range of policies and to find convincing semantics. We describe an alternative based on a relational notion of pre-post specification, focusing especially on challenges posed by the heap. We discuss a 'self-composition' encoding of relational specifications as ordinary ones which can be checked modularly using off-the-shelf program verifers. Experiments using tools like Blast and ESC/Java2 show the need for certain transformations which can themselves be formalized in relational Hoare logic but automated by type checking.