怎样证明一个程序是正确的?这是一个普遍被忽略的问题。
这并不是说软件开发者们从不考虑这个问题。在一个程序的开发过程中,“正确”是所有其他工作的前提,开发者首先做的是证明程序是可以正确的,然后才来考虑性能、扩展性等等其他的问题,所以程序的正确性是所有有理智的开发者都必然会考虑的问题。
对于软件开发,“正确”通常指的是:给定一系列的测试用例和使用场景,程序能够通过这些测试,满足这些应用场景。这明显是一个不充分的定义,它把“正确性”依赖于所给的测试用例跟使用场景的完备性。假如一个程序通过了所有的测试,但在它的开发者没有考虑到的场景里面表现异常,这算不算是一种错误?如果从一开始就没有考虑到这些场景,也就是不存在“正常”又何来的异常?
"Testing shows the presence, not the absence of bugs. —— Edsger W. Dijkstra"
Edsger W. Dijkstra认为可以用形式化(formalization)的方式去证明程序的正确性。把程序看作是一种机械装置(mechanism),给定某些输入经过一系列的操作,这个装置从状态空间(state space)内的一个状态转换到另外一个状态。大部分程序员的目标就是构造这样一种装置:它拥有合适的状态空间,包含了所有需要达到的状态;以及从输入到目标状态的坐标系统。而编程语言则是描述这种装置的一个工具。
在里面,Edsger W. Dijkstra演示了形式化证明在一些小程序中的应用。虽然这种方法在复杂的大程序中似乎很难应用,但这提供了一个新的角度来看待程序和编程。
程序(Program)的正确性
《A Discipline of Programming》热门书评
-
大师的书的确读来有难度
3有用 4无用 风纪扣v 2013-10-02
上世纪80年代这本书的影印版在国内高校计算机界广为流传,尔后却消失匿迹,重读到此书,已是十几年之后的事了。 &...
-
程序(Program)的正确性
0有用 0无用 Hakura Matata 2017-03-28
怎样证明一个程序是正确的?这是一个普遍被忽略的问题。这并不是说软件开发者们从不考虑这个问题。在一个程序的开发过程中,“正确”是所有其他工作的前提,开发者首先做的是证明程序是可以正确的,然后才来考虑性能、扩展性等等其他的问题,所以程序的正确性是所有有理智的开发者都必然会考虑的问题。对于软件开发,“正确...
-
直接看翻译会觉得晦涩
0有用 0无用 hgz一般人 2017-04-07
这本书挺难翻译的。读原文读的巨吃力。主要是那种绕来绕去又特别profound的说话风格。确实不好翻译。而且我觉着英语的表达力比汉语要强。尤其是表达特别复杂的概念的时候。各种定语从句套定语从句的时候。。。再加上裘老翻译的时候选词比较“信”,有的地方反而不够“达”。翻译真实玄学啊。。。所以建议只读英文版...
书名: A Discipline of Programming
作者: [荷] Edsger W·Dijkstra
出版社: Prentice Hall, Inc.
出版年: 1976-10-28
页数: 217
定价: USD 87.33
装帧: Paperback
ISBN: 9780132158718