Local reasoning and dynamic framing for the composite pattern and Its clients

Stan Rosenberg, Anindya Banerjee, David A. Naumann

Research output: Chapter in Book/Report/Conference proceedingConference contributionpeer-review

7 Scopus citations

Abstract

The Composite design pattern is an exemplar of specification and verification challenges for sequential object-oriented programs. Region logic is a Hoare logic augmented with state dependent "modifies" specifications based on simple notations for object sets. Using ordinary first order logic assertions, it supports local reasoning and also the hiding of invariants on encapsulated state, in ways similar to separation logic but suited to off-the-shelf SMT solvers. This paper uses region logic to specify and verify a representative implementation of the Composite design pattern. To evaluate efficacy of the specification, it is used in verifications of several sample client programs including one with hiding. Verification is performed using a verifier for region logic built on top of an existing verification condition generator which serves as a front end to an SMT solver.

Original languageEnglish
Title of host publicationVerified Software
Subtitle of host publicationTheories, Tools, Experiments - Third International Conference, VSTTE 2010, Proceedings
Pages183-198
Number of pages16
DOIs
StatePublished - 2010
Event3rd International Conference on Verified Software: Theories, Tools, Experiments, VSTTE 2010 - Edinburgh, United Kingdom
Duration: 16 Aug 201019 Aug 2010

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume6217 LNCS
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Conference

Conference3rd International Conference on Verified Software: Theories, Tools, Experiments, VSTTE 2010
Country/TerritoryUnited Kingdom
CityEdinburgh
Period16/08/1019/08/10

Fingerprint

Dive into the research topics of 'Local reasoning and dynamic framing for the composite pattern and Its clients'. Together they form a unique fingerprint.

Cite this