Enhancing modular OO verification with separation logic

摘要: Conventional specifications for object-oriented (OO) programs must adhere to behavioral subtyping in support of class inheritance and method overriding. However, this requirement inherently weakens the overridden methods superclasses, leading imprecision during program reasoning. To address this, we advocate a fresh approach OO verification that focuses on distinction relation between cater calls with static dispatching from those dynamic dispatching. We formulate novel specification subsumption can avoid code re-verification, where possible. Using predicate mechanism, propose flexible scheme supporting invariant lossless casting. Our aim is lay foundation practical system precise, concise modular sequential programs. exploit separation logic formalism achieve this.