我今天要教大家一个魔法,会了这个魔法,念一句咒语,任何代码都没有bug
想知道咒语是什么吗?现在就告诉你。
跟我念:「这段代码没有任何期望行为。」
A software bug is an error, flaw, failure or fault in a computer program or system that causes it to produce an incorrect or unexpected result, or to behave in unintended ways.当然,你接下来肯定要问我,能不能写出符合某specification的软件呢?能。这,比如 @Belleve 提到的Coq,Hoare Logic,等等等等,都能做。唯一的问题就是,做起来太繁琐了,证明比实现难很多。这也是为什么大部分软件都没有人做formal verification(Coq,Hoare Logic等)。至于安全性远远高于软件成本的safety critical的东西有没有人用这种办法?当然有了!DeepSpec: The Science of Deep Specification,file system: http:// css.csail.mit.edu/6.888 /2015/papers/haogang.pdf ,基础算法:http://www. cs.ru.nl/~james/RESEARC H/types2008.pdf ,分布式系统:https:// homes.cs.washington.edu /~mernst/pubs/verify-distsystem-pldi2015-abstract.html ,操作系统:http:// web1.cs.columbia.edu/~j unfeng/09fa-e6998/papers/sel4.pdf ,编译器:CompCert - The CompCert C compiler
这就是答案,以下是略相关的东西,开始离题:
能不能降低FV的成本呢?可以,并且一直在降低:在这里有两条路,一是用软件完全自动的证明没bug(Model Checking, SMT,Dafny @ rise4fun from Microsoft),一是采用半自动化,使你在更高层次(tactic等)上控制证明。
这还是太高,能不能再降低FV的成本呢?如果我们牺牲一部分正确性,可以:我们可以用contract,把static analysis改成dynamic analysis,同时,我们可以做一半不做一半,一定的地方用static analysis证明没bug,剩下的用contract,降低bug概率/范围http:// arxiv.org/abs/1506.0420 5
能不能降低学习FV的成本呢?可以,我这里要举两个没有人会猜到我会一起用的例子:Simply Typed Lambda Calculus, Java Card,前者对于所有程序,都会计算出答案,不会死循环,也不会不能运算下去,后者符合Applet Isolation Principle(http://www. labri.fr/perso/ly/publi cations/using_coq_to_verify_javacard.pdf )。类型系统就是FV最著名的例子,没有之一。
能不能反过来用testing帮助formal verification?能!Isabelle就是这样做的:http:// isabelle.in.tum.de/dist /Isabelle2015/doc/nitpick.pdf
可以看出,这里已经有一条尽管比较粗糙,但是pay as you go的gradual path了,我也希望并预言,随着CS/CPU的发展,这条path会越来越无缝(adapt cost越来越低),较高层的成本也会慢慢降低,会使得被验证没bug的地方越来越多