05908622

a

05908622 Dang, Han-Hing H\"ofner, Peter Variable side conditions and greatest relations in algebraic separation logic. de Swart, Harrie (ed.), Relational and algebraic methods in computer science. 12th international conference, RAMICS 2011, Rotterdam, The Netherlands, May 30 -- June 3, 2011. Proceedings. Berlin: Springer (ISBN 978-3-642-21069-3/pbk). Lecture Notes in Computer Science 6663, 125-140 (2011). 2011 Berlin: Springer EN

doi:10.1007/978-3-642-21070-9_11

Summary: When reasoning within separation logic, it is often necessary to provide side conditions for inference rules. These side conditions usually contain information about variables and their use, and are given within a meta-language, i.e., the side conditions cannot be encoded in separation logic itself. In this paper we discuss different possibilities how side conditions of variables-occurring e.g. in the ordinary or the hypothetical frame rule-can be characterised using algebraic separation logic. We also study greatest relations; a concept used in the soundness proof of the hypothetical frame rule. We provide one and only one level of abstraction for the logic, the side conditions and the greatest relations.