Small specifications for tree update
File(s)Gardner2009Small.pdf (223.96 KB)
Accepted version
Author(s)
Gardner, PA
Wheelhouse, M
Type
Conference Paper
Abstract
O’Hearn, Reynolds and Yang introduced Separation Logic to provide modular reasoning about simple, mutable data structures in memory. They were able to construct small specifications of programs, by reasoning about the local parts of memory accessed by programs. Gardner, Calcagno and Zarfaty generalised this work, introducing Context Logic to reason about more complex data structures. In particular, they developed a formal, compositional specification of the Document Object Model, a W3C XML update library. Whilst keeping to the spirit of local reasoning, they were not able to retain small specifications. We introduce Segment Logic, which provides a more fine-grained analysis of the tree structure and yields small specifications. As well as being aesthetically pleasing, small specifications are important for reasoning about concurrent tree update.
Date Issued
2009-09-04
Date Acceptance
2009-09-04
Citation
Lecture Notes in Computer Science, 2009, 6194, pp.178-195
ISBN
978-3-642-14457-8
ISSN
0302-9743
Publisher
Springer Verlag
Start Page
178
End Page
195
Journal / Book Title
Lecture Notes in Computer Science
Volume
6194
Copyright Statement
© Springer-Verlag 2009. The final publication is available at Springer via http://dx.doi.org/10.1007/978-3-642-14458-5_11
Source
Web Services and Formal Methods: 6th International Workshop, WS-FM 2009
Subjects
Science & Technology
Technology
Computer Science, Information Systems
Computer Science, Software Engineering
Computer Science, Theory & Methods
Computer Science
LOGIC
Artificial Intelligence & Image Processing
08 Information And Computing Sciences
Publication Status
Published
Start Date
2009-09-04
Finish Date
2009-09-05
Coverage Spatial
Bologna, Italy