ACM通信
健全和完整性:精确
在酒店吃早餐时，你读到一篇文章，痛斥银行允许的信用卡欺诈交易。你继续结账，砰!你的信用卡被拒绝了，因为(你以后会发现)银行认为在那个异国他乡的人不可能是你。啊,这些银行!他们接受的太多了。啊,这些银行!他们拒绝太多。找到正确的平衡是一种稳健与精度．
类似的概念在程序分析工具的设计中是必不可少的，用于寻找死代码(永远不会执行的程序部分)等可疑情况。分析可以是可靠的，也可以是不可靠的;它可以是完整的，也可以不是。
这些广泛使用的概念有时会被误解。当我天真地问人们这些概念是否清楚时，我得到的第一个答案是肯定的，当然，每个人都知道!然后，当我举出信用卡拒绝或死代码检测等例子时，保证很快就会让位于混乱。事情进展不顺利的一个迹象是，人们开始使用“真阳性”和“假阴性”等术语。到那时，任何达成明确结论的前景都已不复存在。我希望在阅读完本文之后，您再也不会(在程序分析上下文中)受到使用它们的诱惑。
基本的想法很简单。分析声音如果它报告所有错误，并且完整的如果它只报告错误。如果不完整，那就更重要了精确的它报告的非错误更少。
你可以停在这里，离这儿不会太远。但更细致和精确的讨论会有所帮助。
1.一个相对的概念
作为一个常见混淆的例子，人们经常会遇到试图通过图1这样的东西来提供帮助的尝试，它不可能是正确的，因为它意味着所有声音方法都是完整的。(下面会有更好的图片。)
图1:Naïve(错误的)插图
也许这个例子可以被认为是对插图[3]的错误使用，但是考虑一下寻找死代码的例子。如果分析错误地确定某些可访问的代码是不可访问的，那么它是不健全的还是不完整的?
有了这个问题的陈述，唯一的答案是:视情况而定!
这取决于分析人员的任务:
- 如果它是一个提醒程序员错误编程风格的代码检查器，那么它是不完整的:它将错误报告给没有错误的情况。(报告不可访问的代码是可访问的会导致不健全，因为它遗漏了一个应该报告的情况。)
- 如果它是优化编译器的死代码删除算法，它将删除不可访问的代码，那么它是不健全的:编译器将删除它不应该删除的代码。(报告不可访问的代码是可访问的将导致不完整，因为剥夺了编译器的优化。)
作为另一个例子，考虑一个查找程序是否将终止的分析器。(如果你在想“但这是不可能的!，参见本文最后的“附录:关于终止”一节。)如果它说一个程序没有终止，但实际上它终止了，那么它是不可靠的还是不完整的?
同样，这取决于分析程序试图建立什么。如果它是关于一个简单的输入到输出程序(产生结果然后完成的程序)的正确性，我们就会得到不完全性:分析器错误地标记了一个实际上是OK的程序。但如果它是关于验证连续运行的程序，如工厂的控制系统，将不会停止(“活性”)，那么分析器是不可靠的。
示例不限于程序分析。从保护银行免受欺诈购买的角度来看，偶尔拒绝合法信用卡购买的欺诈识别过程是不完整的。从客户的角度来看，信用卡是一种工具，只要你有足够的信用，就可以支付，这是不可靠的。
这些例子足以说明，不存在可靠性和精确度的绝对定义:这取决于我们考虑的布尔属性的哪个版本可取的．这个决定是人的，也是主观的。死代码是优化编译器所需要的，也是不需要的(我们称之为违反)用于样式检查器。终止对于输入输出程序是可取的，而对于持续运行的程序是违反的。
一旦我们决定了哪些情况是可取的，哪些是违反的，我们就可以毫不含糊地定义概念:健全意味着拒绝所有违反，完整意味着接受所有可取的。
虽然这一定义与序言中朴实、非正式的定义一致，但它明确了两个关键方面:
- 相对论．一切都取决于一个明确的决定:什么是可取的，什么是违法的。您希望客户总是能够使用他们的信用卡进行合法的购买，还是希望检测所有的欺诈企图?
- 二元性．如果您颠倒了理想和违反的定义(它们是彼此的否定)，您就自动颠倒了健全性和完备性以及相关属性的概念。
现在我们将探讨这些观察结果的后果。
2.理论和实践
对于所有足够有趣的问题，理论极限(被称为赖斯定理)确保不可能获得健全和完整。
但仅仅说“我们必须准备好放弃合理性或完整性”是不够的。毕竟，如果我们放弃完整，就很容易获得健全:拒绝所有情况．终止强制分析器可以拒绝每个程序，因为它们可能是非终止的。一家与欺诈有关的银行可以拒绝每一笔交易(这似乎是我在旅行时银行的做法)，认为它们可能存在欺诈。另一方面，如果我们牺牲了完整性，我们便很容易确保完整性:接受每一个案件．
这些极端的理论解决方案在实践中是无用的;这里我们需要用工程性质的考虑来调整这个理论。
实际情况并不像对偶概念理论上所暗示的那样对称。如果我们不得不牺牲两个目标中的一个，那么接受一些不完整性通常会更好:得到错误警报(关于案例的虚假报告最终被证明是无害的)比遗漏错误的破坏性要小。换句话说，稳健是必不可少的。
即使是在健全的方面，练习的原则。我们必须考虑到工具如何生产的工程现实。以程序分析器为例。原则上，它应该涵盖整个编程语言。在实践中，它将逐步构建:最初，它可能不处理高级功能，如异常，或动态机制，如反射(一个特别难解决的问题)。所以我们可能要用稳健来换取所谓的"soundiness[4]，意思是该技术还无法处理的情况之外的可靠性。
如果实际的考虑使我们在完整性方面有更多的容忍度，那么在完整性方面，它们将我们拖向相反的方向(对偶性再次打击)。分析工具的作者的灵活性比理论所暗示的要低得多。实际上，几乎没有。如前所述，在原则上，虚惊一场不会造成灾难，而错过的违规则会造成灾难;但在实践中，它们几乎一样糟糕。任何使用过静态分析器或使用过静态分析器的人，都知道这个黄金法则:误报警会杀死分析器．当人们发现这个工具并第一次运行它时，他们会兴奋地发现它如何在他们的程序中发现一些有害的模式。重要的是在后续运行中发生了什么。如果分析器的诊断中有用的宝石丢失在大量不相关的警告中，那么就忘记这个工具吧。人们只是没有耐心去筛选结果。在实践中，任何分析工具都必须非常接近完整性，如果它有任何被采用的机会的话。
完整性，即没有假警报，是一种要么全有要么全无的属性。因为在一般情况下，如果我们还想要稳健性，我们就无法实现它，所以工程方法建议使用数值而不是布尔标准:精度．我们可以定义精度pr为1 - im，其中im为即时通讯精度:误报的比例。
分类理论对精度的定义不同:pr = tp / (tp + fp)，其中tp为假阳性的数量，fp为真阳性的数量。(那么im就是fp / (tp + fp))我们将回到这个定义，它需要对程序分析器进行一些调优。
的概念也来自分类理论回忆: tp / (tp + fn)，其中fn为假阴性数。在我们正在研究的这种应用程序中，召回性对应于稳健性，而不是作为布尔属性("我的程序是否合理?，而是一个定量的问题("我的程序是否合理?”)。的程度不健全UN则为fn / (tp + fn)。
3.严格的定义
利用前面的定义，我们可以正确地说明这些概念。图2显示了U调用案例集(宇宙)的两种不同划分:
- 有些情况是可取的(D)，有些情况是违反的(V)。
- 我们想知道哪个是哪个，但我们没有办法找到确切的答案，所以我们运行一个分析，通过一些情况(P)和拒绝其他(R)。
图2:所有案例，分类
第一个分类(图2中的左列和右列)是事情的情况(实际情况)。第二种分类，顶部和底部行，是我们如何评估它们。然后我们得到四种可能的类别:
- 在用绿色标记的两个类别中，评估准确地击中了现实:被接受的期望(A)，正确地通过，被发现的违规(C)，正确地拒绝。
- 在另外两个用红色标记的项目中，评估结果偏离了目标:错过违规(M)，错误地通过;误报(F)，被错误接受。
以下性质成立，其中U (Universe)是所有情况的集合，⊕是不连并集[5]:
—适用于所有情况的属性:
U = d⊕v
U = p⊕r
D = a⊕f
V = c⊕m
P = a⊕m
R = c⊕f
U = a⊕m⊕f⊕c
我们还将了解如何定义精度pr:为实际违规与报告违规的比例，即C的规模相对于r的规模。约定u为u的规模，依此类推，则pr = C / r，即:
pr = c / (c + f)——精度
im = f / (c + f)——不精确
我们同样可以用定量变量(回忆)来定义稳健性:
so = a / (a + m)——稳健性(定量)
un = m / (a + m)——不稳健
这些特性充分反映了完整性和完整性的二重性。如果我们改变我们的(主观的)标准，什么使一个案例是可取的或违反的，其他一切也会被交换，如下:
图3:二元性
我们会说以这种方式配对的属性"双“彼此[6]。
同样重要的是(可能是一种症状，表明事情并不像有时想象的那么明显)，要注意哪些属性是明显的不双。最重要的例子是“真正”中使用的“真”和“假”的概念。在布尔代数的标准对偶性中(True对偶False, Or对偶and，表达式对偶它的否定)，真和假的概念相互对偶，这使得这些表达式更加令人困惑。在“真阳性”或“假阴性”中，“真”和“假”并不表示“真”和“假”:它们分别表示(再次参见图2)评估的情况匹配还是不符合现实。在二元性下，我们颠倒了现实和评价的标准;但是匹配还是匹配!绿色区域保持绿色，红色区域保持红色。
“正”的对偶是“负”，但“真”的对偶是“真”，“假”的对偶是“假”(在这里使用这些术语的意义上:匹配与否)。所以真阳性的对偶就是真阴性，而不是假阴性，等等。这就是无尽困惑的根源。
本文的术语消除了这些混淆。理想的对偶违反，通过的对偶被拒绝，绿色区域对偶，红色区域对偶。
4.健全完整的分析
如果我们将理想世界定义为评估符合现实[7]，那么图2将简化为两种可能性，即绿色区域:
图4:完美分析(健全和完整)
该方案具有以下属性:
—如图4所示的完美(健全和完整)分析的属性:
M =∅——无遗漏违规
F =∅——不设虚惊
P = D——准确地识别需要的东西
R = V——准确识别违规行为
然而，正如我们所看到的，完美的分析通常是不可能的。我们可以选择构建一个健全的解决方案，可能是不完整的:
图5:合理的可取性分析，不完整
在这种情况下:
—如图5所示的健全分析的属性(不一定完整):
M =∅——无遗漏违规
P = A——只接受需要的
V = C—捕捉所有违规行为
P⊆D——欠近似期望
R⊇V—过近似违例
注意最后两个属性。在完美解中，性质P = D和R = V意味着产生P和V的评估，完全符合现实D和V，从现在开始，我们满足于这样的评估近似兴趣的集合:欠近似值，其中评估的计算保证不超过现实，和过近似值，其中计算不少于现实。在所有情况下，被评估的集合要么是其对应集合的子集，要么是其超集。(不严格，即⊆和⊇而不是⊂和⊃;“近似”是指可能的近似。我们可能偶尔很幸运，准确地捕捉到了现实。)
我们可以走向双重，以可能的不健全为代价来达到完整性:
图6:完整的愿望分析，不健全
属性也是双重的:
—完整分析的属性(不一定是可靠的)，如图6所示:
F =∅——不设虚惊
R = C—只拒绝违例
D = A——接受所有要求
P⊇D—过近似期望
R⊆V—欠近似违例
5.可取性分析与违反性分析
我们在上面看到了为什么“真阳性”、“假阴性”等术语，这些在分类理论中不会引起任何疑虑的术语，在应用于此处感兴趣的通过/失败分析(可取与违反)时具有欺骗性。精确的定义为破坏提供了进一步的证据。图7将我们带回到图2的一般情况(对于既不可靠也不完整的分析)，但将这些术语添加到各自的类别中。
图7:可取性分析(同图2，加标签)
分析器检查某个理想的属性，因此，如果它错误地报告了一个违规(F)，则为假阴性，如果它错过了一个违规(M)，则为假阳性。在分类理论的定义中(第2节，用缩写表示真/假阳性/阴性):TP = A, FP = M, FN = F, TN = C，对于集合大小也类似:TP = A, FP = M, FN = F, TN = C。
分类理论对精度的定义是pr = tp / (tp + fp)，这里给出了a / (a + m)。这是不对的!精确度与分析与完整性的接近程度有关，也就是说，捕获所有的违例。
分类理论是错误的吗?当然不是。很简单，就像爱丽丝踩到了镜子的错误一侧，我们也踩到了二元性的错误一侧。图2和图7描述了这一点合意性分析:检查一个工具是否有用。我们从银行的角度来评估是否存在欺诈行为，而不是从被困客户的角度;输入输出程序的终止，不是连续运行的程序;静态检查器而不是优化编译器的代码可达性。然后，如第3节所示，a / (a + m)描述的不是精度，而是稳健性(在其定量解释中，上面的参数称为“so”)。
要恢复与分类理论的联系，我们只需走对偶的路线，采取的观点违反分析．如果我们在寻找可能的违规，图片看起来是这样的:
图8:违规分析(与图7相同，不同的积极/消极标记)
然后所有的事情都解决了:tp = c, fp = f, fn = m, tn = a，经典的精度定义pr = tp / (tp + fp)得到c / (c + f)，正如我们有权期望的那样。
事实上，不应该有任何混淆，因为我们总是有相同的画面，回到图2，它准确地涵盖了所有的情况，并支持两种解释:可取性分析和违反分析。如前所述，这种混淆来自于使用对抗二元性的“真”/“假”对立。
为了避免这种不必要的混淆，我们应该使用目前讨论的四个类别:可接受的可取性、错误警报、发现的违规和遗漏的违规[8]。图2及其变体清楚地显示了在图3中明确给出的对偶性，并为愿望分析和违反分析提供了解释。稳健性和完整性只是一般框架的特殊情况，通过排除图4和图5中每个错误分析的一个情况而获得。图2之后列出的集合理论属性表达了关键概念，并仍然适用于所有变体。精度c / (c + f)和定量稳健性a / (a + m)具有符合直觉的明确定义。
我希望这个讨论是合理的。我尽力使它完整。至少它是精确的。
笔记和引用
事实上，并不是你的银行“这么认为”，而是它奇妙的新“人工智能”程序。
有关这些概念在测试中使用的讨论，请参阅Mauro Pezzè和Michal Young，软件测试与分析:过程、原则和技术威利,2008。
[3]爱德华·e·塔夫特:定量信息的可视化显示，第二版，图形出版社，2001年。
[4]迈克尔•希克斯什么是稳健性(在静态分析中)?，博客文章可用在这里, 2017年10月。
[5]不相交并集性质X = Y⊕Z意味着Y∩Z =∅(Y和Z不相交)和X = Y∪Z(合在一起，它们产生X)。
我以为这篇文章将标志着“英语”的引入。双作为一个动词，但不是，它已经存在于把一条路从单车道变成双车道(双车道)的意义上。
就像邪典电影里的祝酒词一样永垂不朽高加索的囚徒:“曾祖父说:我有买房的愿望，但我没有买房的可能。我有可能买一只山羊，但我没有这个愿望。因此，让我们为我们的愿望与我们的可能性相匹配而干杯。见第6章52节英文字幕版本．
为了完全一致，我们应该将“虚惊一场”替换为拒绝的．我保留了它，因为它已经建立得很好了，并且与所介绍的其他术语一样，不会引起混淆。
拜伦·库克，安德烈亚斯·波德尔斯基，安德烈·里巴尔琴科:证明程序终止,在ACM通信2011年5月，第54卷第5期，88-98页。
背景和确认
这种思考来自于正在进行的OO结构静态分析工作，当时我需要编写关于健壮性和完整性的正式证明，并发现这些概念的定义比通常认为的更微妙。当我看到Michael Hicks的贡献时，我几乎要放弃写这篇文章了。它很有启发性，但我觉得还有一些东西需要补充。例如，Hicks的基于场景的插图是正确的，但在我看来还是太复杂了;我相信上面使用的简单的2 × 2的图片能更清楚地表达想法。就实质而言，他的报告和我看过的其他报告都没有明确提到二元性，而在我看来，二元性是这里的关键概念。
我非常感谢Carlo Ghezzi的启发性讨论，并从Innopolis大学软件工程实验室的Alexandr Naumchev和其他人的评论中受益。
附录:关于终止
在此，我向从幼儿园就知道以下内容的读者表示歉意:如(第1节):考虑一个分析程序，它确定程序是否将终止不会引起任何特别的反应(令人羡慕的无知的幸福)或震惊的反驳说这样的分析器是不可能的，因为终止(“停止”问题)是不可确定的。这个反应和第一个反应一样不正确。中止问题的不可测性结果表明，用现实的编程语言编写一个通用的终止分析程序是不可能的，它总是为任何程序提供正确的答案，在健全和完整的意义上。但这并不排除编写针对给定程序在有限时间内正确回答问题的终止分析器。毕竟，编写一个分析器并不难，它会告诉我们程序从do_nothing直到真正的循环do_nothing结束程序会终止吗从do_nothing直到假循环do_nothing结束不会终止。在今天的软件验证实践中，分析人员可以为非常大的程序类提供这样可靠的答案，特别是在一些程序员的帮助下变体(循环变量，递归变量)。要了解终止技术的现状，请参阅Cook、Podelski和Rybalchenko[9]所做的漂亮调查。
Bertrand Meyer是瑞士苏黎世联邦理工学院(ETH Zurich)的软件工程(荣誉退休)教授，埃菲尔铁塔的软件(Goleta, CA)，米兰理工大学(意大利)教授，俄诺波利斯大学(俄罗斯)软件工程实验室负责人。
没有发现记录