Powered by OpenAIRE graph
Found an issue? Give us feedback
addClaim

Segment Logic

Authors: Wheelhouse, Mark James;
Abstract

O'Hearn, Reynolds and Yang introduced local Hoare reasoning about mutable data structures using separation logic. They reason about the local parts of the memory accessed by programs, and thus construct their smallest complete specifications. Gardner et al. generalised their work, using context logic to reason about structured data at the same level of abstraction as the data itself. In particular, we developed a formal specification of the Document Object Model (DOM), a W3C XML update library. Whilst we kept to the spirit of local reasoning, we were not able to retain small specifications for all of the commands of DOM: for example, our specification of the appendChild command was not small. We show how to obtain such small specifications by developing a more fine-grained context structure, allowing us to work with arbitrary segments of a data structure. We introduce segment logic, a logic for reasoning about such segmented data structures, staring at first with a simple tree structure, but then showing how to generalise our approach to arbitrary structured data. Using our generalised segment logic we construct a reasoning framework for abstract program modules, showing how to reason about such modules at the client level. In particular we look at modules for trees, lists, heaps and the more complex data model of DOM. An important part of any abstraction technique is an understanding of how to link the abstraction back to concrete implementations. Building on our previous abstraction and refinement work for local reasoning, we show how to soundly implement the segment models used in our abstract reasoning. In particular we show how to implement our fine-grained list and tree modules so that their abstract specifications are satisfied by the concrete implementations. We also show how our reasoning from the abstract level can be translated to reasoning at the concrete level. Finally, we turn our attention to concurrency and show how having genuine small axioms for our commands allows for a simple treatment of abstract level concurrency constructs.

Country
United Kingdom
Related Organizations
Keywords

004

  • BIP!
    Impact byBIP!
    selected citations
    These citations are derived from selected sources.
    This is an alternative to the "Influence" indicator, which also reflects the overall/total impact of an article in the research community at large, based on the underlying citation network (diachronically).
    0
    popularity
    This indicator reflects the "current" impact/attention (the "hype") of an article in the research community at large, based on the underlying citation network.
    Average
    influence
    This indicator reflects the overall/total impact of an article in the research community at large, based on the underlying citation network (diachronically).
    Average
    impulse
    This indicator reflects the initial momentum of an article directly after its publication, based on the underlying citation network.
    Average
Powered by OpenAIRE graph
Found an issue? Give us feedback
selected citations
These citations are derived from selected sources.
This is an alternative to the "Influence" indicator, which also reflects the overall/total impact of an article in the research community at large, based on the underlying citation network (diachronically).
BIP!Citations provided by BIP!
popularity
This indicator reflects the "current" impact/attention (the "hype") of an article in the research community at large, based on the underlying citation network.
BIP!Popularity provided by BIP!
influence
This indicator reflects the overall/total impact of an article in the research community at large, based on the underlying citation network (diachronically).
BIP!Influence provided by BIP!
impulse
This indicator reflects the initial momentum of an article directly after its publication, based on the underlying citation network.
BIP!Impulse provided by BIP!
0
Average
Average
Average
Upload OA version
Are you the author of this publication? Upload your Open Access version to Zenodo!
It’s fast and easy, just two clicks!