用了数学,程序再也不出错啦

这个本来是发在果壳的日志上的,最近这边没什么产出,抓住5月的尾巴填充点内容吧……反正我随便写了大家也就随便看看……当然了这个也是要遵守首页上的CC协议的……

————————分割线————————

想必用windows的大家也经历过各种蓝屏(现在是黑屏),这时候是不是想狠狠地抽开发者呢?其实作为一个写程序的人来说,我觉得有bug是再正常不过的事情了,毕竟是人写程序,有时候错误难以避免。

不过,现在这样不停打补丁毕竟很麻烦,有没有什么办法可以保证程序不出问题呢?

计算机程序其实都是数学运算,可以直接用数学来处理。如果可以在数学上证明程序不会出错,那么它就一定不会出错。

但是,现在的程序动辄几十万行,要是用人力来证明的话,那恐怕要几个数学家花几个月的时间才能完成,那成本就很高了。能不能用电脑来帮我们做数学证明呢?

看起来不太可能,但的确有人在干这种事情。在法国的一帮程序员搞出来了一个自动数学证明程序,叫Coq,在法语里边是公鸡的意思,也是法国的象征(国鸟什么的)。本来他们开发这个程序的本意,正是尝试用它来代替数学家完成某些机械的证明过程。因为证明某个程序不会出错的过程也挺机械的,所以用它也没问题。

要用Coq来证明程序不会出错,主要要做两件事:将程序的每一条语句的数学含义表达出来,还有将“程序不会出错”用数学语言表达出来。前者可以自动化完成,另一帮程序员搞出来的一个Coq插件貌似就是干这个活的。后者的话,就只能手动完成了,毕竟每个程序的目的都是不一样的。

这两件事干完之后,就可以开始证明了,只要把Coq开着就可以了。一般程序越长,证明的时间也就越长,所以有时候会将程序先分割成几部分,再证明每一部分的正确性,然后综合起来。如果机器发现证明不了的地方,也会提示问题的大约所在。

那么,难道Coq就不会出错吗?这也是有可能的,但是也不是没有补救方法。Coq在证明完成之后,会输出一个形式证明,也就是说全部都是逻辑符号组成的证明。这样的证明很容易用一个更简单的程序去验证它的正确性,而这个更简单的程序的正确性,很容易可以由人来直接证明。这样的话,作为一个整体,这个证明就是有保障的了。

这一套东西,法国人搞得比较多,大概是因为整个数学界的氛围很注重形式化的证明吧。

据我所知,这套方法最成功的应用实例也是在法国,就是巴黎地铁的14号线。

这是巴黎地铁最新的一条线,也是唯一一条无人驾驶的地铁线,也是唯一有屏蔽门(据我所知,不过我也不是全部线都坐过)的地铁线。这条线所有的运营,都完全依赖于计算机程序。因为很多人对计算机程序有无端的恐惧感(天网什么的),所以当时法国政府就请专家来解决这个安全性问题。

专家就说,我们用数学来证明吧!没有比数学更可靠的了。

嘛,法国就是有这么一种文化。

于是,控制地铁开动刹车还有屏蔽门等等的程序,就都通过Coq来验证过了,而Coq也不负众望。14号线运营这么多年了,据我所知只有一两次事故发生过,都不太严重,而且跟程序本身没有关系。不过这种方法貌似没有推广开去,比如说欧盟本身好像就不太认可这种方法,不知道为什么……

不过这种方法也有弱点,就是不能处理太复杂的程序,毕竟数学证明还是很费劲的一件事情,而且Coq的表达能力也有限,对于数组和指针之类的东西处理起来相当吃力。所以,大家要是想看到用数学证明了不会无故蓝屏的windows,那恐怕还需要一段相当长的时间。

Coq的官方网址是http://coq.inria.fr/。Coq本身也可以用来辅助数学证明,可以帮助数学家验证并尝试证明相对简单的引理,这就使数学家可以专心于整个大证明的方向。现在貌似就有一个项目,尝试利用Coq去生成Kepler猜想的一个形式证明。此前有人用枚举的方法给出了Kepler猜想的证明,但是要验证这个证明是正确的,还是比较麻烦的。而如果是形式证明的话,那就好得多。

Advertisements

2 thoughts on “用了数学,程序再也不出错啦

发表评论

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