Computing Publications

Publications Home » Considerate Reasoning and the Com...

Considerate Reasoning and the Composite Design Pattern

Alexander Summers, Sophia Drossopoulou

Conference or Workshop Paper
VMCAI'2010
January, 2010
Springer-Verlag, LNCS
Abstract

We propose Considerate Reasoning, a novel specification and

verification technique based on object invariants. This technique supports

succinct specifications of implementations which follow the pattern of breaking properties of other objects and then notifying them appropriately.

It allows the specification to be concerned only with the properties directly relevant to the current method call, with no need to explicitly

mention the concerns of subcalls. In this way, the specification reflects

the division of responsibility present in the implementation, and reflects

what we regard as the natural argument behind the design.

We specify and prove the well-known Composite design pattern using Considerate Reasoning.We show how to encode our approach in Boogie2. The resulting specification verifies automatically within a few seconds; no manual guidance is required beyond the careful representation of the invariants themselves.

Keywords
Program Verification
SLURP
PDF of full publication (145 kilobytes)
(need help viewing PDF files?)
BibTEX file for the publication
N.B.
Conditions for downloading publications from this site.
 

pubs.doc.ic.ac.uk: built & maintained by Ashok Argent-Katwala.