论文研究 处理内共享的分离逻辑扩展 .pdf

处理内共享的分离逻辑扩展，黄达明，曾庆凯，分离逻辑能够支持对指针程序的形式化验证，可以容易地对列表和树等易于表达分离的数据结构进行推理，但是在对十字链表和图等包含山国武花论文在丝在当前结构之内,同吋又表明在此结构之内又有局部推理发生。如图所示。给出了个具有内共享的结构,指向的一棵二叉树τ,树中结点要么具有两棵子树,要么是叶结点而指向的是由二叉树τ的所有叶结点连接而成的链表,是最右边一个叶结点指向的下个位置(对完整链表应该为)。此时这个叶结点链表属于树的一部分,两个结构是内共享的,普通合取表示对于树τ的堆空间,一部分属于叶链表,由0表示,另一部分不属于叶链表但属于树的堆空间,用表示。给出了部分图的分离逻辑表示。其中第一个公式刻画了空部分图,第二个公式刻画了部分图中的一个结点,第三个公式刻画了从结点α出发的图,而结点a通过两条边分别连到从λ和p出发的两个子图。为了刻画内共享,引入了记录名字映射的环境集合和,其中是原始环境,而是将欲刻画的部分图扩展进来后输山的新环境入图具有内具享的结构树也是包含内共享的结构,其叶结点也被链接成一个单向链表,中使用分离逻辑和抽象机语义对树进行了推理,给出另一种思路。从数据结构形状分析角度引入了截断概念,在递归谓词中使用截断点集合,能够在面临内共享结构时,通过将戗断点集合表示的堆部分排除在外,从而将推理集中于所关注的局部堆部分。作者提出了基于截断点的归纳递归合成体系,包括目标语言、抽象状态以及抽象操作语义等的定义和相关的算法,能够处理较为复杂的包含內共亨的数据结构,但是其整体结构相比较和要复杂的多,其主要目的是分析数据结构的形状。从以上分析可以看出使用分离逻辑对内共享结构的衣达是因难的,而且不太直观,直接使用分离逻辑进行推理存在繁琐和难以扩展的问题。例如,链衣是使用广泛的·种数据结构,对分离的两条单向或双向链表来说,使用分离逻辑处理是很简单的。但是有时候会有两条链表交叉并且有多处共享的情况,例如在操作系统內核中经常使用链表来管理进程。这时构成运行进程队列的链表和由系统中某个进程的所有子进程构成的兄弟进程链表之间就有可能存在多处相交结点假设有运行进程链表定义兄弟进程链表定义若链表和B只有唯一的共享结点,则使用分离进辑表达为彐acBBBB而如果和B具有两个不同的共享结点和→,则使用分离逻辑表达为彐 aaa Bp尸山国武花论文在丝可见,在验证过程中难以表达这类“内共享亨”属性,主要表现为:〕表达非常繁琐,当共亨子结构部分较多时推理难以扩展;)很难直接反映出哪些子结构是两个独立结构所共享的。为此,本文引入一个新的突出内共亨关系的逻辑连接词以及相应的推导规则,米解决此问题针对内共享的分离逻辑扩展2.1带共享的分离合取这里我们首次提出扩展分离逻辑以处理带有共享部分的内存结构的三目逻辑连接词,∝表示堆可以被分为两个部分和它们具有共享的区域除了共享区域外和的其余部分满足分离属性且这两块区域以及它们共享的区域分别满足相应的谓词和特别指出的是这个定义强调了和除了以外没有其他共亨的区域。推导规则引入带共享的分离合取连接词的目的是为了方便对包含内共享的数据结构进行推理分析而内共享部分是两块物理堆结构之间唯一的联系以下推导规则可以将带共享的分离合取与分离逻辑原有的分离合取以及分离蕴含联系起来,从而消除内共享带来的推理障碍。以上两个推导规则衣达了对于只包含块内共享部分的两块堆结构之间的推理关系。规则表明,如果和之问间共享,而由和两个部分构成,则从结构中去除的部分与结构满足分离关系。规则明确表达,对于包含内共享部分的两块堆结构和,去除以后的部分’和满足分离关系。规则表明,对于两块分离的堆结构和,本身属于的一部分,当将附加到’上构成新的堆结构后,和之间唯一共享。规则表明,如果由和三部分构成,而和构成’,则’和唯一共享,并且与构成分离属性。规则建立了局部推的基础,表明如果和哐一共亨,并且与相互分离,贝和都保持和的分离属性,这样在、和中进行的局部推理不会影响对于包含不止一块内共享部分的两个堆结构,可以使用以下规则进行推理。山国武花论文在丝规则表明,如果和共享和两部分,并且和是分离的,而从中去除部分后得到’,则和只共享部分。规则表明,和共享部分,现有和分离,且属于的一部分,如果将附加到’上得到,则和共享和两个部分。特别的,我们还可以使用带共享的分离合取实现判断指针别名情况:对于带有内共亨的结构之间的合并,我们还有以下规则引入带共享分离合取连接词的优点以第节最后的问题为例,对于和F具有两个不同的共享结点和的情况,使用木文扩展后的分离逻辑表达为由此可见,在内共亨存在的情况下,带共亨的分离合取连接词可以极大的简化表达,突山共享的了结构。并且使用本文引入的相关推导规则,可以方便的对内共享的数据结构进行推理验证。下面以十字链表以及文献中的二叉树极其边缘链衣为例,说明带共享的分离合取连接词及其推导规则的应用十字链表的分离逻辑表达从结构上来说,十字链表可以看作由若干横冋和纵冋数据链表构成,每条橫向数据链表与纵向数据链表至多有一个共亨结点。在不同的应用中,|字链表的构成可能稍有不同。木文处理的十字链结构的非形式化描述为:横向数据链衣和纵向数据链衣均具有独立的长头结点,每条链表均为单向无环链表;横向数据链表的所有表头结点组织成单向无环链表形式,纵向数据链表的表头结点也同样组织;整个十字链表无总表头结点,通过横向表头链表头指针和纵问表头链表头指针引用。十字链表的结构如图所示。横向表头结点纵向表头结点效据结点图3.十字链表由此,可以分别给出十字链表表头结点和数据结点的语法定义横向表头结点语法定义纵冋表头结点语法定义数据结点语法定义山国武花论文在丝其中,是指向结点的指针,是指向结点的指针,而和都是指向结点的指针,相同的数据结点通过指针链接构成了横向数据结点链表,而相同的数据结点通过指针链接构成纵向数据结点链表本文形式化描述十字链表的思想是首先给出十字链表中包含的底层子结构的形式化定义,然后定义这些子结构在组合成十字链表时自底向上应该保持的属性,最后向上合成抽象出十字链表的数据结构不变式。这样做的原因在于:无法直接给出十字链表的形式化定义;这是一种自底向上模块化组合的形式化描述方法,在验证时可以剎用分离逻辑推理的局部性和模块化优势。定义十字链表中的结点链表的定义十字链表主要由横向表头链表、纵向表头链表、横向数据结点链表以及纵向数据结点链表四种子结构构成,虽然都是链表结构,但是为了使于推理,分别予以定义。横向数据结点链表中所有数据结点的成员的值相同,因此横向数据结点链表的分离逻辑归纳定义如下∧●≡=卜纵向数据结点链表中所有数据结点的成员的值相同,纵向数据结点链表的分离逻辑归纳定义为:●}橫向表头链表中的每个表头结点的成员都指向一个横向数据结点链表,因此横向表头结点链表的分离逻辑归纳定义如下纵向表头链表中的每个表头结点的成员都指向一个纵数据结点链表,纵向表头结点链表的分离逻辑归纳定义为:下面进入十字链表表达中关键的部分:表头结点链表和数据结点链表是分离的,但是横向数据结点链表和纵向数据结点链表之间不一定是分离的,它们可能有至多一个共享部分,即和匹配的那个数据结点。为了刻画堆上的这种状态,我们使用带共享的分离合取逻辑连接词:C*B∝H特别地,可以推出有唯一共享结点的两条正交数据结点链表之间的关系为CBBB定义十字链表中数据结点链表的可达性十字链表中任何一个横向数据结点链表都是可以通过横向表头结点链表中某个结点的成员来引用,而任何一个纵向数据结点链表都可由纵向表头结点链表中某个结点的山国武技论文在丝成员指向,我们定义了两个谓词刻画这个属性横向数据结点链表可达性纵向数据结点链表可达性定义十字链表中子链表之间的共享关系为了措述十字链表中仟意横向数据结点链表和纵向数据结点链表至多只有一个共享结点,以及横冋数据结点链表之间互相分离,纵向数据结点链表之间也互相分离的空间关系属性,根据定义和定义我们定义以下三个谓词横向数据结点链表和纵向数据结点链表之间的共亨关系B7V彐6C. b横向数据结点链表之间的共享关系纵向数据结点链衣之间的共享关系定义谓词在堆上定义由横向表头链表头指针和纵向表头链表头指针决定的十字链表B定义给出十字链表数据结构属性不变式:()整个十字链表的堆空间由横向表头结点链表、纵向表头结点链表和数据结点集合三部分构成,且这三部分可相分离;()每条数据结点链袤都可以通过表头结点链表找到,而且每个数据结点都是一条横向数据结点链表和一条纵向数据结点链表的共亨交点:()横向数据结点链表和纵向数据结点链表或者互相分离,或者至多有一个共亨结点;()不同的横向数据结点链表互相分离,纵向数据结点链衣亦是如此对十字链表操作的分离逻辑推理和验证图插入数据结十字链表上的操作包括插入表头结点、删除表头结点、插入数据结点和删除数据节点等,山国武花论文在丝考虑篇幅限制,仅给岀对于插入数据节点的推理示例。插入数据结点插入数据结点操作需要分析插入结点所在的横向数据结点链表和纵向数据结点链表是否为空,它们是否已经包含相交的数据结点等情况,并分别作岀处理,对其作岀正确性证明的过程比较繁琐和冗长。本文的目的主要是演小对分离逻辑所作扩展在验证过程中的优点,因此我们对插入数据结点之前的前置条件作出一些简化性的假设:()相应的表头结点L经存在,而|字链表中不存在其和成员与待插入结点相应成员相同的数据结点,()对应的横向数据结点链表和对应纵向数据结点链非空。基于假设,实现插入数据结点的具体代码见图。我们需要证明,对于给定的十字链表和一个待插入的由指向的数据结点,在进行插入操作之后结果正确,即得到将指向的数据结点插入原十字链表后得到的新十字链表采用形式化描述如下。彐axBn证明由图可知,通过对插入过程进行分析,整个过程可以分成两个步骤:第一个步骤是査找插入的位置,而第二个步骤才是完成真正的插入数据结点操作。对」查找插入位置,不会改变宇链表结构,因此主要需要完成对插入数据结点步骤的证明插入薮据结点时,首先将其链入相应的向数据结点链表,此时十字链表属性被暂吋破坏,再将这个数据结点再链入相应的纵向数据结点链衣,十字链衣属性得以重建,这对应着图中突出背景显示的两行命令,因此主要给出和此两行命令对应的验证。基于假设,具体的证明目标为如下,其中表示除了断言显示表达的堆状态以外的堆部分保持不变:以下给出具体证明过程:>由分离蕴含连接词的推导规则,得到)>山国武技论文在丝由本文推导规则,得到进而,由部分所表达的堆状态,十字链表属性得到重建:Ha s得证口5二叉树及其边缘链表二叉树及其边缘链表的图示可以参见图,这里二叉树和边缘链表之间不仅满足内共亨的关系,其实更加精确的摧述应该是边缘链表是二义树的一部分。使用木文的分离逻辑扩展,图中的二义树及其边缘链表将表达为了下面对中的边缘链表创建算法进行推理验证,仍然以算法的部分为例:以上推导过程由于篇幅省略,具体可见文献又++p由本文推到规则对比文献中使用分离逻辑进行描述的方法是采取∧的形式,以表示中除了以外的部分,当需要进行∧形式的推导时,使用的是逻辑中的相关规则,显得不直观和难以理解,而木文引入的带共亨的分离合取连接词可以很明确的表达出边缘链表和二叉树之间的关系,也可以方使的进行推理验证总结本文的贡献在于:)扩展了分离逻辑,提出了处理包含共享子结构的内共享分离合取逻辑连接词,并引入相关推导规则,能够在数据结构的分离状态与包含内共享的状态之间建立联系。对比原分离逻辑,木文对分离逻辑的扩展可使得具有内共亨子结构的薮据结构的表达和推理更加方便和简沽,并且更加突出了结构之间的内共享属性。)本文对难以归纳定义的十字链ξ结构进行了形式化描述,并对其操作使用本文的分离逻辑扩展进行了推理验证;我们还完成了对二叉树及其边缘链表进行了形式化描述及相关算法的验证工作。包含内共亨的结构有多种情形,本文提出的分离逻辑扩展可以很好的处理这样一类情况:內共享是由两个比较独立的结构互联形成的,不论这两个结构之间可以有多少交叉共享的部分。但是,像和图等结构,其内共享更加复杂,一个结点往往由多个其它结点指向,而其子节点又可能由多个不同层次的结点指向,难以明确的分清哪些是共享的部分,哪些是独立的部分,对这类具有内共享的结构的推理验证是未来研究需要努力的方向。山国武技论文在丝参考文献[10S.Ishtiaq and P.OHcarn. BI as an assertion language for mutable data structurcs In 28th POPL, pages