Abstract
We use access permissions and typestate to specify and ver- ify a Java library that implements snapshotable search trees, as well as some client code. We formalize our approach in the Plural tool, a sound modular typestate checking tool. We describe the challenges to verify- ing snapshotable trees in Plural, give an abstract interface specification against which we verify the client code, provide a concrete specification for an implementation and describe proof patterns we found. We also relate this verification approach to other techniques used to verify this data structure.
Original language | English |
---|---|
Book series | Lecture Notes in Computer Science |
Volume | 7304 |
Pages (from-to) | 187-201 |
Number of pages | 15 |
ISSN | 0302-9743 |
DOIs | |
Publication status | Published - 2012 |