抽象图变换：状态的图形表示及模型检测应用程序的抽象技术

理论计算机科学电子笔记157（2006）39-59www.elsevier.com/locate/entcs抽象图变换阿伦德·伦辛克特文特大学计算机科学系rensink@cs.utwente.nl迪诺·迪斯特法诺伦敦玛丽皇后大学计算机科学系ddino@dcs.qmul.ac.uk摘要图可以用作操作语义和模型检查中的系统状态的表示;在后一种情况下，它们正在被研究作为位向量的替代。相应的转换是从图的产生式规则中推导出来的在本文中，我们提出了一个抽象技术在这个框架中：状态图是通过收集节点是succiently相似的（导致更小的状态和有限的状态空间）和图形生产规则的应用程序被提升到这个抽象的水平。由于图形抽象和规则应用程序都可以完全自动计算，我们相信，这可以是一个实际可行的软件模型检查技术的核心保留字：图变换、抽象解释、模型检测、验证1引言我们研究基于状态的系统行为模型，特别是软件系统。我们的最终目标是开发工具，以支持通过这些模型对软件进行验证。对于基本的建模形式主义，我们依赖于图变换，这是一个具有丰富基础理论的长期研究领域（参见，例如，[23]为一个概述）。在许多领域和不同设计细节水平上的系统自然地适合于行为规范，其中状态由图（具有有限字母表上的有向标记边）建模，并且转换对应于图变换规则的应用。我们在[20]中提出了一些关于1571-0661 © 2006 Elsevier B. V.在CC BY-NC-ND许可下开放访问。doi：10.1016/j.entcs.2006.01.02240A. Rensink，D.Distefano/Electronic Notes in Theoretical Computer Science 157（2006）39在此设置中应用模型检查技术。图变换的使用在这里是值得的，因为该理论所隐含的独立性和合成性的概念可以立即用于解决状态空间爆炸的问题模型检查中一个强大的概念是状态抽象。人们普遍认为，某种抽象，无论是通过切片，绑定，谓词抽象，对称识别或这些的组合，是必不可少的软件模型检查，以保持状态空间大小的控制。在[8，7]中，我们研究了一种设置中的模型检查，其中状态是图的受限类（分别是多集和单链表）的抽象，其中具有非常相似结构的节点被组合。在目前的文件中，我们结合这两股的研究，通过扩展的抽象一般的图形和解除图形变换的理论所产生的抽象图形。从技术上讲，我们将图的抽象建立在[16]中的先前工作的基础上;当前论文的贡献是将图变换提升到这个水平。应该注意的是，这种抽象已经在抽象解释的上下文中，即在形状图的理论中进行了研究，以获得很大的效果;例如，由Sagiv，Reps，Wilhelm和其他人在[24，25，12，22]。因此，我们有充分的理由相信，这将在我们的基于图变换的模型检查设置中产生同样有效的验证方法Approach. 任何一组图转换规则，应用于一个具体的开始图，都会产生一个（可能无限的）具体的转换系统。在本文中，我们定义了相同规则的应用，但现在是图形抽象- 在上面引用的工作之后，我们称之为形状-以这种方式，所有具体状态之间的转换（具体图形的转换）都会引起抽象状态之间的转换（形状的转换）。因此，我们对具体的过渡系统有一个过度近似，在此基础上，我们可以对实际系统的行为作出某些预测此外，对于每一个抽象转换，至少有一个潜在的具体转换，这意味着我们没有虚假的抽象转换。我们将使用一个循环缓冲器来存储数据值。缓冲器由一个由C-节点和一个中心B-节点组成的n-链接的环形结构组成，该节点通过f-和l-边指向（当前）第一个和最后一个单元。一个单元可以包含一个对象，由一个到O节点的v边建模，也可以是空的，由一个回到B节点的e边建模图图1显示了一个四个单元格的缓冲器示例，其中两个单元格是空的。这个缓冲器的形状结合了（结构上类似的）空C节点和O节点，并且另外A. Rensink，D.Distefano/Electronic Notes in Theoretical Computer Science 157（2006）3941图O=对象B=缓 冲 区 C=单元格形状F=第一个L=末n=下一个v=值e=空⟨put⟩Fig. 1. 四个单元格的圆形缓冲器示例，其形状和两个产生式规则指定节点和传入边上的多重性。1在O节点的输入边上，例如，表示每个具体的O实例都有一个传入的v边，它可以来自任何一个C节点。为了转换这个示例图，图。1还显示了两个规则，每个图由两个图组成：左手边（LHS）和右手边侧（RHS）。这些规则描述了对象的插入和删除，其中为简单起见，建模对象的节点实际上在插入时创建，在删除时删除。规则的效果是相对于LHS的匹配来定义的，LHS是到宿主图中的内射图态射。随后从主图中移除不在RHS中的那些元素的图像，而添加RHS中的新给定一个初始图和一组产生式规则，我们通过递归地将所有规则应用于所有图来获得一个例如，图2示出了用于图1中的图和规则的转换系统。我们建议使用这样的过渡系统作为模型检验的基础;第一个结果在[20]中报告然而，为了使这种技术变得实际可行，我们需要解决以下问题（除其他外）：• 模型在数据结构的大小上应该是通用的事实上，对于我们的例子，如果我们从5单元缓冲器开始，我们会得到一个不同的模型。• 模型应该是有限的。事实上，如果我们在例子中加入一条规则，当一个圆形缓冲器完全满了时，可以向它添加一个单元格，那么图的大小就变得无界，状态空间就变得无限了。通过将图转换提升到形状的级别，我们实现了这两个目标。事实上，我们所实现的是一种完全自动的状态技术，[1]在本文中，我们假设图是确定性的（定义如下），这意味着不需要输出多重性。我们把边的多重性写在箭头的另一端，而不是通常在类图中。CLBCnOn veCBLC=1个=1个C=1v>1O=1个Fnvn=1个e>1l=1 CB=1个=1个>1个C=1nvCOnFnCeBeCLCvnnO⟨get⟩vC OFBnCCeBnFC42A. Rensink，D.Distefano/Electronic Notes in Theoretical Computer Science 157（2006）39图二. 圆形浇注机抽象，在模型本身是动态的设置中-也就是说，节点和边可以在运行时创建和删除我们相信这是软件验证的一个有前途的基础，是对现有模型检查技术的补充。抽象的状态将是规范的形状，这是一个满足一些规范化约束的子类。他们的转变是一个三步走的过程。物化。 这涉及到识别应用规则的子形状（使用匹配），并提取它的显式、具体副本。这是准确模拟变换结果所必需的。同样的原理可以在[24]中找到，从那里我们采取了术语转型物化形状的变换很像普通的图形变换。我们将表明，这种类型的transformation保持和rechects相应的实例图的变换。正常化。转换的结果，虽然仍然是一个抽象图，但通常在规范形状的子类之外因此，我们必须按摩它以使其回到该类中。这可能会引入额外的非确定性：任意形状通常会产生多个规范形状。论文的结构。在第2节中，我们定义了图和图变换的基本概念，我们回顾了[16]中定义的抽象。具体化，转换和规范化步骤在第3- 5节中描述;在第4节中描述6、将它们结合起来，完成框架。最后，第7节总结了本文并讨论了相关工作。理论的证明在完整的报告版本中给出，[19]。2定义图及其变换。在本节中，我们定义了我们将使用的基本图形形式。在下文中，L表示一个固定的、有限的标签集。定义2.1（图和态射）L上的图是元组G=CnFenlBvC OnFLvCOvCOOvCOnnnn nnFFvnFCeCnCenBeCCeBLeeCvC BLCvCLBCnneeevnnnnnCCCOOvCOnOvCO⟨get⟩⟨get⟩⟨get⟩⟨get⟩⟨put⟩⟨put⟩⟨put⟩⟨put⟩A. Rensink，D.Distefano/Electronic Notes in Theoretical Computer Science 157（2006）3943其中N是节点的集合，E <$N ×L× N是标记边的集合。G称为确定的，如果（v，a，w），（v，a，WJ）∈ E蕴涵w = WJ.若G =<$NG，EG<$和H =<$NH，EH<$是L上的图，则态射φ：G→H是一个函数φ：NG→ NH，通过φ（（v，a，w））=（φ（v），a，φ（w））推广到E G，使得φ（EG）<$EH.图中给出了一个示例确定性图1.一、注意，节点标签（B、C等）实际上不是正式定义的一部分;事实上，它们是超级复杂的（它们可以从边标签中导出），我们只是为了可读性而包含它们。在下文中，GraL表示图类，DGraL表示确定图类。 给定一条边e=（v，a，w）∈E，我们称v为e的源，a为e的标签，w为e的目标。它们分别表示为src（e）、lab（e）和tgt（e）一个双射态射φ：G→H称为同构，G和H如果两个环是同构的，则它们是同构的（denotedG=H）他们在下面的定义中，我们建设性地提出了产生式规则及其应用，而不是标准的代数特征[3]。图产生式规则是一对图P =（L，R），其中L，R∈DGraL，分别称为左手边（LHS）和右手边（RHS）。有时我们也把P本身看作由并集L <$R给出的一个图，我们区分了以下集合：• Ndel=NL\NR和Edel=EL\ER，要删除的元素• Nuse=NL<$NR和Euse=EL<$ER，使用的元素（但未更改）;• Nnew= NR\NL和Enew= ER\EL，要创建的元素。图中给出了两个示例产生式规则1.一、L上的产生式规则集记为ProdL。 将产生式规则P=（L，R）应用于图G需要找到一个匹配m：L→G，它是从LHS到图的单射态射（也满足下面介绍的一些其他条件），然后从G中删除Ndel和Edel的图像，并将Nnew和Enew中的元素添加到结果图中。然而，必须注意确保新元素不与G中已有的元素重合。为此目的，当讨论规则P对图G的应用时，我们总是假设P和G是不相交的，即， NPNG= N。这假设可以通过取P的同构副本而不失一般性地得到满足（并且变换的结果不取决于我们取哪个同构副本，模同构）。定义2.3（图变换）设P= （左、右） ∈ProdL，44A. Rensink，D.Distefano/Electronic Notes in Theoretical Computer Science 157（2006）39G∈GraL是不相交的. P在G中的一个匹配是一个内射m：L→G，使得对于所有e∈EG，下列条件成立：(i) 若src（e）∈m（Ndel）或tgt（e）∈m（Ndel），则e∈m（Edel）;(ii) 如果src（e） ∈m（Nuse）和n（m−1（src（e）），lab（e），w）∈Enew，则e∈m（Edel）。如果m是P 在G中的匹配 ，则G根据 P和m 的变换定 义为（（ NG\m（Ndel））<$Nnew，（EG\m（Edel））<$Enew）。记G−−P，−m→H，证明m是P在G中的匹配，H是最小变换图.应用条件1被称为悬挂边条件;它是图变换的所谓双推出方法中的标准（参见图变换的双推出方法）[3]）。条件2可以称为决定论的保留;它是确保转换保留在DGra中的最直接的方法（参见第7节的简要讨论）。示例转换（没有匹配）如图所示。二、Pro position2.4LetP∈ProdL，G∈DGr aL. IfG−−P，−m→HthenH∈德格拉湖多样性和形状。 重数是自然数的区间。从形式上讲，我们 定义 的设置 的 多重性 作为 M={（i，j）∈ N ×（N <${*}）|i ≤ j}，其中 * 用于表示无穷（即，i*<对于所有i∈N）。 我们用μ来表示多重性的范围。 我们写=ifor（i，i），对于（i +1，*）> i，对于（i，*）≥ i。 重数μ ∈ M的下界记为dy[μ]，上界记为dperbound[μ|;thus[（i，j）]=i和[（i，j）]|=j。如果[ μ]> 0，则乘法μ称为p位。 如果[μm≤i≤[ μ m]，则W ∈ i ∈μ|在此基础上，我们将包含μ1<$μ2定义为<$i：i∈μ1<$i∈μ2。给定集合X具有重数μ，记为X：μ，如果|X|∈ μ。下面定义了两个重数上的运算，其中μ，μ1，μ2∈M，i∈N（注意，*−i=*+i=* for alli∈N）：μ1+ μ2=（[μ1]+[μ2]，[μ1|+[μ2|）μ− i =（max（0，[μ− i），[μ| − i）如果[μ| ≥ i.下面表达了这些不同概念的一些代数性质命题2.5设μ∈ M，A，B是任意有限集。(i) 如果A：μ，则（A\B）：μ−|A∩ B|.(ii) 如果i ≤ [μ|则（μ − i）+=i <$μ。多样性被用作定义形状的基本成分。在这些图中，多重性与每个节点相关联，说明它代表多少个具体节点，并且与每对节点v和标签a相关联，说明A. Rensink，D.Distefano/Electronic Notes in Theoretical Computer Science 157（2006）3945每个v的实例有多少条传入的a边形式上：定义2.6（形状）形状是一个元组S=<$N，E，nd，inn，其中<$N，E<$∈GraL（有时用GS表示），以及• nd：N→M是节点重数函数;• 在：N→L→M中，是一个引入的边重数函数。如果以下属性成立，则S被称为确定性的：• 对于所有v ∈ N使得nd（v）== 1且所有a ∈ L，|{w|（v，a，w）∈E}|≤ 1和|{w|（w，a，v）∈E}|≤[i n（v）（a）]|.一个确定性形状的例子如图所示1.一、我们使用ShaL表示L上的形状类，DShaL表示确定性形状。每个形状代表许多实例，这些实例是具体的（确定性的）图。在这个意义上，形状与类型图相当;然而，多重性对实例的结构提供了更多的控制形状和它的实例之间的关系由下面的塑造概念定义。定义2.7（整形）给定一个图G∈DGraL和一个形状S∈ShaL，G到S的成形是态射s：G→GS使得：(i) 对所有v∈NS，s−1（v）：nd（v）;(ii) 对于a llv∈NG和a∈L，{w∈NG|（w，a，v）∈EG}：i n（s（v））（a）;(iii) 对任意v∈NG，a∈ L，若<$（s（v），a，w）∈ES，则<$（v，a，WJ）∈EG.我们写s：G→S来表示s是G到S的成形。重要的是要注意，由于多重性约束之间可能存在不一致性，并非所有形状都有实例。如果一个形状允许实例，我们称之为相容的。在[16]中，我们证明了对于任意（有限）S∈ShaL，相容性的概念是可判定的。一个图通常具有（成形为）许多形状;例如，通过将形状的多重性改变为更允许的形状（即，所有的一切，都是为了保存。事实上，形状通过所谓的抽象态射相互关联。定义2.8（抽象态射）设S，T∈ShaL. 一个从S到T的抽象态射α（记作α：S→T）是一个态射α：GS→GT，其中：(i)对所有v∈NT，ndTΣ(v) 德S（α−1（v））;(ii) 对所有v∈NS和a∈ L，在T（α（v））（a）中∈S（v）（a）。(iii) 对所有v∈NS和a∈ L，<$（α（v），a，w）∈ET蕴涵<$（v，a，WJ）∈ES.46A. Rensink，D.Distefano/Electronic Notes in Theoretical Computer Science 157（2006）39下面的命题陈述了（正如预期的那样）任何形状的instance也是一个更抽象形状的instance命题2.9设G∈DGraL，S，T∈ShaL.如果s：G→S是一个成形，α：S→T是一个抽象，那么αs是G到T的一个成形。3物化正如在引言中所讨论的，我们将提升图形生成规则在形状中的应用我们分两步做到这一点：首先，我们将形状具体化，然后我们将具体化的图转换为具体的图。物质化是相对于规则的LHS的预期匹配来完成的由于这样的匹配不是一个形状（LHS只是图的一个片段，因此形状中的基数约束不一定满足），我们必须首先定义它们是什么类型的对象定义3.1设L∈DGraL和S∈ShaL。 S中L的预成形p是图态射p：L→GS，具有节点和边基数的上界满足的附加性质;即，• 对于一个llv∈NS，|p−1（v）|≤[ndS（v）]|;• 对于a llv∈NG和a∈L，|{w∈NG|（w，a，v）∈EG}|≤[i nS（p（v））（a）|.如果以下附加属性成立，则预成型p被称为混凝土• 对所有v∈NL，ndS（p（v））== 1;• 对所有的（v，a，w）∈EL，（p（v），a，WJ）∈ES有WJ= p（w）.预成形将单射态射从图到图的概念扩展到图到形状的概念。具体性意味着态射只映射到在任何具体实例中唯一可识别的节点和边命题3.2设L，G∈DGraL，S∈ShaL.如果f：L→G是一个单射态射，s：G→S是一个整形，则s<$f是L到S的一个预整形。直觉是，预成形p：L→S的存在表明L可能是S的一个实例的片段。我们目前还没有一个结果来支持这种直觉;也就是说，我们不知道p的存在是否或何时意味着存在一个实例G，它具有（适当的）成形s：G→S和嵌入m：L→G，使得p=s<$m。然而，我们猜想[16]的结果可以很容易地推广，以便将这个性质（对于给定的L和S）简化为整数规划，从而给出一个决策过程。另一方面，对于混凝土预制件，我们有以下进一步的第三章：A. Rensink，D.Distefano/Electronic Notes in Theoretical Computer Science 157（2006）3947S=1个=1个>1个=1个=1个=>1个S+p=1个CvOC=1=1vn1OFnvFn=1个=1个vne>1B=1个=1αpn>e1B=0l =1FL= C1=C0>11l1==Bv=1个>1个C=1个=1个n>0个C=1 nenC=1 =1Cnp的idlCLLBneC图四、图中形状的具体化1个w.r.t. 阿格浦尔的LHS命题3.3设L∈DGraL，S∈ShaL，c：L→S是一个具体的预成形。对任意G∈DGraL，且有一个整形s：G→S，存在一个单射态射m：L→G使得c= s<$m。给定一个LHSL、一个形状S和一个预成形p：L→S，S相对于p的具体化定义为：将L的一个副本单独添加到S，必要时将其连接到S，并调整S的节点多重性以说明从中提取一个或多个实例W.l.o.g. 我们假设NL<$NS= N;我们定义一个函数αp：（NL<$NS）→NS，αp= p=S.αp像往常一样扩展到边。S相对于p的具体化定义为S+p=N+p，E+p，nd+p，in+p，其中N+p=NL<$NSE+p= α−1（ES）\{（v，a，w）|v∈NL，<$（v，a，wJ）∈EL：wJw}.pnd+p：v›→ndS（v）− |p−1（v）|如果v∈ NS=1，否则in+p：v<$→inS（αp（v））.图4中示出了实例具体化。首先要说明的是L、S和S+p之间的关系。(See也参见图5.）命题3.4设L∈DGraL，S∈ShaL，p：L→S是预成形.αp产生从S+p到S的抽象态射，而idL产生L到S+p的具体预成形，使得p = αp<$idL。CS你好，S、、、LmG图3：Prop的可视化。第3.3节48A. Rensink，D.Distefano/Electronic Notes in Theoretical Computer Science 157（2006）39S具体化满足以下特性（见图1）。（5）：-S，pαp+p我 是，LL MG图五、命题3.4和3.5的可视化命题3.5设L，G∈DGraL，S∈ShaL. 对任意的内射射m：L→G和成形s：G→S，设p = s<$m，则存在成形t：G→S+p，其中s = αp<$t，t<$m = idL.4转型在本节中，我们证明了我们定义的抽象的正确性，在这个意义上，形状相对于奇异预成形的变换模拟了底层实例图的变换，反之亦然。首先，我们扩展了变换的定义（见定义）。（2.3）形状。定义4.1（形状变换）设P =（L，R）∈ProdL且S∈ShaL不相交。P在S中的抽象匹配是对c：L→S的具体预成形，使得c：L→GS是P在S的图部分中的（具体）匹配.如果c是P在S中的抽象匹配，则S根据P和s的变换定义为T∈ShaL，使得NT=（NS\c（Ndel））<$NnewET=（ES\c（Edel））<$EnewndT（v）=，nd（v）如果v∈NS S在T（v）（a）中=我们得出S−P−→，c=1，否则⎧nS（v）（a）−|{w|（w，a，v）∈c（Edel）}|+ =|{w|（w，a，v）∈Enew}|如果v∈NS⎪⎩=|{w|（w，a，v）∈Enew}|在她方面T表示 c是 P在 S和 T中的抽象匹配是所得到的变换形状。以下是本文的两个关键定理，它们提供了抽象和具体转换之间的联系。S不A. Rensink，D.Distefano/Electronic Notes in Theoretical Computer Science 157（2006）3949定理m4.2LetP=（L，R）∈ProdL，S，T∈ShaL并假设S−P−→，cT。对于任何形状s：G→S，存在P在G中的匹配m，使得c= s→m，对于G−−P，−m→H，则是成形t：H→T。定理m4.3LetP=（L，R）∈ProdL，G∈DGr aL并假设G−−P，−m→H.F或任何形状s：G→S，使得c=sm是concrte，S-P-→，c成形t：H → T。5正常化T与a物化和变换是抽象图变换的两个基本组成部分然而，有效技术仍然缺少第三个要素：即，我们需要确定一个规范的抽象级别，在这个级别上只存在有限数量的形状，并且每个转换的目标图将被重新规范化。如果做不到这一点，由于物化，变换下的图将变得越来越大，越来越具体，因此状态空间仍然是有限的，抽象的优点也就丧失了。对于这个规范抽象层次，我们将依赖于[16]中提出的思想。对于所有的情况，我们都有一个基重数M={=0，=1，>1}的组合（以这样的方式选择，即每个有限集合恰好有一个基重数）。M>0=M\{=0}表示p个独立的基多重性的选择。接下来，我们定义以下相似性的概念：在形状S的节点上的相似性SNS×NS：(1)v1Sv2⇔inS（v1）= inS（v2）lab（src−1（v1））= lab（src−1（v2））。S S因此，如果两个节点具有相同的传入边多重性和传出边标签，则它们是相似的。定义5.1（正则形状）一个形状S∈ShaL被称为正则，如果(i) S是决定性的;(ii) 对任意v∈N，nd（v）∈M>0;(iii) 对所有（v，a，w）∈E，在（v）（a）∈M>0;(iv) 对所有v，w∈N，v<$Sw蕴涵v = w。换句话说，如果一个形状是确定性的，指定所有节点和边的正基重数（第2和3条），并且不包含非平凡相似节点（第4条），则该形状是规范的。[16]中的一个重要事实是，CShaL对于每个有限集合L都是有限的。我们使用正则这个术语，因为正如我们在[18]中所示，有一种自动的方法可以获得最具体的正则形状可以（G）。50A. Rensink，D.Distefano/Electronic Notes in Theoretical Computer Science 157（2006）39Σ给定确定图G.另一方面，对于一个任意形状S，典型地没有一个规范形状相反，我们定义一个函数范数，使得norm（S）是一组规范形状，在某种意义上是最优的（如下所示）。为了归一化多重性，我们取S中发生的多重性与M的所有（非空）交叉。它定义如下（其中μ∈M且f：X→M）：μ/M={μJ∈ M|i：i ∈ μf/M={g：X→M|<$x∈X：g（x）∈f（x）/M}。函数范数：ShaL→2CShaL isthendefinedasfollows：norm：S›→ {part（T）|T∈DShaL，T a S，T consistent}.其中，性质T a S被定义为以下条件的合取NT{（v，f）|v∈NS，f∈i nS（v）/M}ET{（（v，f），a，（w，g））|（v，a，w）∈ES，g（a）=0}结束T∈ {h：NT→M>0|n ∈ NS：ndΣS（v）<$（v，f）∈NTh（（v，f））}在T={（（v，f），f）|（v，f）∈ NT}而part（S）=T的定义为：NT=NS/SET={（[v]<$S，a，[w]<$S）|（v，a，w）∈ES}[001pdf 1st-31files][001 pdf1st-31files][001pdf1st-31files]v/S w和S（w））/M）|v ∈ NS}i nT={（[v]S，i nS（v））|v∈NS}T a S意味着T本质上是通过将归一化的输入边重数和正归一化节点重数分配给S的节点而从S获得的。这可能会导致S节点消失（如果它们的多重性=0）或被分裂（如果存在输入边多重性的选择T上的条件确保它满足定义5.1的第2和第3条。另一方面，部分（S）组合了S-相似节点，因此确保了定义的第4条，前提是S已经满足第4条。1-3.一个例子可以在图中找到图6示出了通过使用图4中的物化来变换S而获得的形状的归一化。该归一化包含四个形状，其中两个（在右手侧）包含由一个或多个n-连接的C-节点组成的子结构，所述n-连接的C -节点与缓冲器的其余部分断开。这样的结构并不对具体层次上发生的任何图进行建模;它是由A. Rensink，D.Distefano/Electronic Notes in Theoretical Computer Science 157（2006）3951−−−−−−→GG=1个=C1=>1个O=1个=1个=1>1O=1个vn1不=Cv1Fn=零=l=11vn=>1Be=0FC>0=1个B=1个vn=Cn=1个1BF=1v=1个LCven>0个C==1Cn1范数1=-=1 1=1Nn>=1个=1个CvL1n=1个C=1个1O=1=1个=C=1>1O1v=1个=C=1个1=1>O1=1个C=1个v>1个OFn=1v=1个v=1个>=1个1Bnf=1vFn=1个nn=e=1个1Bl=1个Cn==1个Cvn>1Be=1个Lv>1e=1个C=1个=1个CC=v1L=1个n=1个Cn=1个v=C11=1个C=1=1个n>1个C=1个=1n见图6。用S+p（put_p，id_L）对形状T进行归一化T（其中S和P如图所示）。四、抽象任意确定性图的标准形状通过映射can定义：DGraL→CShaL，定义为（2）can：G›→part（Sinst）其中Sinst=（NG，EG，nd，in）是G的nd将=1赋给所有节点v∈N，并且in（v）（a）=μ是M中的唯一重数，使得（tgt−1（v）<$lab−1（a））：μ。例如，图中的形状1G G是图中图的下一个图像。 以下结果”[18]《明史》卷18。定理5.2对任意的G∈DGraL，可以（G）∈CShaL，且θs：G→can（G）.定理5.3对任意S∈ShaL，范数（S）={can（G）|S：G→ S}。6过渡在本节中，我们通过定义具体（图形）转换系统和抽象（形状）转换系统并说明它们之间的关系，将上述结果汇总在一起定义6.1（转换系统）设A是一组产生式规则。• 一个图的变换是一个三元组G−→PH，其中G，H∈DGraL且P∈DGrathatG−−P，−m→Hforsomem. 一个图的传递系统是一个二重（G，→−）当re→−是graphtransionrelaxion且GDGraL在52A. Rensink，D.Distefano/Electronic Notes in Theoretical Computer Science 157（2006）39−−−→→−（即，G∈G且G−→PH蕴涵H∈ G）。• 一个hpetransition是一个三重S−→PT，其中hS，T∈CshaL且P=（L，R）∈证明了S+p是一致的，S+pP，idLSJ和T∈can（SJ），其中p-整形p：L→S。一个Shpetransition系统是一个tuple（S，→−），其中re→−是随机变量，S是L在→−下的随机变量。给定一组产生式规则和一个图G∈DGra，我们对于包含G的最小图迁移系统记为GTS（G，G）;同样，给定S∈CShaL，我们对于包含S的最小形状迁移系统记为STS（S，S）。例如，图2示出了图转换系统GTS（G，G），其中G={Put，Put，G}并且G是图1的图。图7显示了STS（n，can（G）），其中我们使用了一些符号约定来表示多重性：细箭头和节点是单数（节点/传入边多重性=1），而胖箭头是多重的（>1）。图中的箭头7表示反向应用;对于每个箭头，在相反方向上存在隐含的反向较暗（阴影）的区域是状态空间的片段，它实际上是具体转换系统的图像我们现在得出主要的结果，它指出由can定义的抽象是有限的和保守的，并且在弱意义上不过度近似。定理6.2设G是产生式规则集，I∈DGra，GTS（G，→−），STS（G，can（I））=（S，→−）。(i) 可以（G）≠S，且S是有限的;(ii) 对于G，H∈G，G−→PH蕴涵can（G）−→Pcan（H）.(iii) 对于所有S，T∈S使得S−→PT，存在GJ，HJ∈DGra，使得S=can（GJ）且GJ−→PHJ.这个定理意味着我们可以验证安全性质，其中命题是一阶逻辑片段中的图谓词，这是由我们的抽象所反映的-在[16]中被表征为2变量逻辑的片段。这些属性的典型示例是状态不变量，例如：• 缓冲器或者是空的（即，从第一个可到达的单元格不包含对象），或者第一个单元格包含对象;• 如果缓冲器为空，则最后一个单元格是第一个单元格的前趋单元格;• 如果一个单元格包含一个对象，那么它的最后一个或下一个单元格也包含一个对象。无法验证的有效属性示例，即， 在抽象层面上似乎被违反，但实际上在具体系统中是真实的（所谓的• 环形电池的所有电池连接;nFnCeeeFFCvOnfvCvOnFnvCOnefevCOnFe nvCOefe nvC BCOne nveC BCvOCvOnCeBCCe BCLC BLeCeC BLeCLeCCnLeCC nnFnCeBnl vCnfnCeBnL vCnLvnCnvnCCvnnCnCnnnOCvOnnCnnefeCvOn nFCvOnf vCvOnnf vf vCeBCnLnvf vCe BCnlnvCBCeBBCCeBCc CLenlvnCCnlnvCnLnvCCvOnvFnCvOCn vCvOCvOCvOnnCvOnvCeBCnflvln CBn C Oef n nCBfLLeCBn nFCeBnnf vCeBCf vCeBCLnvFnCeBCLnnCv恩恩ne nCC ClvlnvnCnCnCv v vnCvV VCvOnvFCvOnvFL无无无无无无无efe feCnOnf vnCnOf vCnOf vnCnOf vCOnnvC BFnCeBCn nC B C BLeleCeBCCeBCBCCe BCLCeBCnCvnCnCnlnvCnLnvCnlnvCnLnvCnLvnCLegendaCC单节点/入边多节点/入边CvOn vCvOn vC OC OnFen v nnC OC O图形状态转换前后：<按箭头方向 in reverse direction转换系统的正确片段（余数是过近似）FnCeBCnLvnCFnCe BCnlvnCeC BLeCnnCefevC BLeCnC nne nveC BLeCCnnne nveC BLeCCnnA. Rensink，D.Distefano/Electronic Notes in Theoretical Computer Science 157（2006）3953见图7。 抽象布尔转换系统nnCn54A. Rensink，D.Distefano/Electronic Notes in Theoretical Computer Science 157（2006）3931PCE L Ca H2PCE L Ca H4 L CHPC一En5 L CPCE一HnPCE3a LHBLhPCE4a LHBLhPCE5b L CHn不PCE1b L CHnLLine 1（while guard）R LLine 4：a.head：= a.head.nextRL第2行：单元格tmp：= b.headR L第5行：B.head.next：= tmp（case 1）R2PCE L B H3PC不E L B HPCE5b L CHn不1b LC pcnEHL第3行：b.head：= a.headR L第5行：B.head.next：= tmp（case 2）RE =环境，L =列表，C =单元格，N = nil，h =头，n =下一个，t = tmp图8.第八条。 列表反转程序的小步转换规则• 只有当执行的次数也是有限的时候，执行的次数才是有限的;• 对象将按插入顺序删除列表反转。为了更好地与现有方法进行比较，本节的其余部分将专门介绍一个在堆结构分析中多次使用的示例[24、21]。2该程序使用一个数据结构，ofList-通过头边指向1单元格-由下一条边连接的节点;存在唯一的2nil-node建模列表的末尾。图845显示了一个简单的，逐行的翻译6转化为图形转换规则。变量和场由边表示，它们的值由节点表示。有一个中央的、E标记的节点，它代表运行时环境，局部变量边被附加到该节点，并且该节点维护一个pc标记的第5行需要两个规则，以区分b.head.next已经等于tmp的情况（如果列表a最初只有一个元素，可能会发生这种情况）;这是因为我们的匹配需要是单射的（参见定义。2.2）。我们现在可以使用标准的图转换结果来将这些规则组合成[2]然而，请注意，我们提出这一点只是为了比较，而不是因为我们认为这种顺序程序分析是我们方法的优势; 在这里是优越的。这是Sect。7 .第一次会议。while（a.head！nil）doCell tmp：= b.head;b.head：= a.head;a.head：=a.head.next;b.head.next：= tmp;odA. Rensink，D.Distefano/Electronic Notes in Theoretical Computer Science 157（2006）3955SaMBLHCnCnLhNS2aMBn nL HCCS3aMBn nL HCCS4aMBL HCnCS5aMBL HCnnCnLhNLhNLhNLhNS6aMBnLhCCnS7aMBL CHnnCLHNLhNL单>R L交换>R一EBLHnCHNL一EBLhCnLhE =环境，L =列表，C =单元格，N =无，h =头，n =下一个见图9。 列表反转程序的大步长规则。见图10。 列表反转程序的抽象转换系统。身体两个结果规则如图9所示（省略了程序计数器，它现在总是等于1）。我们在图中显示10.由大步长规则swap生成的完整转换系统（从所选的开始状态起，从不启用single过渡系统比我们从小步规则中得到的系统要小（参见，例如，[24]）：图变换理论在这里已经付出了代价变迁系统的可能运行都终止于S7，它表示颠倒的列表，现在由b指向，而a是空的。在转换系统中可以验证的一个示例属性是，两个列表总是保持分离：没有Cell节点被共享。7结论我们已经提出了一种技术，用于操作语义的有限抽象模型的按钮构造，基于由一组图转换规则组成的图产生系统。正如在引言中所指出的，相对于以前的工作的贡献是，本文工作的转换本身和随之而来的抽象过渡系统（第4和第6节）：形状模型之前提出。鉴于这一事实，正如其他地方所争论的那样（见，例如，[2，6，9，13]），图变换是一个非常适合的形式主义建模的软件系统的行为，特别是在面对动态演化，本文的结果形成一个56A. Rensink，D.Distefano/Electronic Notes in