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

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

starting at m and stopping with dangling pointer n.This cannot be expressed without−◦,since only whole lists can be observed. Theorem35(Strong Inexpressivity).

B L Heap,{p}(−{−•}+{n →−}) σ

list

B L Heap,{p}

Proof.Consider the BL-formula P (n→0)−◦p,and interpre-tationσlist(p)=list(m)for m=n.We show that there is no formula P in B L Heap,{p}(−{−•}+{n →−})that is equivalent to P usingσlist.Expecting a contradiction,suppose that such a P exists,and let L⊆N be thefinite number of constants mentioned in P .Consider the restriction of B L Heap to constants in L,written

B L Heap

L .We choose a bisimulation∼which identifies two heaps

when they have the same domain,coincide on values in L,and are identical if one of them contains a list starting at m:

h1∼h2iff dom(h1)=dom(h2)and

∀i,j∈L.h1(i)=j iff h2(i)=j and

if h1|=list(m)or h2|=list(m)then h1=h2. Notice thatσlist(p)is compatible with∼,since if h1∼h2and h1|=list(m)then h2|=list(m).Assume for the moment that ∼is indeed a bisimulation.With this assumption,we show that we do indeed obtain a contradiction.Take m /∈L∪{n,m}and consider the heaps h1=[m→m ,m →n]and h2=[m→m ,m →m ].Note that h1∼h2andσ,h1|=(n→0)−◦p butσ,h2|=(n→0)−◦p.Assuming that∼is a bisimulation

for B L Heap

L,{p}(−{−•}+{n →−}),Proposition33implies that

σlist,h1|=BL P iffσlist,h2|=BL P .We have therefore proved that there cannot be a BL-formula P which is equivalent to P.

Finally,we must prove our assumption that∼is a bisimulation for the modalities{0,◦}∪{i →j,i →−|i,j∈L}.We only look at the◦modality;the other cases are trivial.Assume h1=h 1·h 1 and h1∼h2.We must show that∃h 2,h 2such that h2=h 2·h 2 and h 1∼h 2and h 1∼h 2.Choose h 2,h 2as the unique splitting of h2such that dom(h 2)=dom(h 1)and dom(h 2)=dom(h 1).We show h 1∼h 2;the case h 1∼h 2is identical by symmetry.Thefirst and second conditions in the definition of∼are immediate.For the third condition,assume h 1|=list(m),which implies h1|=list(m) since h 1is a sublist of h1.By definition of h1∼h2,we have h1=h2,hence h 1=h 2which is the desired conclusion.

Lozes also shows that,with an additional modality size r for determining the size of heaps,the◦-modality can be removed.We show that◦is essential for parametric reasoning.The results are:•B L Heap,∅(−{◦,−•}+{size r})=B L Heap,∅(−{−•})

•B L Heap,{p,q}(−{◦,−•}+{size r}) B L Heap,{p,q}(−{−•}). The results also hold with modality n →−.Thus,BL is as ex-pressive as PL with atomic formulae0,size r and n →−,but not parametrically so.We believe this parametric inexpressivity result demonstrates what has been always known intuitively,but by ex-ample only,that the◦-modality is essential for modular reasoning.

We give a direct proof of our parametric inexpressivity result for◦based on the trivial observation that,without◦and−•,all the modalities leave the current heap unchanged.The modality size r, for each r∈N+,is interpreted by h|=size r iff|dom(h)|≤r. We do not require size0as it corresponds to the zero formula0. Theorem36(Parametric Inexpressivity).

B L Heap,{p,q}(−{◦,−•}+{size r}) B L Heap,{p,q}(−{−•}) Proof.The proof is analogous to that of Thm.34.A formula P is heap-invariant iff,when h∈σ(p)⇔h∈σ (p)for all p,then σ,h|=P⇔σ ,h|=P.The formulae in B L Heap,{p,q}(−{◦,−•}+ {size r})are heap-invariant,but p◦q is not.We also prove a second strong inexpressivity result,that◦cannot be eliminated withfixed interpretationσlist,which interprets p and q as list(m1)and list(m2)respectively for m1=m2.The◦modality is essential for specifying the property that the two lists are in the heap and their tails never meet.

Theorem37(Strong Inexpressivity).

B L Heap,{p,q}(−{◦,−•}+{size r}) σ

l ist

B L Heap,{p,q}(−{−•}) Proof.The structure of the proof is analogous to Theorem35. Consider the BL-formula p◦q.As in Theorem35,we restrict our attention to BL-formulae mentioning at most afinite set L⊆N of constants and the propositional variables p,q.

Consider the interpretation h∈σlist(p)iff h satisfies list(m1), and h∈σlist(q)iff h satisfies list(m2).Define relation∼by: h1∼h2iff|dom(h1)|=|dom(h2)|and

σ,h1|=P⇔σ,h2|=P for

P∈{p,q}∪{i →j|i,j∈L}

∼is compatible withσand is a bisimulation for the modalities {0,size r}∪{i →j|i,j∈L}.Take h1=[m1→n ,m2→n ,n →0,n →0]and h2=[m1→n ,m2→n ,n →0,n →0]for distinct n ,n /∈L∪{m1,m2}.Then h1∼h2 andσ,h1|=p◦q,butσ,h2|=p◦q.

From the previous examples,one might be tempted to conclude that whenever a parametric inexpressivity result holds,a corresponding strong inexpressivity result holds too.In fact,this is not the case as we demonstrate using bounded heaps.In bounded heaps,−•cannot be eliminated parametrically for reasons identical to the unbounded case.However,given a specific interpretationσ,any formula is equivalent to a disjunction of characteristic formulae without−•. Theorem38.Let Heap k denote the restriction of heaps,and correspondingly formulae,to locations≤k.The following hold: 1.B L Heap

k,{p}

(−{−•}+{n →−}) B L Heap

k,{p}

2.B L Heap

k,{p}

(−{−•}+{n →−})=σB L Heap

k,{p}

for allσ. Proof.The proof of part1is identical to the proof of The-orem34.For part2,we in fact prove a stronger claim:for any set of heaps H⊆Heap k,there exists a formula …… 此处隐藏：4382字，全部文档内容请下载后查看。喜欢就下载吧 ……