Abstract Context Logic as Modal Logic Completeness and Param(2)

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

taining propositional variables.This notion of expressivity deter-mines whether an arbitrary open formula in one logic,specifying a function from sets to data to sets of data,can be expressed by a formula in the other logic.There are two choices for the domain of this function,either as sets of data specified by closed formulae or as arbitrary sets of data.Thefirst option is enough to determine whether the weakest precondition can be specified in PL.It does not however allow for natural extensions to SL,such as the addition of inductive predicates.We therefore study the second option.We call this type of expressivity parametric expressivity,and show that SL is parametrically more expressive than PL for heaps by demonstrat-ing that(n→0)−∗p cannot be expressed in PL.

Although the SL-adjoint−∗is important for the weakest pre-conditions and has a key role in some proofs[12],it is not typi-cally used for specifying safety properties.For example,it plays no role in the verification tool Smallfoot[1],which combines in-ductive predicates with a cut-down decidable fragment of SL(with quantification).A more fundamental SL-formula is p∗q specifying that the heap can be split into two disjoint parts,one satisfying p and the other q.Lozes’results imply that,for every interpretation of p and q as sets of data corresponding to closed formulae,there is a corresponding PL-formula.Again,the PL-formulae are highly non-uniform.We show that it is not possible to express parametri-cally this formula in PL.However,with the Smallfoot application in mind,it is perhaps more interesting to determine a specific in-expressivity result,that it is not possible to express p∗q in PL with the interpretation of p as list(3),denoting the existence of a 0-terminated linked list starting at address3,and q as list(4).To do this,we study the notion of strong expressivity which states that, for a specific interpretation of the propositional variables as arbi-trary sets of data,every formula with propositional variables in one logic can be expressed in the other logic.

To prove our strong inexpressivity results,we use a standard bisimulation technique from ML.For example,consider the heaps h1=[3→n ,4→n ,n →0,n →0]

h2=[3→n ,4→n ,n →0,n →0].

These heaps are distinguished by SL-formula p∗q,with the in-terpretation of p and q as the lists list(3)and list(4)respectively, since h1can be split into the appropriate disjoint lists whereas h2 cannot due to the sharing at address n .Our proof shows that there is a PL-bisimulation relation relating h1and h2.Bisimulation has the well-known property that it is contained in logical equivalence. Thus,the heaps h1and h2are indistinguishable using PL.

Our original motivation for studying parametric inexpressivity results came from studying CL for trees and AL.We introduced CL to provide local Hoare reasoning about tree update[3],demon-strating that it was not possible to base our Hoare reasoning on AL since it had a missing adjoint.Whilst we believe that our argument was convincing,it was an argument given by example rather than by a formal inexpressivity result.Lozes’expressivity results,fo-cussing on the closed formulae,show that the argument is subtle since AL(without quantifiers)is as expressive as the logic without the structural adjoints[9,6].We prove that CL for trees is paramet-rically more expressive than AL.Unlike the results for SL,we do not know how to prove this directly.Instead,we prove a strong in-expressivity result using an analogous proof method to that outlined above.Since strong inexpressivity implies parametric inexpressiv-ity,we have the result.In addition,we prove that CL for trees minus the extra adjoint is parametrically as expressive as AL,thus show-ing that the additional strength of the CL-reasoning does indeed come from this additional adjoint.We also prove similar results for CL for sequences and a variation of BL applied to sequences(∗is non-commutative).Sequences provide the simplest example of the differences between CL-and BL-reasoning.Again,we prove our parametric inexpressivity result via strong inexpressivity.

2.Context Logic and Bunched Logic

We review the general theory of CL and BL.

2.1Context Logic

We introduced CL to reason about data update[3].Local data up-date typically identifies the portion of data to be replaced,removes it,and inserts the new data in the same place.With CL,we reason about both data and this place of insertion(contexts).CL consists of data formula denoted by P,and context formulae denoted by K. In each case,these include standard formulae from propositional logic,and less familiar structural formulae for directly analysing the data and context structure.

Definition1(CL-Formulae).The set of CL-formulae consists of disjoint sets of data formulae P and context formulae K,con-structed from a set of propositional variables V=V P∪V K where V P and V K are disjoint,countably infinite sets of propositional data variables and context variables respectively.The formulae are given by the grammars:

data formulae

P::=K(P)|K P structural formulae

P∨P|¬P|false additive formulae

p,p1,p2,...prop vars in V P

context formulae

K::=I|P P structural formulae

K∨K|¬K|False additive formulae

k,k1,k2,...prop vars in V K The key formulae are the structural formulae K(P),K P, P1 P2and I.The application formula K(P)specifies that the

given data element can be split into a context satisfying K applied to data satisfying P.For example,if we define the context formula True ¬False,then the formula True(P)states th …… 此处隐藏：5044字，全部文档内容请下载后查看。喜欢就下载吧 ……