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

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

5.Parametric Expressivity

We present our expressivity results.We prove parametric inexpres-sivity results comparing BL for heaps with and without the struc-tural connectives,using a direct proof method.We prove strong inexpressivity results for specific interpretations σ,corresponding to the extension of BL with list predicates.We also study para-metric inexpressivity results comparing CL and BL for sequences and trees.We cannot prove the parametric results directly for these applications.Instead,we prove strong inexpressivity results,and hence by implication the parametric results.In addition,we study BL for bounded heaps,presenting logics which have the same strong expressivity for every interpretation σ,but different para-metric expressivity.

First some notation.Given ML-signature Σ=(S ,O,ρ)and AX-model M Σ,we let L M Σ,V denote the modal logic determined by Σand M Σwith propositional variables in V .We use L M Σ,V S to denote the restriction to propositional variables of sort S ,and L M Σ,{p }for the restriction to propositional variable p .We write L M Σ,V (− )for the logic without modality .For example,C L Seq A ,V D (−{ })denotes C L Seq A without modality and with the propositional variables restricted to sort D.

Definition 31(Parametric Expressivity).Let Σ=(S ,O,ρ)and Σ =(S ,O ,ρ )be two ML-signatures with sort S ∈S ∩S .Consider two models M ,M over the respective signatures such that M S =M S .Consider the logics L M ,V S and L M ,V S .1.Logic L M ,V S is as expressive as L M ,V S with respect to sort S ,written L M ,V S ⊆S L M ,V S ,if and only if ∀P ∈L M ,V S .∃P ∈L M ,V S .∀σ.∀m ∈M S .

σ,M ,m S P ⇔σ,M ,m S P .

We often write L M ,V S ⊆L M ,V S since the sort S is apparent.2.Given σ,logic L M ,V S is as σ-expressive as L M ,V S with respect to sort S ,written L M ,V S ⊆S,σL M ,V S ,if and only if ∀P ∈L M ,V S .∃P ∈L M ,V S .∀m ∈M S .

σ,M ,m S P ⇔σ,M ,m S P .

Again,we write L M ,V S ⊆σL M ,V S since S is apparent.We write L M ,V S =L M ,V S when L M ,V S ⊆L M ,V S and L M ,V S ⊇L M ,V S ,and L M ,V S =σL M ,V S analogously.In fact,we concentrate on inexpressivity results,asking when a logic is strictly more expressive than another.We say that L M ,V S is parametrically more expressive than L M ,V S iff L M ,V S L M ,V S .We say that L M ,V S is strongly more expressive than L M ,V S iff there exists a σsuch that L M ,V S σL M ,V S .

To prove our strong inexpressivity results we rely heavily on the notion of bisimulation.Bisimulation has the property that,if two elements of the models are bisimilar,then they cannot be dis-tinguished from each other in the logic,and hence can be directly used to prove strong inexpressivity.

Definition 32(Bisimulation).A symmetric binary relation ∼=S

S ∈S ∼S with ∼S ⊆M S ×M S is a bisimulation for ML-model M Σif and only if,whenever ((m 1,...,m n ),m )∈M ∆and

m ∼m ,then there exist m i ∈M S i such that m i ∼S i m

i

for i =1...n and ((m 1,...,m n ),m

)∈M ∆.A bisimulation ∼is compatible with interpretation σif and only if,for all m,p ,m ∈σ(p )∧m ∼m ⇒m ∈σ(p ).

Proposition 33.Let ∼be a bisimulation compatible with σfor ML-model M Σ.Then m 1∼S m 2implies σ,M ,m 1 S P iff σ,M ,m 2 S P for all P ∈P ΣS .

To show that L M ,V S σL M ,V S ,our proof method consists of finding a formula P ∈L M ,V S of sort S and a bisimulation ∼for M compatible with σ,such that P distinguishes two elements

which are identified by ∼.Inexpressivity then follows from Propo-sition 33that no formula in P Σcan distinguish the two elements.5.1

Heaps

We have the following results about heaps:

•B L Heap,V D =C L Heap,V D

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

The first result is a parametric expressivity result,showing that the structure of CL collapses to BL in the heap case.This result follows from Proposition 26.The second result is a non-parametric expres-sivity result due to Lozes [9],which compares the expressivity of closed formulae.It states that the adjunct −•can be eliminated if we add formulae n →−to specify that address n is allocated:n →−specifies that there exists m such that n →m .It is expressible using −•as ¬((n →0)−•true );the current heap cannot be extended with cell n ,so n must already be allocated.Lozes’result was initially quite a surprise,since the adjuncts are used in an essential way to describe the weakest preconditions for Hoare reasoning based on BL for heaps.We address this apparent contradiction here,by proving the third result.

The third result is a parametric inexpressivity result,which we prove by showing that formula (n →0)−◦p cannot be expressed in BL for heaps without −•.This formula is interesting because it expresses the weakest precondition of allocation.This inexpres-sivity result says nothing about whether the formula is expressible for a particular interpretation of p .By Lozes’results,we know that it is expressible for every interpretation of p as a closed formula.We also prove a strong inexpressivity result using the same formula and a natural interpretation σlist which interprets p as list (m ):that is,the heap contains a 0-terminated linked list starting at m .This result is interesting because lists are one of the typical inductive predicates used in BL-reasoning.Theorem 34(Parametric Inexpressivity).

B L Heap,{p }(−{−•} …… 此处隐藏：4998字，全部文档内容请下载后查看。喜欢就下载吧 ……