可在www.sciencedirect.com在线获取理论计算机科学电子笔记334（2018）17-29www.elsevier.com/locate/entcs模糊集抽象Jacob Lidman和Josef Svenningsson1计算机科学与工程，查尔姆斯理工大学，瑞典摘要程序分析在改进现代软件中起着关键作用静态（声音）分析产生全局正确的结果，但通常是悲观的结果，而动态（完整）分析产生高度精确的结果，但覆盖面有限我们提出了模糊集抽象，推广以前的工作的基础上3值逻辑。我们的抽象允许混合分析，其中静态结果通过使用模糊控制系统动态地细化。关键词：抽象解释，静态程序分析，动态程序分析1引言静态分析和动态分析是互补的。静态分析是合理的，因为它总结了所有可能的执行，而动态分析提供了更精确的信息，因为它总结了实际发生的执行静力分析中的过度近似有时是依赖结果的应用的严重问题。静态别名分析通常会产生比动态别名分析大几倍的指向集[8]，[9]，并且在扩展中会抑制sev-to。并行化的机会能够结合这两种分析可以大大改善结果，例如在非功能性验证中（例如，当使用关于输入状态/环境的悲观假设时，推导编译器优化的最坏情况收益）。在这种情况下，在编译时，良好的结果是有趣的，这样就不会应用保证有害的优化。相比之下，完整的结果在运行时是有趣的，因为实际的输入集是已知的，因此可以准确地评估优化的好处。模糊数据流框架[5]展示了基于模糊逻辑的程序分析如何揭示1电子邮件：lidman@chalmers.se，josefs@chalmers.sehttps://doi.org/10.1016/j.entcs.2018.03.0031571-0661/© 2018作者。出版社：Elsevier B.V.这是一篇基于CC BY-NC-ND许可证的开放获取文章（http://creativecommons.org/licenses/by-nc-nd/4.0/）。18J. Lidman，J.Svenningsson/Electronic Notes in Theoretical Computer Science 334（2018）17这是经典框架无法实现的优化机会。对多值模糊逻辑的推广在一定程度上允许程序性质为真或假真值是单位间隔2的元素，并且表示程序属性的偏差。例如，结果为0。1875将指示该属性倾向于假，因为它更接近0（假）而不是1（真）。然而，在程序分析中使用模糊逻辑所带来的表达能力的增加，促使人们对分析框架的属性进行更多的研究，特别是合理性和完整性。我们引入了模糊集抽象，它推广了三值逻辑抽象[10]。我们提出了模糊集抽象的理论基础，并证明了静态分析的可靠性（第3.1节）。我们还提出了一个动态分析（第3.2节），我们使用自适应模糊推理系统从模糊控制理论，逐步专业化的分析结果，以提高精度。2预赛本文简要介绍了模糊集的几个概念。我们的静态分析使用谓词变换器来操纵模糊集，用模糊逻辑（2.1节）和可能性理论（2.2节）激励的收集器函数来类似地，我们的动态分析从静态分析的结果开始，并迭代地专门化它以提高我们的结果的准确性。这个过程依赖于模糊分类器（2.3节）。2.1模糊集合与逻辑模糊集为每个元素分配部分成员资格，这与成员资格是二进制的经典集相反。本文利用公共点序关系将两个模糊集：μ A ≤ μB，μ A（s）≤μ B（s）联系起来。定义2.1设S是一组元素，μS是隶属函数，它从单位区间[0， 1]中为每个元素分配一个隶属值然后μS是一个模糊集。单点集上的模糊集可以被认为是部分真值的描述。模糊逻辑定义了逻辑连接词来操纵这样的模糊集。在这里，复合词通常被定义为否定（即， 1 −x），而在Min-max模糊逻辑中，最大运算用于析取运算，最小运算用于合取运算。定义2.2模糊逻辑这是一个很好的例子，它满足了德摩根的要求。和两个二元函数[0，1] 2→ [0，1]，它们是可交换的、结合的和单调的递减/递增的，并且具有一个单调的元素nts（x_n_1=x和x_n_0=x）。类似地，<$是一个一元函数<$：[0，1]→[0，1]，它是递减的，在v中（即，并且满足边界条件<$k（0）=1和<$k（1）=0 3。THE2为了保证终止性，我们使用单位区间的有限同余集3在模糊逻辑文献中，合取算子被称为三角范数（T-范数），析取算子被称为三角合取（S-范数），并补充了C-范数。J. Lidman，J.Svenningsson/Electronic Notes in Theoretical Computer Science 334（2018）1719∈−−.Σ⎧⎪⎨逻辑连接词被逐点提升用于元素的非单例集合2.2可能性理论可能性理论是一个非经典的理论推理的不确定性概率是自对偶的，即P（x）= 1−P（x），而可能性N与必然性N对偶相关，即N（x）= 1N（x）。在这两个度量的基础上是一个可能性分布π，它编码了关于宇宙Ω的部分知识：2Ω，π（x）= 1意味着x是完全可能的，π（x）= 0意味着x被拒绝为不可能的。定义2.3可能性和必要性测度分别定义为：n（X）=supu∈Xπ（u）和N（X）=infu/∈X 1−π（u），其中π：2Ω→ [0， 1]是一个可能性分布，给定一个具有可测子集的论域Ω，满足：• π（π）=0• π（Ω）= 1• 对于任何一个两两不相交的子集Ui<$Ω的集合Ui：π（iUi）= supiπ（Ui）虽然与概率论平行的概念（例如，独立性，条件- ing）可以定义为可能性理论[2]，我们将注意力限制在分布之间的偏序上。信息顺序通过将度量与其否定进行比较来基于它们的信息内容对分布进行排序（即， （x）=1 −或N（x）= 1N（x））。 当它等于它的否定时，该测度提供最少的信息量，即，（x）=（x）= 0。5. 我们定义一个半格5[0，1]，≤ H，H在一组同构于单位区间（即[0，1] = 2 Ω）的事件上，使得x≤ Hy意味着P（x）比P（y）更具信息性：0。100。50。91x±Hy=max（x，y）x，y ≤ 0. 5min（x，y）x，y ≥ 0. 5000. 5其他从概念上讲，连接操作返回两个输入的一致性，即两个输入中信息量最少的一个，或者如果它们是冲突的，则返回中间立场（0.5）（一个输入是< 0。5和onei> 0。5）。信息序用于第二节的静态分析3.1合并来自不同控制路径的结果并形式化具体化函数。2.3基于Takagi-Sugeno自适应网络的模糊推理系统（TS-ANFIS）TS-ANFIS在模糊IF-THEN规则系统中实现分类推理。每一条规则都由前因和后因组成。前件由分类器的每个输入变量的模糊集组成，后件是将输入变量映射到输出域的多项式。图1中显示了一个两个规则的示例分类器，用于两个输入变量x0和x1，其中4可能性测度是Dempster-Shafer理论[2]中可能性函数的特殊情况，Dempster-Shafer理论[ 2 ]是贝叶斯概率论5使用对偶定理，这个并半格的逆序是交半格，在我们的情况下，元素将对应于N（x）的测度，因为n（x）=1 − N（x）。20J. Lidman，J.Svenningsson/Electronic Notes in Theoretical Computer Science 334（2018）17a0级x0x1的1w1N第1页w1f1b0的w2Nw'Σ2wf2 2B1x0x1下面给出的功能w1+w20。60。60。6如果x0是A0且x1是B0，则f=c（1，0）+c（1，1）x0+c（1，2）x1例如，x=0的分类。六，零。其中f1（x） =如果x0是A1且x1是B1，则f=c（2，0）+c（2，1）x0+c（2，2）x1 0。2×0-0。43x1和f2（x） =0。1×1+0。5、成员资格μA0μB0x00.6每个规则的触发强度由下式给出：w1=0。六点零。5 =0。5fμA1μB1w2=0. 286美元。1 =0。1X1x0x1分类器的输出为：f= 0。5 f1（x）+0。1 f2（x）0。60。073== 0。1220。6Fig. 1.双规则双变量对于第一（二）规则，前件部分的模糊集分别称为A0（A1）和B0（B1），类似地，后件部分的多项式的系数记为c1，i（c2，i）.分类器由五层组成前三层查找输入向量的模糊隶属度，并计算该集合的归一化模糊合取，产生规则的归一化触发强度，即。规则的模糊隶属度或权重 在该示例中，输入向量的模糊隶属度为μ A0（x0）= 0。6和μ B0（x1）= 0。5. 最小-最大模糊逻辑的模糊合取估计为w1= min（0. 五，零。6）= 0. 5,类似地，w2= 0。1，因此归一化权重为w1= w1= 0。五、的下一层用归一化的射击强度对结果输出fi（x）进行加权最后一层对每个加权规则分类进行求和。 返回到例子，我们得到f1（x）= 0。034和f2（x）= 0。56因此，分类器的输出为0。50. 034 +0。10. 56= 0。122. 由于结果部分是多项式，并且可以使用统计回归/自适应滤波算法（例如最小均方（LMS））在线改进分类当我们可以保证第3.2节中的动态分析的收敛性时，我们使用TS-ANFIS和LMS。3模糊集合抽象程序分析关于分析的个体的动态（例如，存储器存储、冗余表达式）相对于一组属性的原因。Sagiv等人的三值逻辑分析。[10]使用逻辑谓词来声明个人何时拥有属性，并使用逻辑公式来建模语句如何更新谓词。他们的框架依赖于具有传递闭包和双格理论的一阶3值Kleene逻辑[4]，其中推理值根据信息顺序和真值顺序进行排序。该框架至关重要的是，能够将潜在无限数量的个体和具体语义中的解释上的谓词总结为有限的、易处理的程序分析。我们对提高分析的精度和纳入动态信息的兴趣使我们考虑个人在一定程度上可以拥有属性的分析。为此，我们使用一个家庭的模糊逻辑。模糊逻辑的最简单形式之一是Kleene的三值逻辑，Sagiv et al.[10]我们通过将最小-最大模糊逻辑限制为三个来获得0.50.10.286J. Lidman，J.Svenningsson/Electronic Notes in Theoretical Computer Science 334（2018）1721.ΣS2.Σ2价值观因此，我们将使用他们的程序分析框架作为我们自己的模糊集抽象的基础，这将在3.1节中描述。虽然在我们的框架中的分析是可判定的和声音的抽象描述，在最坏的情况下，可能是非常大的。因此，我们也考虑的情况下，得到的描述保持在最低限度。在这种近似分析产生一个单一的解释代表最大的解释。3.1静态分析类似于Sagiv et al. [10]我们从一组给定的谓词开始，一个词汇表，P={p1，...，p n}。程序语句定义了每个个体的每个属性的新状态，它被建模为谓词Transformer，即P上的一个逻辑公式，它把一个谓词转换成一个新的谓词。定义3.1设P是一个词汇表。程序语句是一组谓词转换器，每个谓词p∈ P对应一个。谓词Transformer由下面语法中的逻辑公式φ流图是一个边标号连通图G=V<${vstart}，E，C，其中vstart是唯一的入度为零的起始节点，节点v∈V是程序语句，边e∈E<$V×V表示两个顶点之间的控制转移，C将一条边映射到它的控制转移条件。φ|不|p（v1，.，（v k）|¬φ|φ∧φ|φ∨φ|v：φ|v：φ|TCv1，v2：φ具体语义定义了满足谓词Transformer的可能的2值逻辑结构的集合。公式的语义是以具有传递闭包的2值逻辑的标准方式定义的。定义3.2[Sagiv et al. [10]，def.3.2]让我们成为一个个体的宇宙，P=P1P2. 将一组一元、二元、. 克-阿尔河predicarectes.• 2-值解释是一个结构S=US，iS其中iS（p≠）是映射从US到真值（即，0或1），p<$∈ P<$。2-值解释的集合被表示为2-NCT[P]。• 赋值Z S是从变量到个体的映射，即Z：V ≤ →U. 如果Z是total，则赋值完成• 公式φ的自由变量是用标准方法定义的。如果free（φ）= φ，我们说φ是一个封闭公式。• 闭公式φ二值意义[[φ]]S（Z）与完全赋值Z产生一个真值，并在图2中归纳定义（左）• 如果[φ]]S（Z）= 1，则S和Z满足φ。 我们用S，Z表示|= φ或S|= φ if φ满足所有Z。语句根据预定义的传递函数更新（每个个体的）每个属性。因此，一个语句的语义应该生成新的谓词，这些谓词是根据它的前一个谓词定义3.3[Sagiv et al.[10]，def.3.3]设P = P1<$P2 <$. Pk是一个词汇22J. Lidman，J.Svenningsson/Electronic Notes in Theoretical Computer Science 334（2018）1722∧p2⎧2[0，1]q[0，1]q[0，1]q[0，1]q[0，1]q222[0，1]q22[0，1]q[0，1]qMaxu[0，n]∈U∨˜[0，n]∈U˜i=0[[φ]][0，1]qZ2x=1p2VS（vstart）v=vstart222[[]]S（Z）=0[[T]]S（Z）=1[[<$φ]]S（Z）=1−[[φ]]S（Z）S[0，1]qS[0，1]q[[<$φ]]S（Z）= 0。0（Z）= 1。0（Z）=<$。[[φ]]S（Z）[[p（v1，.， vk）]]S（Z） = iS（p）. Z（v1），.，Z（vk）2[[p（v1，.， vk）]]S（Z） =iS（p）. Z（v1），.，Z（vk）[0，1]q[[φ1 <$φ2]]S（Z） =min.[[φ1]]S（Z），[[φ2]]S（Z）[[φ1 <$φ2]]S（Z）=φ1。[[φ1]]S（Z），[[φ2]]S（Z）[[φ1 <$φ2]]S（Z） =max.[[φ1]]S（Z），[[φ2]]S（Z）[[φ1 <$φ2]]S（Z）=φ1。[[φ1]]S（Z），[[φ2]]S[[v：φ]]S（Z） =minu∈US[[φ]]S. Z[v<$→u][[v：φ]]S（Z） =[[φ]]Su∈US. Z[v<$→u]S（Z） =maxu∈US[[φ]]S. Z[v<$→u][[v：φ]]S（Z） =[[φ]]S. Z[v<$→u]2 2[[T Cv1，v2：φ]]S（Z） =[0，1]q[[T Cv1，v2：φ]]Su∈US（Z）=[0，1]q2n−1Sv1›→uiv2Σ⎞⎠[0，1]qn−1Su⎝⎛v1uiΣ⎞⎠Z（v1）=u0Z（v2）=unZ（v1） =u0Z（v2） =un图二.经典一阶传递闭包逻辑（左）和同余域[0， 1]q上的一阶传递闭包模糊逻辑（右）的语义定义一元二进制 k元谓词，设φw是自由变量的公式v1，.，v x在语句w处更新谓词p。给定一个结构S，我们将W后S的语义定义为：[[st（w）]]（S）=.US，kλp∈Pxλu1，.，λux. [[φw]]S（[v1≤ →u1，.， vx≤→ux]）2值语义定义了一个节点在入口上可能看到的（可能是无限的）逻辑结构集。收集语义后来被定义为2值语义的最小固定点。定义3.4令VS将v∈V映射到一组2值逻辑结构。图G= V，E，C的2值语义由下式给出：[[G]] 2（VS）=λv.⎪.[[st（w）]]（S）|S∈VS（w）andS|=C（w，v）否则Ew→v ∈E2[0，1]上的自然序具有无限高，因此包含无限链。在这样的域中的定点迭代可能不会终止.加宽运算符通过以有限步数遍历域来解决这个问题，例如通过域中的一系列跳跃，然后是顶部/底部元素。然而，很难控制由加宽算子引入的过逼近程度。而不是引入一个加宽算子，我们让我们的模糊抽象使用单位区间的有限同余域。为了用可表达性来换取易处理性，或者反之亦然，我们定义了[0， 1]上的一个同余域族上的抽象语义：q域，其中q∈N− { 0}。这[[]][[T]]2[0，1]q[0，1]qZ最小值[[φ]]i=0ui+1v2›→ui+1J. Lidman，J.Svenningsson/Electronic Notes in Theoretical Computer Science 334（2018）1723些域是线性排序的，使得在Rbq中的真值t被分成两个真值（不包括0）。5）在q+1中。我们在图3中示出了对于R1的全等关系（即，3-Sagiv等人使用的Kleene逻辑[10]），2002 年和2003 年。因此，在图2的浅灰色框中的值（即1/4、1/ 2和3/4）被映射到图1中的1/2，并且类似地，图3的深灰色框表示被映射到图2中的单个值的值集合。的同余24J. Lidman，J.Svenningsson/Electronic Notes in Theoretical Computer Science 334（2018）172Q2[0，1]q[0，1]q.- 是的Σ120β1-结构域（三值逻辑）β2-结构域β3-结构域图3.第三章。分次真值序的等价分割关系与第2节中介绍的信息顺序一致，即，当解释在一个SQREQ域中的SQREQ+1值时，该值从来没有更多的信息。定义3.5x∈[0，1]的q等价类，记为[x]q，定义为：将x四舍五入到最接近的1的倍数。所有n阶等价的集合类是[0，1]={x|x∈N q}其中N q=. X|x∈N <$0 ≤x≤2 <$.1Q2Q在第2节中，根据模糊逻辑定义了在Rbq上的抽象语义。这个定义使用了类似于具体语义的解释和赋值等概念，但其中的真值现在是[0，1] q的元素而不是{0，1}。定义3.6[Sagiv et al.[10]，def.4.2][0， 1]q-值解释和赋值类似于具体语义。• 给我一个模糊的逻辑。∧˜,∨˜,¬˜Σthefuzzyϵqmeaning[[φ]]S(Z)ofaclosed公式φ和完全赋值Z在[0， 1]q中产生真值，在图2中归纳定义（右）• 定义一个语句的语义（即，[st（w）]][0，1]q）类似于定义3.3中的具体情况，但公式在给定的模糊逻辑中解释。• 如果[φ]]S（Z）> 0，则S和Z潜在地满足φ。 我们用S，Z表示|=[0，1]Qφ或S| =[0，1]qφ，如果φ对所有Z都满足。嵌入是由Sagiv et al. [10]将2-值和3-值解释联系起来。非正式地，它们将符合信息顺序的逻辑结构联系起来。 嵌入聚类个体并决定其属性的值根据集群成员的相应值。重要的是，使信息损失最小化的嵌入类被称为紧嵌入，并用于定义一个图的抽象语义。请注意，尽管我们选择在这里对个体进行聚类，但也可以像在谓词抽象中那样对谓词进行聚类[7]。定义3.7设S=Us，iS和SJ=Us′，iS′是两个[0， 1]q-解释。满射函数f：US→US′是≤-嵌入（记为S≤FSJ），如果它1117685848421880012434388Q22J. Lidman，J.Svenningsson/Electronic Notes in Theoretical Computer Science 334（2018）1725.- 是的Σi=1.ΣQ所有Pi，3 ≤i≤k. . 非线性化子fNorm是一个≤-em的bedding，它产生一个新的满足下面的关系。如果关系保持相等，则嵌入是紧的<$x ∈ [1，k]，<$p ∈ Px：i S′（p）（uJ1，.， uJx）≥（u1，.，u x）∈（U S）xf（ui）=uJi，1≤i≤xi S（p）（u1，.，ux）抽象语义需要保持信息损失是保守的（即不应该虚假地引入更精确的结果）。由于这个原因，我们的抽象语义是单调增加的信息顺序≤。引理3.8（Sagiv et al. [10]，引理4.4）设S = U S，i S且SJ=US′，iS′是两个结构，其中S = SJ，f：US→ US′是≤-嵌入。那么对于每个完全指派Z，所有k元p∈Pk：iS≤ iS′ [[φ]]S≤[[φ]][0， 1]q其中iS≤ iS′是≤的逐点扩张。直觉上，给定有限数量的个体（谓词），我们应该能够将（甚至无限数量的）谓词（个体）聚类成有限数量的聚类，使得聚类中的所有谓词（个体）相对于个体（谓词）是等价我们把这种特殊的嵌入称为normalization6。更具体地说，来自归一化器的聚类的数量由下式限定：|≤（1 + 2 q）k|≤(1+2 q)Σk|Pi|在[0，1]域中。定义3.9设P = P1. 其中Pk是一元（P1），. k元（Pk）谓词。 两个个体ui，ui∈US，uiuj等价，如果所有谓词对u i和u j求值为相同的值，即如果p∈P1：p（u i）= p（u j），且<$p∈ P2，uJ∈US：[p（ui，uJ）=p（uj，uJ）]<$[p（uJ，ui）=p（uJ，uj）]，类似地，对于逻辑结构在美国。乌斯怀斯，乌斯怀斯把美国和美国的相同个体例3.10设S={u1，u2，u3，u4，u5，u6}，i S与最左边的表一样为- low.这里，u2、u4和u6对于所有谓词都是等价的（即，p、q和r）。下面最右边的表格中显示的是应用NOR时产生的结构Malizer，其中等价个体由新个体U246表示。个人一元p q谓词Ru1101u2110u3010u4110u5111u6110个人一元p q谓词Ru1101u246110u3010u5111因此，使用规范化，我们可以产生一个具有有限个个体的逻辑结构，并通[0，1]q’S26J. Lidman，J.Svenningsson/Electronic Notes in Theoretical Computer Science 334（2018）17过扩展，限制逻辑结构的数量我们6Sagiv等人。[10]将此称为规范抽象J. Lidman，J.Svenningsson/Electronic Notes in Theoretical Computer Science 334（2018）1727你，Σ我的朋友VS（vstart）V=vstart2Qn(i)（n≥ 1）≤ n且Fn（S）= Si的有界并语义.绍克x=1{λu1，.，λux. .ny=1 iSy（p）.[v1u1，.，v x≤→ u x] |p ∈Px}还考虑规范化的极端情况，即逻辑结构集是单例的情况。为了适应这两种情况下，我们参数化的抽象语义的函数Fn，收集器功能，需要n套（代表的结果从n个传入的边缘）的逻辑结构，并产生一组逻辑结构。我们考虑以下F和≤的组合：∪（ii）（n=1）T.he最大语义，其中≤H且Fn（S）=HHi=1Σ.我们引入一个抽象语义作为固定点，相对于集合包含(whenn是有界的）或来自下面的方程系统的第2.2节的信息顺序（当n= 1时），并且表明它过度近似收集语义。定义3.11设Fn是一个收集器函数，f是一个紧≤n-嵌入∗和VS映射v∈q qV到有界[0，1]值逻辑结构的集合。 [0， 1]-图G=V，E，C的值语义由下式给出：1∗[[G]][0，1]q（VS）=λ v. 我的天啊。[[st（w）]]（S） S ∈ V S（w）且⎫⎪⎬否则，⎩⎪∗⎜⎝⎪⎩[0， 1]q. S |=[0，1]qC（w，v）w→v∈E计算固定点通过迭代地应用单调递增的传递函数来进行，并在有界时间内终止，因为可能的逻辑结构的集合是有界的。根据定理，分析的结果是合理的三点一二分注意，使用Fn的模糊集抽象的结果是最准确的H最大的逻辑结构一个SQREQ域可以提供，即在一个因素真值。1号定理3.12对于一个图G= V，E，C，且初始假设S项={S0，.，S n}<$[0，1] q-<$CT [P]，n∈ N，图的集合语义记为C，并使用2值语义定义：C= lfp<$[[G]] 2（{v开始→ S进入}<${v → S|v ∈ V-{v start}）具有有界联合和最大收集器函数的抽象语义类似地使用[0， 1]q值语义定义：AF=lfpF[[G]]⊆[0，1]q（{v start→S entry}{v→ S entry|v∈V-{v start}）A、F、H=lfpFH[[G]]≤H[0，1]q（{v开始 →FH（S）条目 ）}{v1→ 2|v ∈ V-{v start}）哪里1=。美国，{λu1，.，u x.i（p）.[v1u1，.，v x≤→28J. Lidman，J.Svenningsson/Electronic Notes in Theoretical Computer Science 334（2018）17Su x]=0。 5}2x=1p∈Px相应的具体化函数由γ F和γ FH给出，其中[S] 1表示结构S在三值逻辑中的解释，即逐点扩张KJ. Lidman，J.Svenningsson/Electronic Notes in Theoretical Computer Science 334（2018）1729.⎧⎪⎨.Σ阿克斯我是我∈我们让纳夫我表示f关于变量xi的（偏）导数，νX2Q定义3.5γFγFH（S）={S#∈2-STRUCT[P]|S#≤H[S]1}（U，i）=.U，i#n∈[0，1]q-ST RUCT[P]|<$x∈[1，k]， p∈Px，u1，.，ux∈U：. i（p）。[v1≤ →u1，.， vx≤ →ux]<$−i#（p）.[v1 u1，.，vx u]≤Σ1有了上面的定义，我们可以陈述或主要定理：具体语义近似于抽象语义和具体化函数的组合：你好：C（v）s∈AF<$（v）γF（s）C（v）γFH.AFH（v）3.2动力学分析接下来，我们将探讨一个动态分析，它从静态分析的结果开始，并通过将分析结果专门化来提高精度，给出一个属性的动态分配序列。其目的是提高完备性，可能是牺牲可靠性，并计算一个新的模糊集，提高分类精度。由此产生的模糊集的描述隐含的TS-ANFIS。我们考虑在实例与分析结果之间的最小平方误差我们的动态分析实例TS-ANFIS和使用梯度下降（GD）改善在线分类。GD类似于牛顿Esparza等人 [3]证明了多项式f（x）= ici φi（x）=ici#jai，ji，j在ω-连续（交换）半环上，由于Kleene的不动点点定理 由于模糊集的隶属度是单位区间的元素，[0， 1]我们使用实半环R∈{∞}， +，·，0， 1上多项式的特殊情况。i表示它的梯度和Df。 （x）=f（v）·x a的距离多项式f.我们强调我们的多项式是在实半环的一个同余域上求值的，即在实半环的一个同余域上求值.在这篇文章中，我们考虑的情况下，从静态分析得到的逻辑结构集是一个单例，即，使用大于7的最大抽象语义计算结果。逻辑结构，即S=U，i，可以被认为是一组分类器，每个k元谓词p∈i有一个分类器，其中变量被分配一个个体（来自U）作为输入值。给定p，我们创建一个双规则TS-ANFIS，其中变量x[1，k]是个体的实值编码，例如编码uii。7通过构造一个具有2n条规则的TS-ANFIS，可以将我们的方案扩展到任意nN。 但这显然代价高昂，由于缺乏更好的方案，我们将正式化推迟到未来的工作中X30J. Lidman，J.Svenningsson/Electronic Notes in Theoretical Computer Science 334（2018）17∈i、ji、j牛顿GD在2016年，f+（νi）=lfp.Df.（f（νi）−ν）牛顿νif+（νi）=μ·lfp.（νiφ（x）−y）2GDifN−ewtoon（νi）= gfp.Df. i（ν−f（νi））νf−（νi）=μ·gfp。（y−viφ（x））2GDi表1牛顿/GD定点方程• (Rule 1）p是前提部分中的模糊集，f（x1，...，xk）= 1是后件多项式。• （规则2）是前提部分中的模糊集，并且f（x1，...，x（k）=0是后件多项式。因此，初始TS-ANFIS的输出等于谓词p。 我们的动态分析迭代地给出了一个示例分配x和相应的实际模糊隶属度y。它计算一个新的固定点时，x是输入产生预期的模糊隶属度，并更新随之而来的多项式f（x），基于误差。用于规则1的算法最小化对应于常数（其被初始化为1）的多项式系数并且最大化剩余系数（其被初始化为0）。规则2的多项式保持不变。 表1给出了固定点方程。 注意，一个半环一般没有加法逆，因此减法可能看起来是错误的。但正如Esparza等人所指出的。[3]对于特殊情况，当函数是半环中的多项式时，偏差总是正的，这是一个推论。泰勒定理的一种推广形式对于交换半环，精度随着每次迭代而指数地增加[6]。一个二进制q域中元素的个数是2q. 因此，我们的动力学分析的每次迭代都会在dq+1域中产生固定点。引理3.13表明不动点系统有解。由于所有的上升/下降链在一个n-q域中是有限的，假设x是单调递减/递增的，序列将收敛到一个新的后件多项式。引理3.13设f（x）为多项式。然后是升序/降序.νiΣ i∈N 是单调递增/递减的，并且收敛到唯一的最小/最大-估计固定点：• 0≤νi≤f+（νi）≤νi+1≤sup≤jNνj• 在f≤jN∈νj≤νi+1≤f−（νi）≤νi≤1不动点方程允许我们在引理中陈述的递归封闭形式三点十四分我们的结果表明，我们可以保证有效性的实半环上的输入施加约束，而不是诉诸一个非负版本的GD算法[1]。引理3.14给定一个x，y，和一个多项式f（x），令e（k）=f（x）-y，对于f+，e（k）= y − f（x），对于f −。 我们可以用c k+1= c k+2 μe i（k）φ（x）计算f。最后，我们在定理3.15中表明，我们的动态分析确实改善了一组例子的分析结果定理3.15对于一个图G=V，E，C，A：V ≤→[0， 1]q-π CT[P]J. Lidman，J.Svenningsson/Electronic Notes in Theoretical Computer Science 334（2018）1731.- 是的Σ是用Fn的分析结果H 抽象语义学和抽象语义学1≤i≤N 的序列其中，xji+1≤xji，yi+1≤ yi。然后每次迭代iGD算法的，应用到示例中，更新多项式，该系数是非负的，并且在极限下收敛于使样本集的最小平方误差最4结论我们已经介绍了模糊集抽象，使陈述的属性是真或假的程序在一定程度上。这为推测性优化开辟了新的可能性，现在可以使用关于哪些值、分支等比其他值更有可能的信息。我们还展示了如何通过细化以下结果来执行混合分析：在线静态分析。这已经完成了使用TS-ANFIS，自适应模糊推理系统从控制理论。这一结果为从丰富的模糊控制理论文献中引进其他结果铺平了道路引用[1] 陈杰，C.理查德，J.C. M. Honeine，Nonnegative least-mean-square algorithm，IEEE Transactions onSignal Processing59（2011），pp. 5225-5235[2] Dubois，D.，H. Prade和H.林明，[3] Esparza，J.，S. Kiefer和M.牛顿程序分析，J。ACM57（2010），pp.33：1[4] Ginsberg ， M. ， Multivalued logics ： A uniform approach to inference in arti ficial intelligence ，Computational Intelligence4（1988）. 265-316[5] Lidman，J.和J. Svenningsson，使用模糊逻辑桥接静态和动态程序分析，编程语言和系统的定量方面（QAPL）（2017）。[6] Luttenberger，M.和M. Schlund，407-418[7] Manevich 河 ， E. Yahav ， G. Ramalingam 和 M. Sagiv ， “Predicate Abstraction and CanonicalAbstraction for Singly-Linked Lists，”Springer Berlin Heidelberg，Berlin，Heidelberg，2005 pp. 181[8] Mock，M.，M.达斯角，澳-地Chambers和S. J. Eggers，Dynamic points-to sets：A comparison withstatic analyses and potential applications in program understanding and optimization ， in ：Proceedings of the 2001 ACM SIGPLAN-SIGSOFT Workshop on Program Analysis for Software Toolsand Engineering，PASTE六十六比七十二[9] 里贝罗角和M.Cintra，量化点到关系，在：并行计算的语言和，计算机科学讲义4382，Springer BerlinHeidelberg，2007页。190-204.[10] Sagiv，M.，T. 代表和R。Wilhelm，通过3值逻辑的参数形状分析，ACM Trans.程序. Lang.Syst.24（2002），pp. 217-298.A省略的证明证据定理3.12我们首先考虑使用F函数的情况，注意γ（S）创建了所有≤S的2值逻辑结构的集合，32J. Lidman，J.Svenningsson/Electronic Notes in Theoretical Computer Science 334（2018）17.ΣH2Q2QΣ.Σ·23Σ ci#ai，ji，j最小化最小平方误差，e（x）2=。f（x）−y2在一个标准上，f（x）=2我我我布拉奇我JX被量化到101域（即，Sagiv等的3值域[10]第3.5节）。由于生成S（即，固定点迭代）由定理3.8保守地完成，我们可以重新使用Sagiv等人的论点[10]定理4.9（即，的嵌入是广泛的。 到信息阶：[φ]] S（Z）≤ [[φ]] S′（f <$Z）），定理6.1（即，我们是保守的w.r. t分支条件和程序语句）和定理6.2（即，C（v）∈A（v）γ（s））。接下来我们考虑使用F H函数时的情况。注意，根据Knaster-Tarskis固定点定理，抽象语义是定义良好的。我们认为，结果是一个保守的近似（即，v：C（v）<$γ FH A FH（v））基于对收集器Fn存在一个固定点的矛盾证明：假设一个固定点S∞已经到达，那么S∞（v），v∈V是 γFH（S∞（v））是[0，1]q个逻辑结构的集合，其中谓词在S∞（v）的1以内如果S∞不是保守近似则存在一个离γFH（S∞（v））更远的元素S∈/∈γFH（S ∞（v））与之相矛盾的是，S∞是唯一的不动点。Q证据这是Esparza等人[3]中定理3.10在（非负）实半环上的特殊情况。Q证据是3.14。由于固定点迭代是在全序集（最小平方误差）上进行的，所以最小/最大和最小/最大元素重合。我们考虑求多项式f（x）的系数c i =ic i φi（x）=ticularbronx，ybronx.由于e（x）2是凸的，我们知道存在全局极小解其中梯度为零：- 是的f（x）−y≠2。布拉奇Σ ∂Σ c φ（x）−y因此maxcif（x）-y φ（x）= 2e（x）φ（x）. f（x）−y2=2e（x）φ（x），由于表达式只依赖于在当前迭代中的变量，更新序列由ci+1=ci +1给出。2 μe（x）φ（x）。 类似的C。y−f（x）<$2=−2e（x）φ（x）因此ci+1=ci−. −2e（x）φ（x）<$我=ci+2e（x）φ（x）。Q证据的3.15。引理3.14表明，每次迭代都会找到使最小平方误差最小的系数。xy单调的Toghether与引理3.13保证序列最终收敛Q
我的内容管理
展开
