ACM通信
研究突出了
技术角度:证明程序的连续性
证明一个程序的正确性通常是一个孤注一掷的游戏。一个程序的规范要么是正确的，要么不是。如果我们的证明成功，我们有100%的正确性;如果我们的证明不成功，我们就一无所有了。形式的正确性证明是困难的，因为一个人必须象征性地覆盖整个可能的输入范围，而输入中最微小的差距也会导致证明上的差距。
但如果事实证明，留下一个缺口带来的风险实际上很小呢?当然，这是测试的假设:如果我用一个值样本测试某个函数，并且它对这个样本正常工作，那么我有理由假设它对类似的值也可以工作。如果函数的行为是连续如果它对10,100和1,000计算出正确的平方根，那么它对这三者之间的任何值也应该是正确的。
有人可能会认为这是一个危险的假设:仅仅因为我的程序对这三个值运行良好，为什么它就应该对其他值运行呢?程序可以自由地做任何事情;因为它不需要遵循数学或物理定律，它可以以完全不同的方式表现任何新的值。这种逻辑观点原则上是正确的。然而，在现实生活中，程序员更喜欢容易理解和推理的抽象。测试在实践中起作用的原因是程序员自然地追求连续性。
能够正式地对连续性和健壮性进行推理，让我们看到程序不仅由逻辑驱动，而且由分析演算驱动;这种观点对于理解为什么即使只是粗略测试，程序通常也能很好地工作非常有帮助。
虽然直观的概念很容易掌握，但连续性的概念迄今为止一直被广泛地回避。特别是，在环路存在的情况下，不可能自动地推理出连续性。这就是Swarat Chaudhuri、Sumit Gulwani和Roberto Lublinerman的工作发挥作用的地方。他们的框架可以正式验证程序的连续性，证明输入的小变化只会导致输出的小变化。他们表明，排序或最短路径等程序是连续的，甚至是李普希茨连续的，这意味着对函数输入的扰动只会导致其输出成比例的变化。这样的函数也应该被声明为健壮的，这意味着即使输入是不确定或错误的，它的行为也是可预测的。
能够正式地对连续性和健壮性进行推理，让我们看到程序不仅由逻辑驱动，而且由分析演算驱动;这种观点对于理解为什么即使只是粗略测试，程序通常也能很好地工作非常有帮助。这项工作也弥合了程序和控制理论之间的差距，允许在不同的田地之间进行充分的交叉施肥;事实上，人们可以把程序代码的数学优化看作是控制理论采用编程概念。那么，我们应该把程序看作是由逻辑驱动的，还是由微积分驱动的，或者两者兼有?我鼓励你阅读下面的文章，看看计算机程序中逻辑和微积分之间的多重联系。
©2012 acm 0001-0782/12/0800 $10.00
如果您不是为了盈利或商业利益而制作或分发本作品的部分或全部，并在第一页注明本通知和完整引用，则允许您免费制作本作品的部分或全部数字或纸质副本，供个人或课堂使用。本作品的组成部分必须由ACM以外的其他人享有版权。信用文摘是允许的。以其他方式复制、重新发布、在服务器上发布或重新分发到列表，需要事先获得特定的许可和/或费用。请求发布的权限permissions@acm.org或传真(212)869-0481。
数字图书馆是由计算机协会出版的。版权所有©2012 ACM股份有限公司
没有发现记录