没有合适的资源?快使用搜索试试~ 我知道了~
加权Hynons域的静态分析与乘法运算中的数组访问安全性相关
≤·理论计算机科学电子笔记267(2010)59-72www.elsevier.com/locate/entcs加权障碍子Jandrzej Fulara1,2,Konrad Durnoga3,Krzysztof Jakubczyk1,4andAleksy Schubert1,5华沙大学信息学研究所。Banacha 2波兰华沙摘要通过抽象解释,提出了一个新的静态分析数值抽象域--加权Hynons域。它能够表示形式的区间约束和关系不变量x a y,其中x和y是变量,a表示非负常数。 当使用乘法时,这种域在分析数组访问的安全性时是有用的(例如,在保护公式或在访问表达式)。我们提供了所有标准的抽象域操作,包括加宽运算符,以及一个基于图的算法,用于检查满足性和计算域时间复杂度为O(n)。这个域的表达性介于Logozzo和Fähndrich的五边形和Simon,King和Howe的每个不等式的两个变量关键词:数值抽象域,静态分析,抽象解释。1介绍程序的具体语义可能在有限的计算中产生,因此回答任何非平凡的问题可能是不可行的。一个更简单但不完全精确的模型可以用来推理程序属性。摘要解释[6]是一种广泛使用的技术,它简化了计算过程,使其重要属性可以在有限的资源(时间,空间等)内捕获。一台计算机。该技术已成功应用于各个领域,包括程序验证[2],错误发现和调试[3],1这项工作得到了波兰政府拨款N N206 493138的部分支持。2电子邮件:fulara@mimuw.edu.pl3电子邮件:kdr@mimuw.edu.pl4 电子邮件地址:kjk@mimuw.edu.pl5 电子邮件地址:alx@mimuw.edu.pl1571-0661 © 2010 Elsevier B.V. 在CC BY-NC-ND许可下开放访问。doi:10.1016/j.entcs.2010.09.00660J. Fulara等人理论计算机科学电子笔记267(2010)5922∈≤·2∈≤± ±≤Require:array input[1. m]1:{input.len ≤m}2:输出数组[1. 2 * input.len]第三节: {输出.len ≤2·输入.len;. ;m≤1·output.len}第四章: 对于i=1到m,5:{i≤1·输出.len;. 个文件夹6: 输出[2 *i-1]→输入[i]7:输出[2 *i]→ 输入[i]第八章: 端九: 返回输出Fig. 1. 一个简单的代码片段以及允许证明数组访问正确性的不变量在第6和第7行。编译期间的生成或代码优化,包括程序转换[5]。抽象解释框架允许自动推断描述分析程序的某些属性的不变量。为了应用这个框架,我们需要定义一个抽象域--一个不变量的表示,以及对它们的运算(并、交、加宽、满足性检验等)。[8]的一项建议。本文提出了一个抽象域,它可以表示形式为x,y的数值变量对之间的关系其中a是非负常数,以及区间约束x[b,c]。在二维的情况下,这样的约束描述了一个多边形,最多有6条边和6个角,这些角由不等式的系数确定(图2)。这就是为什么我们称之为加权障碍。例如图1给出了一个简单的过程,它复制给定输入数组的所有条目。静态分析使用加权障碍域可以在第5行自动推断出不变量i≤1·output.len。1.1相关工作在过去,几个数值抽象域被开发。 最基本的一个是区间域[7],它表示x[a,b]形式的不变量。它是有效的(线性时间和内存),但不处理变量之间的关系。凸多面体的定义域[10]是非常精确的-它表示形式为α1v1+α2v2+..的不变量。+α nv n其中v1,...,v n是程序变量,c,α1,.,α n是数值常数。然而,域表示和操作是低效的(变量数量呈指数级),因此对于许多应用来说是不实用的。八边形域[1,12]存储约束x y c,其中x和y是程序变量,c是常数。 所有域操作都可以在O(n3)时间内使用O(n2)内存执行,其中n表示变量的数量。使用五边形域[11],可以表示x y形式的变量之间的数值区间和符号不等式。 域操作的复杂度是O(n2),但作者没有给出一个满足性测试(如果域元素描述了一个空的约束系统)。J. Fulara等人理论计算机科学电子笔记267(2010)5961≤∞≤·∈∈{∈|联系我们−∞ ≤ ≤ ∞ ∈∞y y yX(一)X(b)第(1)款X(c)第(1)款图二、五角形(a)、加权六边形(b)和TVPI(c)用于同一组混凝土点。解决方案)。每个不等式两个变量(TVPI)抽象域[13]更强大(它可以用c表示ax+ ) , 但 也 不 太 有 效 - 最 坏 情 况 下 的 时 间 复 杂 度 是 O ( k2n3logn ( logn+logk)),其中n表示变量的数量,k可以与一对变量之间的最大不等式数量一样大(在TVPI的情况下,可以是任意大)。五角形、TVPI和加权阻碍子的比较可以在图2中找到。1.2文件纲要第2节描述了抽象域的元素的表示,定义了连接和相遇运算符,并介绍了使用这些运算符的格结构。第3节给出了一个算法,用于检查满足性和计算我们域的给定元素在第4节中,我们提供了一个加宽运算符。域的传递函数在第5节中讨论。我们在第6节结束。2问题定义我们关心的是确定一个约束系统xa y(其中x,y是变量,a是某个非负常数)是否满足。更正式地说:我们给定一个变量Var的有限集合和一个选择为实数R或有理数Q的场的集合I,它们具有自然序。我们考虑一个形式为x ≤ a · y的不等式的有限组I,使得x,yVar和aI≥0,其中I≥0表示一个J我 0aJ. 注意我们把对a的一个重要限制是,我们只允许非负系数。这使得可以保持约束的良好几何解释。 当我们要求这样一个系统I的可满足性时,我们实际上是在询问是否存在某种赋值ρ:Var→I,它给变量赋值,使得所有约束ρ(x)≤a·ρ(y)对I成立。此外,我们希望将变量的值限制在一定的区间内,即对区间约束进行建模,例如x ∈ [b,c],其中b ∈ I <${−∞}和c ∈ I <${+∞}(前提是aJ+对于所有的J我;下面我们只写以指示+)。为了做到这一点,我们引入了三个人工变量,记为v−,v062J. Fulara等人理论计算机科学电子笔记267(2010)59和v+,其可以被假定为包含在Var中。应该明确地说,v−、v0、v+都分别允许值−1、0和1。我们在任何地方都能看到J. Fulara等人理论计算机科学电子笔记267(2010)5963yy≤2x22→52≤≤× → ∪ {∞}.∈|≤·I≥∞y≤1xXy≤ x图三.由枢轴不等式y≤2x和y≤ 1x限制的可能解的区域。将我们的注意力缩小到估值ρ:Var·I,其中·表示ρ对v−、v0和v+执行固定分配。由于我们已经定义了一个帮助变量,我们可以将x∈[−5,3](比如当I=R时)这样的条件表示为不等式的合取:v−≤1x和x≤3v+。 显然,只有当x∈[b,+∞](或x∈[−∞,c])时,才证明了一个不等式.注意到v0对于表示形式为0 ≤ x的不等式是必要的。系统I可能包含一些冗余信息。我们对绑定相同两个变量的成对约束特别感兴趣,例如,对于I = R,y≤2x且y≤1x。除非我们有关于x和y的额外知识(例如,x和y被限制为正值),否则我们必须跟踪这两个不等式。然而,如果我们另外有y,那么这个约束将是超连续的,因为可以在图3中可以看到。 因此,yx不等式可以被安全地丢弃。 这只是 仅保留枢轴极约束的方法。即我们建立两个互补函数s,l:VarVarI≥0,无(s代表最小,l代表最大)定义为s(x,y)mina I0不等式x ay在l(x,y)max.a∈I≥0<${∞}|不等式yx≤a·yisinI(一)其中s(x,y)和l(x,y)都等于特殊值Nil如果I不包含形式为x≤a·y的不等式(因此s(x,y)=Nil当且仅当l(x,y)=Nil)。 我们以如下方式扩展了I≥0on和Nila·Nil=Nil·a=Nil ∞·a=a·∞=∞ia/= 0 0· ∞=∞ ·0 = 0使用上述设置,我们感兴趣的是确定关于s和l的一组可能的解γ:γ。(s,l)ρ:Var→·I|如果s(x,y)/=Nil且l(x,y)无Σ则ρ(x)≤s(x,y)·ρ(y)且ρ(x)≤l(x,y)·ρ(y).在本文中,我们将这些集合称为加权障碍62J. Fulara等人理论计算机科学电子笔记267(2010)59.对(s,l)不为空且对eachx,y∈Var,..Σ∧.Σ∧≤.Σ∨≤≤。- 是的Σ(s,l)= 0。 因此,我们可以做出一个安排,即γ(λ)=λ。2.1晶格结构成对(s,l)约束具有符合格结构的代数性质.我们在本小节中更精确地陈述这些性质。设L是笛卡尔投影的子集.Var×Var→I≥0<${∞,Nil}<$2组合我们有s(x,y)=l(x,y)=Nil或s(x,y)≤l(x,y)(其中s(x,y)和l(x,y)等于Nil)。另外,我们还在L中引入了一个特殊的元素.直觉,-是的是一个常见的代表所有emp tyWeig htedHampions,即(s,l)与我们定义了两个二元运算:最大下界(meet)和最小上界(join),它们对L中的元素对进行运算。为此,我们从I≥0<${∞,Nil}上的两个辅助序关系≤Nil和≤Nil开始,它们扩展了≤:a≤NilaJi<$a ≤aJoraJ=Nila≤NilaJi <$a ≤aJora=Nil.显然,我们也可以引入运算符(表示为min≤Nil和max≤Nil;对于≤Nil也是如此)来计算任意但有限数量的元素关于≤Nil和≤Nil阶的最小值和最大值。现在对于a,b∈L,我们有一B(sab,lab)如果a=(sa,la)且b=(sb,lb)且γ(sa<$b,la<$b)/=γ除此之外,其中对于所有x,y∈Var函数sab和lab由下式给出:同样sab(x,y)minNil sa(x,y),sb(x,y)和lab(x,y)max≤Nil. la(x,y),lb(x,y)如果a=(sa,la)且b=(sb,lb),则⊥(二)a其中对于所有x,y∈Vara如果b=否则,sab(x,y)maxNil sa(x,y),sb(x,y)和lab(x,y)min≤Nil.la(x,y),lb(x,y)(三)只有在maxNilsa(x,y),sb(x,y)≤min≤Nilla(x,y),lb(x,y)的情况下,否则sab(x,y)=lab(x,y)=Nil。图4中描绘了我们为什么设置这个限制的γJ. Fulara等人理论计算机科学电子笔记267(2010)5963.Σ直觉。图4(c)中的点a必须属于γ(a≠b),但不满足约束min(la(y,x),lb(y,x))。注意,(sab,lab)解决了一个非矛盾的不等式系统,即:γ(sa<$b,la<$b)/= π。这可以用下面的引理来理解。引理2.1对于所有a,b∈L,我们有:64J. Fulara等人理论计算机科学电子笔记267(2010)59我我γ αPVar →∧∨是对空γ的一种检查(sab,lab)。 然而,我们提出yysb(y,x)ymax(sa,sb)一Xx(一)lb(y,x)(b)第(1)款min(la,lb)(c)第(1)款图四、一个提示为什么max(sa(y,x),sb(y,x))≤min(la(y,x),lb(y,x))需要在该定义中。(i)γ(a<$b)=γ(a)<$γ(b),(ii) γ(a<$b)<$γ(a)<$γ(b)。注1:可以有效地计算双和双运算符。这个观察在交集的情况下似乎是明显的,因为上面的引理说,交集直接对应于这个操作。豪韦河这不是一个明显的定义,因为在一个明确的定义,下面第3节讨论了这个问题。它可以决定,除其他事项外,(sab,lab)表示是否满足不等式系统。既然我们已经列出了上面的关键定义,我们可以重述本小节开头定理2.2集合L在λ和λ算子下构成格从上面的定理可以得出,L可以被看作是偏序集。特别地,满足(或连接)关系在L上导出一个典范偏序:a≤bi<$a<$b=a,对所有a,b∈L。(四)当选择I作为R时,则L与和形成完全格。在这种情况下,唯一定义一个抽象函数:(·I)→ L as α(c)={a ∈ L |c <$γ(a)}使得γ和α形成伽罗瓦连接[9]。2.2图模型表示不等式组的一个方便的方法是用图。这两者之间的对应关系是非常简单的,我们赞成的图形表示的一组不等式模型。这使我们能够应用一个标准的图形算法,可以确定是否是令人满意的,如果是,我们可以构造一个显式sa(y,x)la(y,x)J. Fulara等人理论计算机科学电子笔记267(2010)5965V的一致赋值ρ。我们定义了两个加权有向图Gs=(V,E,s)和Gl=(V,E,l),其中:• 与Var同构的顶点集-每个顶点都标有自己的变量名(我们可以互换使用顶点和变量的概念)。 我们还假设V是有序的,即它同构于{1. |Var|}中。66J. Fulara等人理论计算机科学电子笔记267(2010)5912x51v−3v+产品介绍y≤·∈.ΣG G12x≤2yx≤5−3 ≤x0≤z(一)yz1v0(b)第(1)款yz1v0(c)第(1)款图五. 一个不等式组(a)及其图形表示Gs(b)和Gl(c).• 有向边集E使得(x,y)∈ Ei <$I包含一个不等式x a y,其中aI≥0(或者,s(x,y)和l(x,y)不等于Nil),• 权函数s和l由(1)给出一对典型的图Gs和Gl如图12所示。五、我们证明了一个变量u是正的,如果存在一条路,v+,v0,v1, . . ,在E. 类似地,u是负的,如果存在路径u,w0,w1,.,v−v 对于给定的加权有向图G =(V,E,ω),我们定义了路p = πv,v1,v2,.的积长π G(p), vk,u∈πG(p)= ω(v,v1)·ω(v1,v2)···ω(vk,u).3可满足性检验和正规形式多个不等式组可能有相同的解集。需要定义一个计算它们的范式的变换。这这确实是我们下面提出的算法1它还解决了另一个问题-空虚测试。算法1允许确定给定的不等式系统是否满足。对于a=(s,l)和相应的s,l,该算法计算给定不等式的传递闭包的变体。它基于著名的Floor-Warshall算法[4],用于计算图中所有顶点对之间的最短路径 如果解的集合γ(s,l)对于给定的输入图,为空,则算法返回False。否则,它将计算一个规范形式,(s,l)。算法1执行以下步骤:(i) 添加到(s,l)相关信息x≤x,平凡约束v−≤0·x,v0≤ 0·x且x≤∞·v+,且由v−,v0和v+组成。为了实现这一目标,我们定义了2X51v−3v+⎪⎨⎪⎩J. Fulara等人理论计算机科学电子笔记267(2010)5967≤FW好吧≤Nil∈{}/⎪⎪⎪GG⎩GG(sk,lk)(x,y)=(minNil(sk−1(x,y),sk−1(x,vk)·sk−1(vk,y)),⎧⎪⎨(s0,l0)(x,y)=(sin,lin)(x,y)n(1, 1)如果x=y,x/∈{v−,v0,v+},对于k从1到|Var|我们定义:最大值≤Nil(lk−1(x,y),lk−1(x,vk)·lk−1(vk,y)))。现在,(s输出,l输出)(x,y)=(s|Var|,l|Var|)(x,y)。见图6。 ModifiedFloor-Warshall()算法,用于查找具有最小和最大乘积长度的路径对(sout,lout)表示输入(sin,lin)的计算输出。(sJ,lJ)为:0,max(0,l(x,y))ifx v−,v0,x=y.min≤Nil(∞,s(x,y)),∞≠如果y=v+,x/∈{v−,v0,v+}(sJ,lJ)(x,y)6=s(x,y)=l(x,y)=Nil(0,1)如果x=y=v−(0,∞)如果x=v0,y∈{v0,v+}或者y=v0,x∈ {v−,v0}(1,∞)如果x=y=v+(s,l)(x,y)否则。(ii) 找出所有积极的变量。要做到这一点,遍历其中一个图(s或l),使用标准的广度优先sear ch算法,从v+ 开 始。将每个访问过的节点标记为阳性。如果达到v0,则返回False。(iii) 找到所有负变量:遍历s或l,但从v −开始,用反向边。如果到达v0或之前标记为正数的节点,则返回False。将每个成功访问的节点标记为否定。(iv) 对于每对顶点,找到具有最小和最大乘积长度的路径。我们在这里使用图6中给出的Floor-Warshall算法(FW)的修改,应用于(sJ,lJ)。令(sJ,LJ)= FW(sJ,lJ)。(v) 求pro管道长度为πGs(c)1和πGl(c)>1的圈c和c∈:设X={v ∈ Var|sJJ(v,v)<1}和Y ={v ∈ Var|lJJ(v,v)>1}。如果X包含正变量或Y包含负变量,则返回False。(vi) 对于x ∈ X,指定sJJ(x,x)= 0。对于y ∈ Y,设lJJ(y,y)= ∞。对于x,使得对于某个y,LJJ(x,y)= 0,设SJJ(x,v0)= 0,ljj(x,v0)=∞。对于x使得LJJ(x,y)= 0且SJJ(x,y)= 0对于某个y,设SJJ(x,v0)= 0且ljj(x,v0)= ∞。(vii) 将图6中的算法应用于(sJJ,lJJ),并将输出表示为(s,l)。如果存在s∈(v+,v)=0(其中c或r表示1≤0·v)或r∈(v,v-)=∞[6]我们使用符号(s,l)(x,y)`s(x,y),l(x,y)′。⎨⎪⎪68J. Fulara等人理论计算机科学电子笔记267(2010)59我≤·≤·≤·≤ ∞·≤·≤·≤ ≤·≤≤·≤·≤·≤I- -(that表示v≤−∞),返回False。否则返回True。生成的范式包含每对变量的最严格的约束,这些约束由输入系统的每个解填充。 在算法1的步骤i中,我们添加了一些必须包含在范式中的平凡约束,但在计算标准传递闭包(在步骤iv中执行)时无法找到-它们不是原始不等式的结果。步骤ii和iii允许我们找到值必须为正(或负)的变量。在步骤iv中,我们使用Floor-Warshall算法传播约束。 在第五步中,我们检查是否存在正变量x和不等式X一x,其中一个<1或一个负的y和一个不等式yB其中b >1。 这样的不平等是不能容忍的。 至于步骤vi,如果存在约束,x a x其中a<1和x不是正数,它可以被迭代任意多次:xa x一个2X...a kx乘 积 长度最小的路径x和x之间的关系并没有很好的定义。为了避免这个问题,我们在sJJ中替换原始不等式xx与x0 x. 出于类似的原因,我们在lJJ中替换形式y的不等式B如果b >1,则y为y。 最后,我们传播修改,在步骤vii中再次使用Floor-Warshall算法。下面陈述的定理表达了算法1的主要性质。我们首先展示它可以用作满意度测试。定理3.1(可满足性检验)是可满足的,当且仅当算法1对于相应的函数对(s,l)返回True。证据 如果算法返回True,我们可以用以下方式构造一个满足I的赋值ρ:Var→·I:• 如果u是p,则ρ(u)= 1(注意s≠(v+,u)>0),s(v+,u)• 如果u为负,则ρ(u)= −l<$(u,v−)(注意l<$(u,v−)∞),<• 在其他情况下,ρ(u)= 0。每个不等式x从原始系统 匹配以下之一案例:• x,y是位置。 则ρ(x)=1/s<$(v+,x)和ρ(y)=1/s<$(v+,y)。因为s∈(v+,y)表示v+和y之间所有路径s的最小值,所以我们有s<$(v+,y)≤a·s<$(v+,x).s∈(v+,x)>0和s∈(v+,y)>0(因为x,y是p态的)。将两边除以ys(v+,x)·s(v+,y),我们得到:1 1s<$(v+,x)≤a·s<$(v+,y).因此ρ满足不等式x≤a·y,即ρ(x)≤a·ρ(y)。• x和y都是负数。 因此,ρ(x)=l<$(x,v−)和ρ(y)=l<$(y,v−)。因为l(x,v−)表示x和v−之间所有路径的最大乘积长度,它J. Fulara等人理论计算机科学电子笔记267(2010)5969.Σ.- 是的Σ∨.Σ.{ ∈|}认为a·l<$(y,v−)≤l<$(x,v−)。两边都乘以-1,我们得到−l<$(x,v−)≤−a·l<$(y,v−)。因此估值ρ满足x≤a·y。• 在其他情况下,x不是正数,y不是负数。因此,ρ(x)≤0,ρ(y)≥0。所有不等式中的所有系数都是非负的,因此,满足x≤a·y。可以应用标准案例分析来表明,如果算法返回False,则γ(s,l)= π。Q下面的定理表明,如果算法返回True,则计算的输出(s,l)等价于输入(s,l)。定理3.2(正确性)计算的输出(s,l)与输入(s,l)有相同的解集:ρ∈γ(s,l)i <$ρ∈γ(s,l<$)。证据 我们表明,没有解决方案丢失,没有新的介绍。 无解 由于不等式的传递性,无论如何都应该服从计算出的边的新权重。由于结果中的所有不等式都不比原不等式紧,因此没有引入解。Q现在我们可以证明算法1的输出确实是所有具有相同解集的域元素定理3.3(标准形式)如果(s,l)满足,则inf≤{c∈L|γ(c)=γ(s,l)}它是一个很好的定义和等于(s,l)。证据 对(s,l)在A=c L γ(c)=γ(s,l)中定理3.2 然后,我们取A的任何元素,并证明其每个元素在用算法1归一化后仍然高于(s,l)。Q两个加权障碍物的联接不需要是加权六边形。我们的连接运算符()只计算由它的参数描述的加权障碍子的并集的一些过近似(参见引理2.1)。下面的定理表明,规范化两个参数会导致最小可能的加权六边形:定理3.4(最佳逼近)通过算法1计算的正规形a和b可以用于找到γ(a)<$γ(b)的最佳过逼近:γ(ab)= inf {γ(c)|γ(c)<$γ(a<$)<$γ(c)<$γ(b<$)}。70J. Fulara等人理论计算机科学电子笔记267(2010)59⊥.如果a=(sa,la)且b=(sb,lb),则为G证据 我们首先证明了γ(ab)= inf{γ(cd)|γ(a)<$γ(c)和γ(b)<$γ(d)}。然后,标准的考虑给出了所需的结果。Q4加宽算子当在分析程序的控制流程图中遇到循环时,可能需要计算一个定点来找到相应的抽象状态。当分析中使用的抽象域具有无限高度时,这可能导致无限迭代过程。为了避免这个问题,引入了加宽算子[6]。 它用于在有限步数中计算定点的过度近似。因此,我们需要为加权障碍定义加宽算子。直觉上,如果对于一对变量x和y,加宽的第二个参数包含比第一个参数更弱的约束,那么结果不包含这对变量的约束。我们将加宽算子o:L×L→L定义为:aob a如果b= ,否则,其中对于任何x,y∈Var:• 如果sb(x,y)≤Nilsa(x,y)且la(x,y)≤Nillb(x,y),则:saob(x,y)=sa(x,y)和laob(x,y)=la(x,y)。• saob(x,y)= laob(x,y)= Nil,否则。我们必须证明上面定义的o实际上是一个扩展算子。定理4.1我们的算子o满足加宽算子的定义:(i) 对所有的a,b ∈ L ab ≤aob,(ii) 对于每个抽象状态的无限序列c0,c1,. . ,序列a0,a1,. 定义为:并没有严格地增加。a0=c0ai=ai−1ocifor i >0证据 直接检查所需的属性。Q请注意,不应该规范化加宽的结果(将(saob,laob)替换为(saob,laob))。这可能导致潜在的无限递增序列a0,a1,. .图7示出了序列c0、c1、.生成无限递增序列a0,a1,. . .为了简单起见,只给出了s图的一部分(变量v-和v0没有显示)。请注意,使用加宽算子而不进行归一化,序列aJ在第一步之后稳定下来(图7(e))。J. Fulara等人理论计算机科学电子笔记267(2010)59712我1112我v+11 1v+...Σ←Σy yX2(a) 了c0yz x z2(b) Ciy y22iX122i+11 1v+z222i+2X122i+11 1v+z x z2 2(c) a2i(d) a2i+1(e)a1磅=a2磅图第七章加宽结果的归一化可以给出严格递增的无穷序列。5传递函数要将抽象域应用于程序分析,需要指定每种类型的指令如何改变抽象状态。传递函数必须过度近似具体语义[6]。我们展示了几个如何在加权障碍中对测试建模的示例。设a表示测试e. 我们在测试后计算集合的过近似b{ρ∈γ(a)|ρ满足e}γ(b)。对于e=v1≤c<$v2,我们计算b为:如果a=或γ(bJ)=,则b=否则,其中bJ定义为:bJ(x,y)=sa(x,y),la(x,y)min≤Nil(sa(x,y),c),max≤Nil(la(x,y),c)如果(x,y)/=(v1,v2)否则,请执行以下操作。现在让我们考虑一个赋值w w+k,其中k>0。图8显示了二维情况下的赋值结果请注意,传递函数引入了一些精度损失-计算的加权六边形过度近似运算的精确结果(在图8(b)中表示为虚线形状)。整个转让的规则是漫长的和技术性的。为了清楚和简洁起见,我们在这里只给出了所加常数k为正值的情况。给定非空输入a,赋值的结果b计算如下:• 对于x,y/=w:b(x,y)=(s∈a(x,y),la∈ a(x,y))1111v+72J. Fulara等人理论计算机科学电子笔记267(2010)59←∈≤·(无,无)否则,• b(x,w)=(sb(x,w),lb(x,w)),其中:一一1−k·la(v−,w)一一乌乌DdCcWaB(一)Wa+ k b+ k(b)第(1)款见图8。 在(a)和(b)赋值w w + k之前和之后的加权六边形。虚线形状表示指定的确切结果。n(sa(w,y) +k·sa(v+,y),∞)如果sa(v+,w)• b(w,y)=la(y,)Nil,sa(w,y)Nil⎪⎨(0,la∗(w,y) +∗k−)ifla<$(y,v−)Nil,la(w,v−)/=Nil,⎪⎩la(w,v−)−k>0.sa(x,w)·sa(x,v+)·sb(x,w)=如果s(x,w)/=Nil,则s(x,v+)/=Nilsa(x,w)否则,.la(x,w)如果00
下载后可阅读完整内容,剩余1页未读,立即下载
![pdf](https://img-home.csdnimg.cn/images/20210720083512.png)
![-](https://csdnimg.cn/download_wenku/file_type_column_c1.png)
![](https://csdnimg.cn/download_wenku/file_type_ask_c1.png)
![](https://csdnimg.cn/download_wenku/file_type_ask_c1.png)
![](https://csdnimg.cn/download_wenku/file_type_ask_c1.png)
![](https://csdnimg.cn/download_wenku/file_type_ask_c1.png)
![](https://csdnimg.cn/download_wenku/file_type_ask_c1.png)
![](https://csdnimg.cn/download_wenku/file_type_ask_c1.png)
![](https://csdnimg.cn/download_wenku/file_type_ask_c1.png)
![](https://csdnimg.cn/download_wenku/file_type_ask_c1.png)
![](https://csdnimg.cn/download_wenku/file_type_ask_c1.png)
![](https://csdnimg.cn/download_wenku/file_type_ask_c1.png)
![](https://csdnimg.cn/download_wenku/file_type_ask_c1.png)
![](https://csdnimg.cn/download_wenku/file_type_ask_c1.png)
![](https://csdnimg.cn/download_wenku/file_type_ask_c1.png)
![](https://csdnimg.cn/download_wenku/file_type_ask_c1.png)
安全验证
文档复制为VIP权益,开通VIP直接复制
![](https://csdnimg.cn/release/wenkucmsfe/public/img/green-success.6a4acb44.png)