Flow Logic for Imperative Objects