登录
首页
vwin德赢AC米兰官网网址本期:2022年7月
研究突出了
项目的连续性和稳健性
信贷:Culturamas
计算机科学家长期以来一直认为，软件与物理系统在一个基本方面是不同的:后者具有连续的动态，而前者没有。在这篇论文中，我们认为数学分析中的连续性概念是相关的和有趣的，甚至对软件也是如此。首先，我们演示了许多日常程序是这样的连续(即输入的任意小的变化只会导致输出的任意小的变化)或李普希兹连续(也就是说，当他们的输入发生变化时，他们的输出发生最大比例的变化)。其次，我们给出了一个基本自动的框架来验证一个程序是否连续或Lipschitz，表明传统的、离散的方法来证明程序的正确性，可以扩展到对这些性质的推理。我们的分析的一个直接应用是关于的推理鲁棒性在不确定输入上执行的程序。从长远来看，它给人们带来了希望，希望人们能够开发出一个可以将逻辑数学和分析数学自由结合起来的程序推理工具包。
1.简介
在计算机科学中，软件系统的动态本质上是不连续的，这一事实使它们从根本上不同于物理系统，这是公认的智慧。25年前，帕纳斯15将工程可靠软件的困难归因于“描述[软件]系统行为的数学函数不是连续的”这一事实。这意味着传统的分析微积分——当人们在分析流体的动力学时所选择的数学——不能很好地适应软件工程的需要。可以对不连续系统进行推理的逻辑更适合作为程序的数学。
在本文中，我们认为这种智慧应该持保留态度。首先，许多日常程序都是连续的，就像在分析中一样，输入的任意小的变化都会导致输出的任意小的变化。有些甚至是李普希兹连续也就是说，对程序输入的扰动最多导致输出的成比例的变化。其次，我们证明了程序的分析性质与经典的程序验证的逻辑方法并不矛盾，给出了一种基于逻辑的、大部分自动化的方法来正式验证程序是连续的或Lipschitz连续的。这一分析的直接应用是关于的推理鲁棒性在不确定性下执行的程序。从长远来看，它为程序分析的统一理论带来了希望，将逻辑方法和分析方法结合起来。
下面我们就上述问题作进一步阐述。也许软件系统破坏连续性的最基本原因是条件分支也就是形式的构念如果B然后P1其他的P2“在物理科学中产生的连续动力系统通常不包含这样的结构，但大多数非平凡程序都包含这样的结构。”如果一个程序有一个分支，那么即使是对其输入的最小扰动也可能导致它计算一个分支而不是另一个分支。因此，我们也许可以得出这样的结论:任何包含分支的程序实际上都是不连续的。
要知道这个结论是不正确的，考虑一下对数字数组排序的问题，这是计算中最基本的任务之一。每个经典的排序算法都包含条件分支。但是让我们来检查一下规范排序算法的一种数学函数排序它将数组映射到它们排序的排列。该规范不仅是连续的，而且是Lipschitz连续的:更改输入数组的任何项一个由±
回到顶部
2.连续性，Lipschitz连续性和鲁棒性
在本节中，我们将定义连续性2和Lipschitz连续性3.并展示如何使用它们来定义鲁棒性。然而，首先，我们修正了我们所推理的程序设计语言IMP。
IMP是命令式程序的“核心”语言，这意味着它只支持命令式编程的最核心特性——赋值、分支和循环。该语言具有两个离散的数据类型整数和整数数组，以及两个连续的数据类型和实数数组。支持对这些类型的常规算术和比较。根据通常设计实数算法的计算模型，我们的实数是无限精度的，对它们的初等运算假设是由单位时间的神谕给出的。
IMP中的每个数据类型都与度规．一个这个度量是给定类型值之间距离的概念。为了具体起见，我们在本文的其余部分确定了IMP类型的以下度量:
- 整数和实数类型与欧氏度规相关d（x, y) = |x y|。
- 长度相同的数组(实数或整数)的度量是l规范:d（一个1，一个2) = Max我{|一个1［我］一个2［我) |}。直观地说，数组的变化是
20.探索一个项目的结果质量和资源消耗之间的权衡。这类转换可以被视为故意将不确定性引入到程序的操作语义中。如果程序是健壮的，那么这个额外的不确定性不会显著影响它的可观察行为，因此这样的转换执行起来“更安全”。更多细节可在我们关于鲁棒性分析的会议论文中获得。3.
现在，如果一个程序是Lipschitz，那么我们可以给出由于输入的不确定性而导致其行为变化的定量上界，而且，如果输入只有轻微的不确定性，这个上界就很小。因此，Lipschitz连续性是一个相当强的鲁棒性。连续性是程序计算中鲁棒性较弱的定义ex是连续的，即使它极大地放大了输入的错误。尽管如此，它从一种常见的鲁棒性违反中获得了自由:输入中的不确定性改变了程序的控制流，而这种更改导致程序输出的显著更改。
3.程序验证
现在，我们提出了证明程序连续的自动化框架2或李普希茨。3.我们的分析是声音也就是说，一个程序被我们的分析证明是连续的或Lipschitz确实是连续的。然而，由于分析的目标是图灵完备语言，所以它是不完整的例如，一个程序可能是连续的，即使分析不认为它是连续的。
图2)．如例1所述，程序在离散类型的输入变量中总是连续的。因此，为了使问题更有趣，我们假设冒泡排序的输入是一个实数数组。和以前一样，我们用实数数组来建模图，其中每一项表示一条边的权值。给定一个程序P，我们的任务是推导一个句法连续性的判断为P，定义为一个术语b
如果b然后P1其他的P2，然后我们递归地推导出连续性判断P1而且P2．连续性判断是使用一组语法证明规则得到的，这些规则可以以标准的方式转换为自动程序分析，迭代地将连续性判断分配给子程序。图1展示了我们最重要的规则;要获得完整的集合，请参阅原始参考资料。2要理解规则的语法，请考虑规则BASE。该规则派生出结论b
b1，
图2中的项的扰动一个是否会导致“交换?一个［我),一个［我+ 1]“离开。一个不变。”ITE规则背后的核心思想是表明这样的发散并不真正重要，因为在程序状态下，对程序变量的任意小扰动都可以“翻转”保护的值b条件语句(让我们称这种状态的集合为边界的b)，条件句的分支在行为上是任意关闭的。
准确地说，让我们从b公式如下:
19现在，要得出一个程序的连续性判断"如果b然后P1其他的P2“就产出而言出， ITE显示P1而且P2成为出-等价的条件下
c和一组变量X,如果图1能否推导出判断b图2．例6(冒泡排序)。中的冒泡排序的实现图2．(我们假设它被改写为而-用明显的方式编程。)我们的目标是使判断为真
图2．注意，在任何迭代中，都可能有几个项目w的d［w是最小的。然后，一个稍微被扰动的初值d可能会导致循环迭代选择不同的w的值发生了剧烈的变化d在迭代结束时。因此，这个循环的个别迭代不是连续的，我们不能应用loop。
在之前的工作中，2我们给出了一个更有力的规则，叫做时代感应，以证明类似上述项目的连续性。这里的关键见解是，如果我们将一些循环迭代分组在一起，那么连续性就成为分组的归纳属性。例如，在Dijkstra的算法中，一个“分组”就是一个极大集年代的初始值绑定的连续循环迭代的d［w］．让0是第一次迭代之前的程序状态年代是执行。由于任意小的扰动0，我们可以在年代顺序完全不同。然而，在迭代之后运行的迭代年代在原始的执行中仍然会在迭代之后运行年代．而且，对于一个固定的0，程序状态，一旦所有迭代完成年代已经执行的，是相同的，无论这些迭代以什么顺序执行。因此，一个小的扰动不能显著地改变结束时的状态年代，和迭代集年代形成一个连续的计算。
我们已在……实施了这些规则图1，以及时代归纳规则，以一种几乎自动的程序分析的形式。给定一个程序，分析遍历它的控制点，将连续性判断分配给子程序，直到达到收敛。辅助任务，例如检查两个直线程序片段的等价性(ITE规则需要)，可以使用Z3自动执行8smt解算程序。人类干预预期有两种形式。首先，在时代归纳规则的应用中，我们有时期望程序员编写定义迭代的适当“分组”的注释。其次，如果需要一个复杂的循环不变量来进行证明(例如，当程序等价查询中的一个程序是嵌套循环时)，程序员应该提供它。可以使用启发式和辅助工具来自动化这些步骤，但是我们当前的系统没有使用它们。
鉴于我们的证明规则的不完整性，一个自然的经验问题是，我们的系统是否能够验证第2节中描述的连续计算任务的连续性。为了回答这个问题，我们在真实和真实数组数据类型上选择了几个13连续算法(包括算法)。我们的系统能够验证其中11种算法的连续性，包括Bellman-Ford、Dijkstra和Floyd-Warshall的最短路径算法;除冒泡排序外，还有归并排序和选择排序;Prim和Kruskal的最小生成树算法。我们无法验证的算法包括快速排序(Quick Sort)。请参见Chaudhuri等人。2了解更多细节。
如果b然后P1其他的P2"用矩阵集(
图3显示了关联集合的规则
11最后,图3推导出判断P: {J}，则P在输入x中为J(J, i)-Lipschitz我输出xj．例8(热身)。回忆程序＂如果（x> 2)然后x: = x/ 2其他的x: = 5x+ 11”例5 (x是实数)。我们的规则可以将左分支与包含单个条目的单个Lipschitz矩阵相关联1/2,右分支包含一个矩阵包含一个元素5。考虑到程序的连续性，我们认为该程序在输入x和输出x时是5-Lipschitz的．
例9(冒泡排序)。考虑冒泡排序算法(图2)，像以前一样，让R< p, q >表示从第p行到第q行的代码片段0是A和x1成为t．
现在,让
图3，我们可以推出(t:= A[i]): {J}， (A[i]:= A[i]+ 1]): {我}，((我+ 1]: =t): {J，我}。进行必要的矩阵乘法，我们得到R< 4 4 >:{J}。使用规则尽管,我们有R< 3、4 >:{我，J}。现在，很容易证明R< 3、4 >被执行了N次，其中N是a的大小< 2、4 >:{我，J｝N．给定J2＝我J = J我＝J，这等价于判断R< 2、4 >:{我，J}。由此，我们得到了BubbleSort:{J，我}。根据例1中进行的连续性证明，冒泡排序在输入A和输出A中为1- lipschitz．
直观地说，冒泡排序如此健壮的原因是:(1)从执行算术运算的程序点到给输出变量赋值的点之间没有数据流，(2)处处保持连续性。事实上，我们可以正式证明任何满足上述两个条件的程序都是1-Lipschitz。然而，我们在这里不展开这一论证．
例10 (bellmanford;DIJKSTRA算法)。让我们考虑BellmanFord算法(图2)，令x0等于G和x1考虑第5行(即，程序R< 5 > 5）;我们的规则可以给这个程序赋值Lipschitz矩阵J，其中
如果（x> 0)然后x: = x+ 1否则跳过”,x为整数。这个程序是2-Lipschitz。它的斜率在初始态附近是最高的x= 0:如果的初始值x的最终值从0变为1x从0到2。同时，如果我们投x在实数中，生成的程序是不连续的，因此不是K-Lipschitz为任何K．有可能给出一个不受上述问题影响的李普希茨连续性分析。该分析将上述整数转换为实数，然后计算得到的程序的Lipschitz矩阵;然而，它检查的是一个比连续性稍弱的属性。由于篇幅所限，我们不在此详细分析。
我们用上面提到的Lipschitz连续性验证方法扩展了连续性分析的实现，并将得到的系统应用到3.1节末尾提到的13个算法集合中。所有这些算法都是1-Lipschitz或者N李普希茨。我们的系统能够计算出11个算法中的9个的最佳Lipschitz常数，其中连续性可以被验证。在一个案例中(Bellman-Ford)，它证明了一个N-Lipschitz计算为N2李普希茨。它表现不佳的一个例子是Floyd-Warshall最短路径算法，它能计算的最好的Lipschitz常数是指数N3.．
4.相关工作
据我们所知，我们是第一个2提出项目连续性分析的框架。在我们面前的哈姆雷特12提倡软件连续性的概念;然而，他的结论是，“在实践中，机械地测试连续性是不可能的”，因为存在循环。在我们的第一篇关于这个主题的论文之后不久(在我们后续的关于Lipschitz项目连续性的工作之前)，Reed和Pierce18给出了一个验证函数型程序Lipschitz连续性的类型系统。该系统可以无缝地处理功能数据结构，如列表和映射;然而，与我们的方法不同，它不能推理不连续的控制流，并且会认为任何带有条件分支的程序具有的Lipschitz常数。
最近，杰哈和拉斯霍德尼科娃开始性能测试估计程序的Lipschitz常数的一种方法。给定一个程序，该方法以一定的概率确定性确定它是1-Lipschitz还是
13，该方法的吸引力在于它明确的完整性保证，而且它只需要黑盒子访问程序。鲁棒性是控制理论中的标准正确性属性，16，17有一个完整的控制子领域研究鲁棒控制器的设计和分析。然而，本文所研究的系统是用微分方程和混合自动机抽象地定义的，而不是程序。系统建模与鲁棒性分析项目是由我们在通用软件的背景下首先提出的，由Majumdar和Saha14在控制软件的上下文中。
此外，在抽象解释文献中有许多努力，虽然没有明确地验证连续性或鲁棒性，但由于浮点舍入和传感器错误而推断出程序行为中的不确定性。6，7，10其他相关文献包括关于自动分化(AD)的研究，1目标是转换一个程序P转换成一个程序，返回的导数P它存在的地方。与这里描述的工作不同，AD不尝试验证——不尝试验证一个程序是可微的或Lipschitz的。
5.结论
本文讨论了采用连续性和Lipschitz连续性等分析性质作为程序正确性的性质。这些属性是相关的，因为它们可以作为有用的定义鲁棒性程序的不确定性。此外，它们还提出了一些令人着迷的技术问题。也许与直觉相反，计算机科学的一些经典算法满足连续性或Lipschitz连续性，而关于这些特性的系统推理问题需要分析和逻辑洞察力的重要结合。
我们相信这里所描述的工作是迈向将经典微积分扩展到符号数学的第一步，在符号数学中程序形成函数和动力系统的一级表示。从实践的角度来看，这是很重要的，因为物理系统越来越多地由软件控制，甚至应用数学家也越来越多地推理没有写在教科书上的数学符号，而是作为代码．从哲学的角度来说，经典微积分专注于实际分析的计算方面，而微积分文本的表示法的发展主要是为了方便手工符号计算。然而，在我们这个时代，大多数数学计算都是由计算机进行的，我们这个时代的微积分不应该忽视计算机最容易处理的符号:程序。这一表述具有重要的意义，它不仅打开了研究连续性或导数的大门，而且打开了研究傅里叶变换、微分方程和代码的数学优化的大门。在这些方面的一些努力4，5，9已经在进行中;毫无疑问，在未来几年里还会出现其他的。
参考文献
1.巴克，科利斯，G，霍夫兰德，P，诺曼，U，诺里斯，B.自动区分:应用，理论和实现，伯克豪泽，2006。
2.Chaudhuri, S, Gulwani, S, Lublinerman, R.程序的连续性分析。在POPL(2010), 5770。
3.Chaudhuri, S, Gulwani, S, Lublinerman, R, Navidpour, S。在工程师协会(2011), 102112。
4.S. Chaudhuri, Solar-Lezama, A.翻译流畅。在PLDI(2010), 279291。
5.Chaudhuri, S.， Solar-Lezama, a .稳健地平滑程序。在骑兵(2011), 277292。
6.陈亮，Miné，王建军，库索。区间多面体:一种推断区间线性关系的抽象域。在情景应用程序(2009), 309325。
7.库索特，P.，库索特，R.，费雷特，J.，莫博涅，L.， Miné， A.，蒙尼奥斯，D.，竞争对手，X. ASTREÉ分析仪。在雇员股票拥有(2005), 2130。
8.de Moura, L. M. Bjørner, N. Z3:一个高效的smt求解器。在TACAS(2008), 337340。
9.近似双模拟:计算机科学和控制理论之间的桥梁。欧元。第17期， 5(2011)， 568。
11.可达性约束问题。在PLDI(2010), 292304。
13.Jha, M.， Raskhodnikova, S. lipschitz函数的测试与重构及其在数据隐私保护中的应用。在foc(2011), 433442。
14.符号鲁棒性分析。在即时战略游戏(2009), 355363。
15.战略防御系统的软件方面。Commun。ACM 28， 12(1985)， 13261335。
16.Pettersson, S, Lennartson, B.混合系统的稳定性和鲁棒性。在决策与控制(1996年12月)，12021207。
17.混合系统的模型检验:从可达性到稳定性。在HSCC(2006), 507521。
脚注
回忆一下度规在一组中年代是一个函数d: S × S
回到顶部数据
©2012 acm 0001-0782/12/0800 $10.00
允许为个人或课堂使用部分或全部作品制作数字或硬拷贝，但不得为盈利或商业利益而复制或分发，且副本在首页上附有本通知和完整的引用。除ACM外，本作品的其他组件的版权必须受到尊重。允许有信用的文摘。以其他方式复制、重新发布、在服务器上发布或重新分发到列表，都需要事先获得特定的许可和/或费用。请求发布的权限permissions@acm.org传真(212)869-0481。
数字图书馆是由计算机协会出版的。版权所有©2012 ACM, Inc.
评论
路加福音邓斯坦
当阅读这篇文章时，我对位图“isin.gif”用来表示集合成员(正确的)和“希腊月圆字”符号(不正确的，应该是)，甚至更糟糕的是，用于下标月圆字epsilon的方式感到非常困惑。直到我检查了纸质杂志，这才终于有了意义。
CACM管理员
以下公开信发表在2012年11月出版的《致编辑的信》(//www.eqigeno.com/magazines/2012/11/156596)上。
——CACM管理员Swarat Chaudhuri等人在《程序的连续性和鲁棒性》(2012年8月)一文中说:“软件系统能够违反连续性的最基本原因是条件分支”，但忽略了一个更根本的原因，即程序变量的状态数量有限。实数的计算机表示是不精确的，只有整数的有限子集可以精确表示。因此，在计算机算术中，方程(如(x+y) + (z-y) = x+z)不一定成立，可以引入不连续。这篇文章忽略了这个问题，同时声明，“……我们的实数是无限精度的”，并且不指定整数的上下限。这些假设在数学中很常见，但对计算机程序无效。有些程序可以用Chaudhuri的方法证明是连续的，但在执行时会表现出不连续的行为。
这篇文章还通过提出仅基于数据类型的度量来忽略实际问题，说:“长度相同的实数或整数数组的度量是l范数:d(A1, A2) = maxi{|A1[i] A2[i]|}. ...我们定义d(A1, A2) =如果A1和A2的大小不同"如以下示例所示，要获得连续性的相关定义，必须考虑应用程序的性质:通过考虑一个通过孩子的社会安全号码识别家庭的“数据挖掘”应用程序，可以看出本文的度量对于某些应用程序的不适当性。如果文章的度量应用于三个记录
A: 101234567 104432769
B: 101234567 104432769 106222444
C: 101234568 104432768A和B之间的距离无穷大，A和C之间的距离非常近。而记录B是记录A的延伸，描述的是第三个孩子出生后A所描述的家庭。记录C描述了一个不同的家庭。一个适当的度量应该考虑A接近B而远离C。
此外，文章将其示例描述为“日常程序”，但这些程序是典型的教科书算法，而不是我们每天使用的典型软件。例如，本文证明了计算两个节点之间最短路径长度的程序是连续的。然而，广泛使用的寻路软件输出的是路径，而不仅仅是长度。一个弧线长度的微小变化可能会通过暗示一条完全不同的路线而彻底改变输出。软件不断取代模拟设备的一个原因是，用户经常需要这些设备的不连续行为。具有连续行为的软件将永远是罕见的。
半个世纪以来，证明程序的正确性一直是计算机科学家的目标;这篇文章反映了我们离实现这一目标还有多远。它不是验证实际程序的属性，而是检查程序的模型。模型通常具有真实机制所不具备的属性，即使实际的程序会失败，也可以验证程序模型的正确性。
本文的方法是有用的，因为试图证明一个程序的模型是正确的可以揭示微妙的错误。然而，当得到正确性证明时，必须持保留态度。
大卫·洛奇·帕纳斯
加拿大渥太华----------------------------------------
作者的回应
从纯数学的角度来看，离散空间之间的任何函数都是连续的，因此所有的计算机程序都是连续的。但这一事实并不包含任何有用的信息。在实践中，有些程序行为稳健，有些则不然，程序的无限精度模型提供了一种很好的方法来预测程序是否稳健。
此外，我们的框架扩展到对有限集范围内的值进行操作的程序。对于这样的程序，连续性不是一个很好的鲁棒性属性，但是，比方说，Lipschitz连续性是。本文中的示例程序在这些定义下仍然健壮;我们也有证据表明，我们的鲁棒性分析可以适用于这种情况。
Swarat乔杜里
休斯顿,德克萨斯州苏米特Gulwani
雷蒙德,佤邦
显示所有2评论
