Modular reasoning about invariants over shared state with interposed data members