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

Relatore
Anindya Banerjee

Data e ora
martedì 2 novembre 2010 alle ore 16.45

Referente
Maria Paola Bonacina

Referente esterno

Data pubblicazione
26 ottobre 2010

Dipartimento
Informatica  

Riassunto

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. We will use 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 the Boogie verification condition generator which in turn
serves as a front end to the Z3 SMT solver.

ornamento
Inizio pagina