Elimination of spatial connectives in static spatial logics

Description

The recent interest for specification on resources yields so-called spatial logics, that is specification languages offering spatial connectives: a separation into two subcomponents of the considered structure, (* ,or |), and its adjunct, the guarantee respect to the extension of the structure (− * ,). We consider two resource models and their related logics: • the Static Ambient (SA), proposed as a model of semistructured data [4], with the Static Ambient Logic (SAL) that was proposed as a request language, both obtained restricting the Mobile Ambient calculus [5] and logic [6] to their purely static aspects. • the shared mutable data structures adressed by the Separation Logic (SL), as it has been defined in [15] as an adequate assertion language for Hoare style reasoning on imperative programs manipulating pointers. We raise the questions of the expressiveness and the minimality of these logics. Our main contributions are the elimination of adjuncts for SAL, the minimality of the adjunct-free fragment (SAL int), and the elimination of both spatial connectives * and − * for SL.

Abstract

International audience

Additional details