Venue

Ph.D. Thesis, Imperial College London

Publication Year

2011

Authors

  • Thomas Dinsdale-Young

Abstract

This thesis tackles problems concerning abstract data structures — expressibil- ity and decidability results for logics for reasoning about abstract data struc- tures, and techniques for proving the correctness of programs that implement abstract data structures. The main expressivity issue addressed is the ques- tion of whether certain spatial adjunct connectives contribute to the expressive power of context logic for trees. The question is answered in the affirmative for context logic in its basic form, but in the negative for a multi-holed variant of context logic. This result is interesting, since the adjunct connectives play an important role in expressing the weakest preconditions of programs. The decidability results show that multi-holed context logic is decidable for trees, sequences and terms, by encoding logical formulae with automata. Concerning the correctness of programs that implement abstract data struc- tures, this thesis presents two techniques for justifying abstract local reasoning about such implementations in the sequential setting. In the concurrent setting, this thesis presents an approach to verifying implementations of abstract specifi- cations that incorporate a fiction of disjointness using a fine-grained permissions model.

Source Materials