Sciweavers

Share
VSTTE
2010
Springer

Local Reasoning and Dynamic Framing for the Composite Pattern and Its Clients

10 years 10 months ago
Local Reasoning and Dynamic Framing for the Composite Pattern and Its Clients
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.
Stan Rosenberg, Anindya Banerjee, David A. Naumann
Added 31 Jan 2011
Updated 31 Jan 2011
Type Journal
Year 2010
Where VSTTE
Authors Stan Rosenberg, Anindya Banerjee, David A. Naumann
Comments (0)
books