TY - JOUR

T1 - Modular Verification of Linked Lists with Views via Separation Logic

AU - Jensen, Jonas Braband

AU - Birkedal, Lars

AU - Sestoft, Peter

PY - 2011/1

Y1 - 2011/1

N2 - We present a separation logic specification and verification of linked lists with views, a data structure from the C5 collection library for .NET. A view is a generalization of the well-known concept of an iterator. Linked lists with views form an interesting case study for verification since they allow mutation through multiple, possibly overlapping, views of the same underlying list. For modularity, we build on a fragment of higher- order separation logic and use abstract predicates to give a specification with respect to which clients can be proved correct. We introduce a novel mathematical model of lists with views, and formulate succinct modular abstract specifications of the operations on the data structure. To show that the concrete implementation realizes the specification, we use frac- tional permissions in a novel way to capture the sharing of data between views and their underlying list. We conclude by suggesting directions for future research that arose from conducting this case study.

AB - We present a separation logic specification and verification of linked lists with views, a data structure from the C5 collection library for .NET. A view is a generalization of the well-known concept of an iterator. Linked lists with views form an interesting case study for verification since they allow mutation through multiple, possibly overlapping, views of the same underlying list. For modularity, we build on a fragment of higher- order separation logic and use abstract predicates to give a specification with respect to which clients can be proved correct. We introduce a novel mathematical model of lists with views, and formulate succinct modular abstract specifications of the operations on the data structure. To show that the concrete implementation realizes the specification, we use frac- tional permissions in a novel way to capture the sharing of data between views and their underlying list. We conclude by suggesting directions for future research that arose from conducting this case study.

U2 - 10.5381/jot.2011.10.1.a2

DO - 10.5381/jot.2011.10.1.a2

M3 - Journal article

SN - 1660-1769

VL - 10

SP - 21

EP - 40

JO - Journal of Object Technology

JF - Journal of Object Technology

IS - 1

ER -