zbMATH — the first resource for mathematics

Compositional reasoning for pointer structures. (English) Zbl 1235.68050
Uustalu, Tarmo (ed.), Mathematics of program construction. 8th international conference, MPC 2006, Kuressaare, Estonia, July 3–5, 2006. Proceedings. Berlin: Springer (ISBN 978-3-540-35631-8/pbk). Lecture Notes in Computer Science 4014, 115-139 (2006).
Summary: This paper studies the compositional definition and behaviour of properties that arise in pointer structures. A pointer structure is represented as a (pointer) graph. A pointer property is a set of pointer structures. A parameterised binary combinator is defined that enables important properties (like acyclicity, canonicity and reachability) to be defined in a compositional manner. The technique of parameterising a combinator derives from the definition of parallel-by-merge in ‘Unifying Theories of Programming’. It is applied here to the study of disjointness combinators that extend the separating conjunction of Separation Logic. A case study is provided to demonstrate how these ideas are used, in the form of rules of Hoare logic, to verify the correctness of an Object-Oriented program.
For the entire collection see [Zbl 1107.68016].

68N30 Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.)
68N19 Other programming paradigms (object-oriented, sequential, concurrent, automatic, etc.)
68Q60 Specification and verification (program logics, model checking, etc.)
Full Text: DOI