Elimination of spatial connectives in static spatial logics

摘要

The recent interest for specification on resources yields so-called spatial logics, that is specification languages offering new forms of reasoning: the local reasoning through the separation of the resource space into two disjoint subspaces, and the contextual reasoning through hypothetical extension of the resource space. We consider two resource models and their related logics: · The static ambient model, proposed as an abstraction of semistructured data (Proc. ESOP'Ol, Lecture Notes in Computer Science, vol. 2028, Springer, Berlin, 2001, pp. 1-22 (invited paper)) with the static ambient logic (SAL) that was proposed as a request language, both obtained by restricting the mobile ambient calculus (Proc. FOSSACS'98, Lecture Notes in Computer Science, vol., 1378, Springer, Berlin, 1998, pp. 140-155) and logic (Proc. POPL'OO, ACM Press, New York, 2000, pp. 365-377) to their purely static aspects. · The memory model and the assertion language of separation logic, both defined in Reynolds (Proc. LICS'02, 2002) for the purpose of the axiomatic semantic of imperative programs manipulating pointers. We raise the questions of the expressiveness and the minimality of these logics. Our main contribution is a minimalisation technique we may apply for these two logics. We moreover show some restrictions of this technique for the extension SAL{sup}({arbitrary}) with universal quantification, and we establish the minimality of the adjunct-free fragment (SAL{sub}(int)).