@inbook {IOPORT.05887524,
    author       = {Tamalet, Alejandro and Madlener, Ken},
    title        = {Reasoning about assignments in recursive data structures.},
    year         = {2011},
    booktitle    = {Formal methods: foundations and applications. 13th Brazilian symposium on formal methods, SBMF 2010, Natal, Brazil, November 8--11, 2010. Revised selected papers},
    isbn         = {978-3-642-19828-1},
    pages        = {161-176},
    publisher    = {Berlin: Springer},
    doi          = {10.1007/978-3-642-19829-8_11},
    abstract     = {Summary: This paper presents a framework to reason about the effects of assignments in recursive data structures. We define an operational semantics for a core language based on Meyer's ideas for a semantics for the object-oriented language Eiffel. A series of field accesses, e.g. $f_{1} \bullet f_{2} \bullet \cdot \cdot \cdot \bullet f_{n}$ , can be seen as a path on the heap. We provide rules that describe how these multidot expressions are affected by an assignment. Using multidot expressions to construct an abstraction of a list, we show the correctness of a list reversal algorithm. This approach does not require induction and the reasoning about the assignments is encapsulated in the mentioned rules. We also discuss how to use this approach when working with other data structures and how it compares to the inductive approach. The framework, rules and examples have been formalised and proven correct using the PVS proof assistant.},
    identifier   = {05887524},
}