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 (rst-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 dene a guarded fragment that turns out to be both decidable and suciently expressive to prove the preservation of the loop invariant of ...

• Type: Conference
• Year: 2009
• Where: FOSSACS
• Authors: Kshitij Bansal, Rémi Brochenin, Étienne Lozes
• Keywords: Applied Computing, FOSSACS 2009, Ordered Lists, Recursive Data Structures, Separation Logic