Beyond Shapes: Lists with Ordered Data

摘要

Standard analysis on recursive data structures restrict their attention to shape properties (for instance, a program that manipulates a list returns a list), excluding properties that deal with the actual content of these structures. For instance, these analysis would not establish that the result of merging two ordered lists is an ordered list. Separation logic, one of the prominent framework for these kind of analysis, proposed a heap model that could represent data, but, to our knowledge, no predicate dealing with data has ever been integrated to the logic while preserving decidability. We establish decidability for (first-order) separation logic with a predicate that allows to compare two successive data in a list. We then consider the extension where two data in arbitrary positions may be compared, and establish the undecidability in general. We define a guarded fragment that turns out to be both decidable and sufficiently expressive to prove the preservation of the loop invariant of a standard program merging ordered lists. We finally consider the extension with the magic-wand and prove that, by constrast with the data-free case, even a very restricted use of the magic wand already introduces undecidability.