TY - GEN
T1 - Local reasoning and dynamic framing for the composite pattern and Its clients
AU - Rosenberg, Stan
AU - Banerjee, Anindya
AU - Naumann, David A.
PY - 2010
Y1 - 2010
N2 - 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.
AB - 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.
UR - http://www.scopus.com/inward/record.url?scp=77957080947&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=77957080947&partnerID=8YFLogxK
U2 - 10.1007/978-3-642-15057-9_13
DO - 10.1007/978-3-642-15057-9_13
M3 - Conference contribution
AN - SCOPUS:77957080947
SN - 364215056X
SN - 9783642150562
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 183
EP - 198
BT - Verified Software
T2 - 3rd International Conference on Verified Software: Theories, Tools, Experiments, VSTTE 2010
Y2 - 16 August 2010 through 19 August 2010
ER -