论述内容：本文介绍了基于抽象解释的静态分析的活动，并通过应用逻辑关系来合成其适当的编程逻辑

理论计算机科学电子笔记173（2007）339-356www.elsevier.com/locate/entcs从逻辑关系David A. 施密特计算机与信息科学系堪萨斯州立大学Manhattan，KS 66506USA摘要我们将定义基于抽象解释的静态分析的活动与通过应用Abramsky所演示的逻辑关系来合成其适当的编程逻辑我们从基类型的近似关系开始，它将具体的计算值与它们的近似值联系起来，我们将这种关系提升到函数空间和上、下幂集。由此产生的族的关系不需要生成伽罗瓦连接，但当他们这样做，我们表明，关系的概念的健全性和完整性与伽罗瓦连接为基础的概念相吻合。关键词：抽象解释，逻辑关系，伽罗瓦联络，时态逻辑1介绍静态分析-程序属性的自动提取-依赖于适当选择的编程逻辑，用于说明和验证属性。例如，非确定性状态转换系统的静态分析通常采用动态[16]或Hennessy-Milner [18]逻辑的变体来声明和验证性质：对于状态，c∈C：C| = p，对于原始性质，p，c|=[f]φ，ifforallcJ∈f（c），cJ|=φC|=<$f <$φ，如果存在CJ∈ f（c）使得CJ|= φ其中f：C→ P（C）表示非确定性转移函数/动作。1由NSF ITR-0326577支持2电子邮件：schmidt@cis.ksu.edu1571-0661 © 2007 Elsevier B. V.在CC BY-NC-ND许可下开放访问。doi：10.1016/j.entcs.2007.02.042340地方检察Schmidt/Electronic Notes in Theoretical Computer Science 173（2007）这种逻辑从何而来？我们可以通过设c∈C且S<$C：S|=<$φ，如果对所有c∈S，c| = φS|=<$φ，如果存在c ∈ S使得c |= φ c| = f;φ，如果f（c）|= φ这说明所设置的域在原始逻辑中是简单的。现在，[f]φ应读作f;φ的缩写。这个逻辑本身是另一个逻辑的一个实例，其中泛量化器量化了析取;存在量化器的合取;传递函数的域和余域性质都可以描述：S|=k（i< kφi），如果对于所有c∈S，则存在sj0：x：= pred（x）x：= succ（x）writeInt（x）Q：输出是否为pos？A：抽象解释domainInt by符号={neg，zero，pos，any}：readSign（x）如果isPos（x）：x：=pred（x）哪里succ（pos）=possucc（zero）=possucc和pred （ neg ）=negpred（zero）=negpred计算静态分析：{zero<$→pos，neg <$→any，pos <$→any，any <$→any}这个问题只决定于零-静态分析是合理的，不完整图1.一、抽象解释：性质计算通过逻辑关系从基本类型上的抽象映射和更高类型上的生成映射中提取近似关系;Backhouse和Backhouse [4]，他们在关系代数中公理化了Abramsky的许多本文件的贡献是它使用的逻辑关系产生一个静态的分析-即使在没有伽罗瓦连接-和合成一个逻辑适当的推理分析的2静态分析和逻辑属性图1显示了一个小程序和一个问题：在终止时，输出是正整数吗我们可以采用静态分析，而不是彻底地测试程序来回答这个问题，在图中，静态分析使用符号属性的抽象域Sign作为计算的近似值。当程序对转换函数succ和pred进行了抽象，得到了程序的抽象解释，可用于抽象测试例图中显示的结果让我们得出结论，输入为0会导致正输出，但Sign内的精度损失会阻止对正、负和任意整数输入的决策。33如果我们通过添加性质≤零和≥零来改进Sign，则改进后的succ和pred也将决定pos和neg的问题。342地方检察Schmidt/Electronic Notes in Theoretical Computer Science 173（2007）{...、-2，-1，0，1，2，.}{−4，− 1，0}{0}简体中文neg零P（国际）{...、-3，-POS{−4，{−2}{1，2，3，.}{1，4}{2，4，6，8，.}没有{}γ：符号→ P（Int）γ（无）={}γ（neg）={···，−3，−2，−1}γ（零）={ 0}γ（pos）={ 1， 2，3，···}γ（任意）=Intα：P（Int）→符号α（S）= H{a|γ（a）δ}例如，在一个实施例中， α{2，4，6，8，. }=posα{−4，−1， 0} =任意α{0} =零α{}=无，等等（P（Int），<$）<$α，γ<$（Sign，±）是一个伽罗瓦连接：γ解释了在Sign中，α将每个具体集合映射到最好地描述该集合的属性。图二. P（Int）与Sign之间的Galois联系3伽罗瓦连接伽罗瓦连接是大多数静态分析的基础[7，20，26]：对于完备格，（C，）和（A，±，H，H），一对单调映射，α：C→A和γ：A→C，定义了伽罗瓦连接，简称为C<$α，γ<$A，i <$α <$γ±A→AidA，γα±C→CidC。[4]正如我们将看到的，伽罗瓦连接结构使我们能够精确地程序和逻辑的合理、最精确和完全图2显示了通常与整数的符号抽象相关联的伽罗瓦连接，如图1所示。 图中的伽罗瓦连接是原始抽象关系ρ Sign Int × Sign的设n>0，定义ρSign_Int×Sign如下：−n ρ符号neg+n ρ符号pos0ρSignzerom ρSignany， for allm∈Int例如，+3具有属性pos，因为+3ρ符号pos。设A是一个完备格（静态分析[20]所需），C是一个（偏序）集。对所有的c，cJ∈C，对所有的a，aJ∈A，一个二元关系ρ<$C×A，是(i) U-闭i <$cρ a和a±AJ蕴涵cρAJ(ii) GLB-闭i ∈ cρH{a| cρ a}4等价地说，当对所有c∈C和a∈A，c<$Cγ（a）i <$α（c）±a，函数α和γ形成伽罗瓦联络。当格被视为范畴而函数被视为函子时，伽罗瓦连接定义了一个附加项[1]。地方检察Schmidt/Electronic Notes in Theoretical Computer Science 173（2007）3431 2 1 1 12(iii) L-闭i <$cρ a和CJ±c蕴涵CJρ a(iv) LUB-closed i {c| cρ a}ρ a.U-和L-闭包确保近似关系ρ[9，24]的可靠性，GLB-和LUB-闭包分别确保最精确的抽象（α）和具体化（γ）的存在-我们有[1，4，36，38]U-GLB-L-LUB-closedρC× A定义了伽罗瓦连接，C<$α ρ，γ ρ<$A，其中α ρ（c）= H{a| cρ a}和γ ρ（a）=<${c| cρ a}。此外，每个伽罗瓦连接定义了U-GLB-L-LUB-闭关系，cρ a i <$c<$Cγ（a）（i <$α（c）± a）.每个静态分析都基于近似关系，并且大多数这样的关系具有U-GLB-L-LUB-闭包（但不是全部，例如，[9、23、41]）。 关系ρSignInt×Sign（其中Int是离散序的）是U-L-GLB-闭的，但不是LUB-闭的。在这种情况下，图2中的伽罗瓦连接可以通过完成Int到P（Int）来构造。我们通过将ρ Sign“提升”为逻辑关系ρ L（Sign）来做到这一点4逻辑关系和伽罗瓦联系复合类型上的近似关系由逻辑关系正确定义[28]。对于基类型、b、函数类型以及下幂集和上幂集类型，τ：：= b|τ1→τ2|L（τ）|U（τ）我们定义这些域：• Db被给出（例如，Int和Sign）• Dτ1→τ2=Dτ1→Dτ2，Dτ1的单调函数的偏序集到Dτ2。 （静态分析的单调性曲面[7]。）• DL（τ）=PL（Dτ），Dτ的一个下幂集，它是D的下闭子集的集合，其中包括所有的↓d，对于所有的d∈D，部分地按π排序，并且在π下闭。 5（这包括P↓（D），D的所有下闭子集的集合。• DU（τ）=PU（Dτ），Dτ的一个上幂集，它是D的上闭子集的集合，对于所有d∈D，它包含所有的↑d，按π偏序，在π下闭。(This包括P↑（D），D的所有上闭子集的集合。近似逻辑关系族通常定义为ρτ<$Cτ×Aτ：ρb是给定的，对于基类型b（例如，ρ符号（Int×符号）fρτ→τfi ∈c∈Cτ和a∈Aτ，c ρτ a蕴涵f（c）ρτf（a）S ρL（τ）Ti∈L（τ），存在a∈T∈AL（τ）使得c ρτ aS ρU（τ）Ti ∈U（τ），存在c∈S∈CU（τ）使得c ρτ a5如果S={DJ∈D，则S ∈ D是下封闭的|对于d∈D，↓d={DJ∈D|dJ±Dd};SD为upclosedif S={dJ∈D|{d∈S，d±DdJ};nd↑d={dJ∈D|d±DdJ}。344地方检察Schmidt/Electronic Notes in Theoretical Computer Science 173（2007）图三.幂集逼近定义如预期，例如，fρτ→τf断言函数f近似于-1 2因为近似关系相关的参数映射到近似关系相关的答案。S ρL（τ）T定义了一个过近似关系：S被T过近似，因为S的每个元素在T中都有一个近似。对偶地，S ρU（τ）T定义了一个欠逼近关系，因为T中的每个元素都被S中的一个具体元素所证明。见图3集合近似的例子，它提出了下幂集和上幂集[27，39]上关系的逻辑读数，让人想起Winskel [42]提出的模态语言下幂集近似是Abramsky的安全附加的一个例子4.1逻辑关系的闭包性质命题4.1对于ρτ<$Cτ×Aτ，(i) ρ L（τ）和ρ U（τ）是L-闭的; ρ τJ→τ是L-闭的，i ∈ ρ τ是。(ii) ρ L（τ）和ρ U（τ）是U-闭的; ρ τJ→τ是U-闭的i <$ρ τ是。(iii) 若ρ τ是U-GLB-闭的，则ρ L（τ）也是; ρ τJ→τ是U-GLB-闭的，i ∈ ρ τ是。(iv) 如果ρ τ是L-LUB-闭的，那么ρ U（τ）也是; ρ τJ→τ是L-LUB-闭的，i ∈ ρ τ是。UI下幂集近似定义了普遍的、析取的、条件：例如，{neg，zero，none}断言（neg<$zero）-所有数据都是非正的：P（P{ S|SUIInt}{any，neg，zero，pos，none}P（符号）{neg，zero，pos，none}{ S|S非阳性}UI{ S|S阴性）UI- -{neg，zero，none} {neg，pos，none}{zero，pos，none}{neg，none} {zero，none}{pos，无}联系我们- -上幂集近似定义合取的，存在的特性：例如，{neg，pos，any}断言否定-存在否定和肯定的数据：P（P（Int）op）{ S|SUIInt}- -联系我们{neg，任何}{zero，任何}{pos，any}{neg，zero，any} {neg，pos，any}{zero，pos，any}{any，负，零，正}P（签{ S| 0S，−n S，+nUI- -{ S| S非空}UI{ S|−n{\fnMicrosoftYaHei\fs14\bord1\shad0\3aHCC\b0}UI{ S|0S，− n{\fnMicrosoftYaHei\fs14\bord1\shad0\3aHCC\b0}{\fnMicUIUIUI地方检察Schmidt/Electronic Notes in Theoretical Computer Science 173（2007）345τττ τ τττ τ ττ最好最好缺少对ρL（τ）的LUB闭包和对ρU（τ）的GLB闭包的保证;这取决于所使用的特定幂集但我们有[36]• 对于PL（τ）型的下幂集PA，ρL（τ）<$P↓（Cτ）×PA是LUB闭的.• 对于任何上幂集，PU（τ），ρU（τ）<$PC×P↑（Aτ）型的PC使用这些结果，我们可以根据需要从逻辑关系中建立伽罗瓦连接。一个标准的技巧是完成一个U-GLB闭关系，如ρ符号Int×Sign，其中Int是离散序的，到U-GLB-L-LUB-闭ρL（Sign）P（Int）×triv（Sign），其中下幂集triv（Sign）=（{↓a|a∈Sign}，n）与Sign序同构。这就产生了图2中的伽罗瓦连接。5功能健全性和完整性图1显示了具体的状态转换函数succ：Int→Int和pred：Int→Int，必须抽象为succ：Sign→Sign和pred：Sign→Sign来进行静态分析。一个函数f：C τ→C τ，当f ρ τ → τ f时，可由f：A τ→A τ完全抽象. 这个关系定义与抽象解释中的函数健全性的经典定义一致[ 1，8，15 ]：如果fρτ→τf是U-GLB-L-LUB-闭的，那么以下是等价的：• f ρτ→τ f• αρ C→A fαρ• fγρ温度范围 γρ 布拉夫αρ和γρ是关于f和f的半同态;见图4。给定伽罗瓦联络，Cτ<$αρτ，γρτ <$Aτ，关于伽罗瓦联络的f：C τ → C τ是f=αρτ◦ fγρτ=H{f |fρ τ→τf}[8]。 如最后一个等式和命题4.1所示，如果ρτ缺乏U-GLB-闭包，则不存在Galois联络，也不存在最精确联络抽象f在A内的映射被f精确保持(i) 当α作为从f到f的同态时，则f对于f是α（向后）完备的[8，15]。(ii) 当γ是从f到f的同态时，则f是γ（向前）-完全的f[14]。参见图4。 如果某个f对于f是（α -或γ -）完备的，则f也是（α -或γ-）完备的[15 ]第10段。的完整性的结果将在下一节中展开有一个关于可靠性的重要例子：对于一个非确定性的状态转移系统，（R，R× ） ， 我 们 将 转 移 关 系 R 刻 画 为 fR ： → P （ ） 。 假 设 有 一 个 近 似 关 系ρState<$$>×A和一个抽象转换系统（A，R<$A×A），如“抽象模型检验”[ 5，13 ]中所用使用模拟的标准定义[18]：R ρ状态-模拟所有346地方检察Schmidt/Electronic Notes in Theoretical Computer Science 173（2007）状态最好功能健全性：f：A→A是健全的，因为f：C→Ciαf±f<$αif<$γ±γfFS f（S）#（a）f第#段英（S）faf#（a）α和γ是半同态。例如：对于succ：P（Int）→ P（Int），succ（S）={n +1 |n ∈ S}，succ是succ的可靠性。γ（forward）-完备性：fγ=γfα（向后）-完备性：αf=fα（a）fFS f（S）af#f#（a）（S）f#γ是从A到C的同态：它保持f为f。α是从C到A的同态：它保持f为f。例如：对于negate：P（Int）→ P（Int），negate（S）={−n|n∈S}和negate（neg）= pos，negate（pos）= neg，等等，negate对于negate是α-和γ-完全的;相反，succ对于succ既不是α-也不是γ-完全的;最后，square对于square（S）={n2|n∈ S}。见图4。 用半同态和全同态c，cJ∈A，a∈A，c ρ状态 a和 cR cJ意味着存在 aJ∈ A使得 a R aJ和 cJ ρ状态 aJ，如果fR：A→PA是单调的，其中PA是下幂集，则R ρState-模拟Ri<$fRρState→L（State）fR.对偶模拟，其中Rb ρ−1- 模拟R，其特征在于具有上部幂集为fR ρState→U（State）fRb（参见6程序逻辑给定一个抽象，ρC×A，生成一个静态分析（例如，图1和2），我们需要一种断言语言来定义静态分析必须检查和验证的属性，以确保程序正确性或代码改进。最简单的断言语言仅仅是A本身的元素（例如，符号，如图1中所用），其“逻辑语义”是[[ a ]] ρ = {c|cρ a}，对每个a ∈ A.一个直接的好处是，对于f：C→C是合理的每个f：A→A也是f关于断言语言A的合理后置条件Transformer：对于所有a∈A和c∈C：c∈[[a]]ρimpliesf（c）∈[[f（a）]]ρ事实上，F是A中f的最强后置条件Transformer。地方检察Schmidt/Electronic Notes in Theoretical Computer Science 173（2007）347ρ ρ ρρ典型的静态分析使用这样的A和f来计算抽象程序的后置条件。在程序退出时（或在关键的内部程序点），有一些断言需要检查。 假设断言被陈述为aout∈A。使用cin ρ ain，静态分析计算f（ain）并检查f（ain）±aout是否为真。如果是，则f（cin）∈[[aout]]ρ通过U-闭包成立数据流分析，类型检查和程序验证通常被实现。前面的技术是健全的，但“不完整”（参见。图1）。我们更倾向于一个判定过程：假设ρ ∈ C × A是U-GLB-闭的，并定义α ρ：C→A为α ρ（c）= H {a| cρa}，即α ρ将c映射到它的最佳逼近。我们说fρ-决定f，如果，对所有c∈C，a∈A，f（αρ（c））±ai<$f（c）∈[[a]]ρ这意味着f 当ρ定义了伽罗瓦连接，可判定性与αρ-函数完备性一致命题6.1对于U-GLB-L-LUB-闭ρ，f ρ-决定fi <$f对f 是α ρ-完全的。这就是为什么α完备性在实践中很重要。6.1内部逻辑断言语言A具有内在逻辑，即存在逻辑连接词，这些逻辑连接词被表示为A上的函数。这里有一个重要的例子。若ρ∈C×A是U-GLB闭的，则H：A×A→A是A中的逻辑合取：对所有c∈C，a0，a1∈A：c∈[[a0Ha1]]ρ i <$c∈[[a0]]ρ且c∈[[a1]]ρ这扩展了基于A的断言语言，φ：：= a|φ H φ，对于所有的a∈ A，我们可以使用通常的合取推理规则例如，在图2中，H是合取，我们可以断言2∈[[anyHpos]]ρSign。最重要的是，当一个逻辑连接词存在于A的内部逻辑中时，我们可以在A的答：对于合取，如果静态分析证明aout±φ1Hφ2，那么我们可以安全地得出结论，对于所有cρ aout，c∈[[φ1]]ρ和c∈[[φ2]]ρ。并非所有的命题连接词都存在：对于图2，析取失败，因为0 ∈[[any]]=[negH pos]]，但0/∈ [[neg]]和0/∈ [[pos]]。6 因此，标志标志zero±negHpos并不意味着0∈ [[neg]]ρSign或0∈ [[pos]]ρSign。前面对合取的定义有些不正式;更精确的说法是：[[H（a0，a1）]]ρ=且（[[a0]]ρ，[[a1]]ρ）6 如果在符号中存在析取，它必须等于H。348地方检察Schmidt/Electronic Notes in Theoretical Computer Science 173（2007）L（τ）τ其中，和：P（C）×P（C）→ P（C）是π。 这使得连接词，并且，在A中由H表示。对于k元逻辑联结词f：P（C）k→ P（C），k元函数f：Ak→A，我们说fρ-表示f，如果[[f（ai）ik]]ρ=f（[[ai]]ρ）i k(See合取的例子，其中f=and且f=H。）我们将这个概念与函数完备性联系起来：对于ρ <$C × A，定义ρ<$P（C）×A为S ρ a i <$，对于所有c∈S，cρ a。7ρ是L-LUB闭的，因此γ ρ：A→ P（C）是γ ρ（a）= ε {S| Sρ a}={c| cρ a}=[[a]]ρ.命题6.2当ρ<$C×A是U-GLB-闭的时，f：A→A ρ-表示f：P（C）→ P（C）i <$f对f是γ ρ-完全的。这就是为什么γ-完备性在实践中很重要。7逻辑关系产生逻辑连接词从基类型τ和近似关系ρτ<$Cτ×Aτ出发，利用复合类型上的逻辑关系生成断言语言Aτ中的逻辑运算符.请从第4节开始回顾下幂集的定义;回想一下，对于具体下幂集PL（Cτ）和抽象下幂集PL（Aτ），对于下闭集S∈PL（Cτ）和T∈PL（Aτ），S ρL（τ）Ti∈S，存在a∈T使得c ρτ aPL（Aτ）中的下闭集可以写成表达式↓{ai}ik。 我们治疗↓就好像它是ais：↓{·}：Aτk→ PL（Aτ）的k元逻辑连接词，从逻辑关系定义其语义：[[↓{ai}i

下载后可阅读完整内容，剩余1页未读，立即下载