Abstract Context Logic as Modal Logic Completeness and Param

similar style of reasoning about structured data. They each consist of a structural (separating) composition for reasoning about disjoint subdata, and corresponding structural adjoint(s) for reasoning hypothetically about data. We show how to interpret the

Context Logic as Modal Logic: Completeness and Parametric Inexpressivity

Cristiano Calcagno Philippa Gardner Uri Zarfaty

Department of Computing,Imperial College London

{ccris,pg,udz}@doc.ic.ac.uk

Abstract

Separation Logic,Ambient Logic and Context Logic are based on a similar style of reasoning about structured data.They each consist of a structural(separating)composition for reasoning about dis-joint subdata,and corresponding structural adjoint(s)for reasoning hypothetically about data.We show how to interpret these struc-tural connectives as modalities in Modal Logic and prove complete-ness results.The structural connectives are essential for describing properties of the underlying data,such as weakest preconditions for Hoare reasoning for Separation and Context Logic,and secu-rity properties for Ambient Logic.In fact,we introduced Context Logic to reason about tree update,precisely because the structural connectives of the Ambient Logic did not have enough expressive power.Despite these connectives being essential,first Lozes then Dawar,Gardner and Ghelli proved elimination results for Separa-tion Logic and Ambient Logic(without quantifiers).In this paper, we solve this apparent contradiction.We study parametric inexpres-sivity results,which demonstrate that the structural connectives are indeed fundamental for this style of reasoning.

Categories and Subject Descriptors D.2.4[Software/Program verification]:Correctness proofs,Formal methods,Validation General Terms Languages,Theory,Verification

Keywords Logic,Expressivity,Structured Data,Contexts

1.Introduction

Separation Logic(SL)and Ambient Logic(AL)are related log-ics for reasoning about heaps and trees respectively.O’Hearn, Reynolds and Yang introduced SL[8,11,13]to develop local Hoare reasoning about heap update,based on the general theory of Bunched Logic(BL)due to O’Hearn and Pym[10].Cardelli and Gordon independently introduced AL[5]for reasoning about static trees.AL has been used to reason about security properties of firewalls and structural properties of XML[6].We have integrated these two lines of research.In[3],we showed that it is not possible to use AL to reason about tree update(XML update).Instead,we introduced the general theory of Context Logic(CL)for reasoning about structured data,which generalises BL.We demonstrated that the application of CL-reasoning to trees can be used as a basis for Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on thefirst page.To copy otherwise,to republish,to post on servers or to redistribute to lists,requires prior specific permission and/or a fee.

POPL’07January17–19,2007,Nice,France.

Copyright c 2007ACM1-59593-575-4/07/0001...$5.00local Hoare reasoning about tree update,whilst the application of CL-reasoning to heaps exactly corresponds to SL-reasoning.

These logics are based on a similar style of reasoning about structured data.They each extend propositional connectives with a structural(separating)composition for reasoning about disjoint subdata,and the corresponding structural adjoint(s).1We show how to interpret the structural connectives of BL and CL as modalities in modal logic(ML).We present additional axioms for these modali-ties to give a precise correspondence between the original presenta-tion of BL and CL,and their ML-interpretations.These axioms are well-behaved,in that they satisfy the conditions necessary for us to apply a general completeness result about ML(Sahlqvist’s the-orem).We thus prove that the CL-proof theory is sound and com-plete with respect to the set of CL-models(and analogously for BL).This work follows previous unpublished work by Calcagno and Yang,who proved completeness for CL fromfirst principles.

The structural connectives are essential for modular reason-ing about programs,and for describing weakest preconditions and safety properties.However,recent expressivity results for SL and AL due to Lozes[9]appear to contradict this fundamental claim. Lozes concentrates on expressivity for closed formulae,determin-ing whether an arbitrary closed formula specifying a set of data in one logic can be expressed by a formula in the other logic speci-fying the same set of data.For example,Lozes has shown that SL and Propositional Logic(PL)with simple atomic heap formulae are equally expressive using this definition of expressivity.How-ever,our experience says that SL is more expressive than PL,since for example we can reason directly about disjointness and dynamic update of linked lists.We solve this apparent mismatch between the theoretical results and our practical experience by proving in-expressivity results for stronger definitions of expressivity.

SL forms the basis of local Hoare reasoning about heap update. An important part of the reasoning is to be able to express the weakest preconditions,which provide completeness for straight-line code and have a key role in some verification tools(to verify a Hoare triple,firstfind the weakest precondition of a given postcon-dition and then prove that the given precondition implies the weak-est precondition).Our results show that the weakest preconditions cannot be expressed in PL for heaps.To illustrate this,consider the weakest precondition of allocation(n→0)−∗p,specifying that whenever a cell with address n and value0is added to the given heap then the resulting heap satisfies post-condition p.Lozes’result says that,f …… 此处隐藏：4277字，全部文档内容请下载后查看。喜欢就下载吧 ……