We use cookies to ensure that we give you the best experience on our website. By continuing to browse this repository, you give consent for essential cookies to be used. You can read more about our Privacy and Cookie Policy.

Durham Research Online
You are in:

Enhancing modular OO verification with separation logic.

Chin, W.-N. and David, C. and Nguyen, H. H. and Qin, S. (2008) 'Enhancing modular OO verification with separation logic.', ACM SIGPLAN notices., 43 (1). pp. 87-99.


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 specifications of overridden methods in superclasses, leading to imprecision during program reasoning. To address this, we advocate a fresh approach to OO verification that focuses on the distinction and relation between specifications that cater to calls with static dispatching from those for calls with dynamic dispatching. We formulate a novel specification subsumption that can avoid code re-verification, where possible. Using a predicate mechanism, we propose a flexible scheme for supporting class invariant and lossless casting. Our aim is to lay the foundation for a practical verification system that is precise, concise and modular for sequential OO programs. We exploit the separation logic formalism to achieve this.

Item Type:Article
Keywords:Automated verification, Enhanced subsumption, Separation.
Full text:Full text not available from this repository.
Publisher Web site:
Record Created:16 Nov 2009 17:05
Last Modified:30 Jul 2010 12:21

Social bookmarking: del.icio.usConnoteaBibSonomyCiteULikeFacebookTwitterExport: EndNote, Zotero | BibTex
Look up in GoogleScholar | Find in a UK Library