不要谈「正确性」

很多程序员自嘲「数学不好」。反过来看就是在憧憬基于数学理论写就的程序一定完全正确。其实并非如此。比如说,简单的 parser 可以严格基于有限态自动机和 LL(n) 理论,但写过的人都知道调试起来并不简单,即便充分测试也不能达到 100% 正确。

mbe

另一个例子是 3D renderer。无论是物理真实的 ray tracing 还是简单的 phong model,renderer 就是数学公式的代码实现。最近用 Metal by Example 的例子作为起点写程序。一开始还运行得不错。直到加上摄像位置的变换之后,near/far 平面会切掉在 view volume 里的模型。一开始也没在意,给 near/far 参数随便加上个余量凑合用。混了两个星期后偶然想到 Metal by Example 用的 projection 和 OpenGL 的一模一样,而 Metal 的 depth 范围不同于 OpenGL [1] 。在 Twitter 上向作者确认之后果然是这个问题。Metal by Example 经过了 15 个月的开发,出版也有一年左右。但是这个基本问题一直没有被发现。

软件开发的现状略带讽刺 —— 严格依据数学理论的程序反而缺乏有效的工具来验证其正确性。但这里其实也没什么讽刺性,因为数学本身的理论正确性也并非自动获得。一个新证明的正确性必需要经过其他数学家的人工验证,有时需要历时几年,甚至在最后才发现证明中的错误。数学的正确性是依靠数学界的「社交活动」达成的 [2] 。正如测试是软件开发的「社交活动」。

那么,数学理论是不是对软件质量没有帮助呢?也对也不对。数学理论并不能直接保证正确性,无法帮助发现错误。但是一旦发现了错误,数学理论可以帮助更快的修复软件。当我们在一个复杂的 ad hoc if-else 分支群里发现错误行为之后,很难立刻理清修复方案。而面对上文的 projection 错误,立刻就可以修正错误的参数。我把这种特性称为「可修复性」。可修复性和「正确性」不是一个层面的问题。其实软件开发的很多 best pratice 并非追求「正确性」,而是去提高「可修复性」。例如提高代码的可读性,以及我以前讨论的 MVC 模式的局限和突破,都是追求「可修复性」。经常听到很多团队讨论开发流程和实践的时候以「正确性」作为争论的立脚点,讨论怎么做才能节约测试成本,这样就走偏了。

「可修复性」不是「正确性」。也没有办法直接降低测试成本。但是「可修复性」是软件的一个隐形 spec。当错误被发现的时候,「可修复性」将一切争论局限在实现层面,避免了在设计层面的争论,更不会出现 feature vs. bug 的可笑争吵。「可修复性」还避免了修改中无意引入新的 bug。就目前的软件开发现状,我认为没有任何编程行为能有效提高「正确性」,那些能产生正确代码的程序员也无非是把代码丢给测试团队之前,自己先系统测试一番。一切编程本身的实践,都应该围绕「可修复性」来讨论。一切针对「正确性」的讨论,都应该交给测试领域。

脚注:

  1. Metal 的 canonical view volume 是 2x2x1,它的 z-buffer 范围不超过 [0, 1] 。OpenGL 为 2x2x2 ,z-buffer 范围为 [-1, 1] 。
  2. 当然,类似 Coq 这样的形式验证工具说明有可能改变这样的现状,但是距离实现仍然有一定距离。

发表评论

Fill in your details below or click an icon to log in:

WordPress.com Logo

You are commenting using your WordPress.com account. Log Out / 更改 )

Twitter picture

You are commenting using your Twitter account. Log Out / 更改 )

Facebook photo

You are commenting using your Facebook account. Log Out / 更改 )

Google+ photo

You are commenting using your Google+ account. Log Out / 更改 )

Connecting to %s


%d 博主赞过: