We verify the correctness of a recursive version of Tony Hoare's quicksort algorithm using the Hoare-logic based verification tool Dafny. We then develop a non-standard, iterative version which is based on a stack of pivot-locations rather than the standard stack of ranges. We outline an incomplete Dafny proof for the latter.

We study abstract local reasoning for concurrent libraries. There are two main approaches: provide a specification of a library by abstracting from concrete reasoning about an implementation; or provide a direct abstract library specification, justified by refining to an implementation. Both approaches have a significant gap in their reasoning, due to a mismatch between the abstract connectivity of the abstract data structures and the concrete connectivity of the concrete heap representations. We demonstrate this gap using structural separation logic (SSL) for specifying a concurrent tree library and concurrent abstract predicates (CAP) for reasoning about a concrete tree implementation. The gap between the abstract and concrete connectivity emerges as a mismatch between the SSL tree predicates and CAP heap predicates. This gap is closed by an interface function I which links the abstract and concrete connectivity. In the accompanying technical report, we generalise our SSL reasoning and results to arbitrary concurrent data libraries.

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.

Indexes are ubiquitous. Examples include associative arrays, dictionaries, maps and hashes used in applications such as databases, file systems and dynamic languages. Abstractly, a sequential index can be viewed as a partial function from keys to values. Values can be queried by their keys, and the index can be mutated by adding or removing mappings. Whilst appealingly simple, this abstract specification is insufficient for reasoning about indexes that are accessed concurrently. We present an abstract specification for concurrent indexes. We verify several representative concurrent client applications using our specification, demonstrating that clients can reason abstractly without having to consider specific underlying implementations. Our specification would, however, mean nothing if it were not satisfied by standard implementations of concurrent indexes. We verify that our specification is satisfied by algorithms based on linked lists, hash tables and BLink trees. The complexity of these algorithms, in particular the BLink tree algorithm, can be completely

Shared-memory concurrency plays an important role in modern computer systems: for example, in classic file systems and databases, and the evolving web and multi-core operating systems. Many of these systems make fundamental use of concurrent indexes. A concurrent index can be viewed as a mapping from key values to data (typically pointers), which can be accessed simultaneously by many threads calling read/write operations on key values. A user typically works with this abstract view of indexes, rather than with the intricate details of complex implementations. We could verify such implementations directly, but we instead choose to give a formal abstract specification of concurrent indexes, and verify that well-known implementations using BLink trees and hash tables satisfy this specification.

Local reasoning is a well established concept in the field of program verification, which is useful at different levels of abstraction. In separation logic we use a low-level abstraction that is close to how the machine sees the program state. In context logic we work with high-level abstractions that are close to how the clients of modules view the program state. We give a definition for what it means to correctly implement a module, and show how high-level abstract reasoning about a module can be translated to low-level reasoning about its implementation. We consider two approaches to such translations: those that preserve locality and those that break it.

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, they developed a formal specification of the Document Object Model, a W3C XML update library. Whilst they kept to the spirit of local reasoning, they were not able to retain small specifications: for example, the specification of appendChild was not small. We show how to obtain small specifications by working with a more fine-grained context structure, allowing us to work with arbitrary tree fragments.

This Transfer Report comes at the end of the first 8 months of my PhD here at Imperial College London. The purpose of this report is to outline the work that I have carried out in my time so far, and also to give an indication of what I hope to include in my final PhD Thesis write up. (Discusses Featherweight DOM, specifying Move, concurrent tree update, links to low-level reasoning and future implementations. Also includes a background survey of program reasoning, Separation Logic and Context Logic.)

The W3C Document Object Model (DOM) specifies an XML update library. DOM is written in English, and is therefore not compositional and not complete. We provide a first step towards a compositional specification of DOM. Unlike DOM, we are able to work with a minimal set of commands and obtain complete reasoning for straight-line code. Our work transfers O'Hearn, Reynolds and Yang's local Hoare reasoning for analysing heaps to XML, viewing XML as an in-place memory store as does DOM. In particular, we apply recent work by Calcagno, Gardner and Zarfaty on local Hoare reasoning about simple tree update to this real-world DOM application. Our reasoning not only formally specifies a significant subset of DOM Core Level 1, but can also be used to verify, for example, invariant properties of simple Javascript programs.

The W3C Document Object Model (DOM) specifies an XML update library. DOM is written in English, and is therefore not compositional and not complete. We provide a first step towards a compositional specification of DOM. Unlike DOM, we are able to work with a minimal set of commands and obtain complete reasoning for straight-line code. Our work transfers O'Hearn, Reynolds and Yang's local Hoare reasoning for analysing heaps to XML, viewing XML as an in-place memory store as does DOM. In particular, we apply recent work by Calcagno, Gardner and Zarfaty on local Hoare reasoning about a simple tree-update language to DOM, showing that our reasoning scales to DOM. Our reasoning not only formally specifies a significant subset of DOM Core Level 1, but can also be used to verify e.g. invariant properties of simple Javascript programs.

We present an initial attempt at providing a formal specification for a minimal structural subsection of DOM Core Level 1. From this 'Minimal DOM' we show how to extended our specification to cover all of the structural behaviour of DOM Core Level 1 and more. We first provide a local specification of our 'Minimal DOM' and then show how the use of Context Logic gives us a powerful and expressive reasoning framework with which to take our local specification to a high level specification. This will be the first time that Context Logic has been applied to a large, real-world, example. Our hope is that our work will demonstrate that Context Logic is just as applicable to real problems as its close sibling Separation Logic.