这个是 @裴喜龙 老师给的系统正确性论述。
系统正确性的三个层次：程序正确性、逻辑计算正确性、模型正确性。
程序正确性，是程序正常工作，无异常退出。
逻辑计算正确性，是程序与设计的一致性，如果出现不一致，则是出错。
模型正确性，是设计与需求层面的事，对客观事务的理解出错了，
程序正确性由测试解决，是代码上的事，是程序实现技术上的事，是运行时、操作系统的事。
在cdl语言级支持Frama-C，是解决“逻辑计算正确性”，用于验证程序逻辑与设计的一致性的。
++++
第一个程序正确性，如果确定定义为『程序正常工作，无异常退出。』个人理解，这个只要语言的类型系统sound就够了，这个应该就是safe的定义。最早这样表述的应该是Robin Milner，在他的ML语言的工作中。
第二个逻辑计算正确性，是程序与设计的一致性；这个用我熟悉的表达方式，似乎是应该表达为『程序满足Specification的要求』；specification和implementation在字面上容易理解，但specification可能很难定义，或者很难证明，或者这个证明不一定在语言层面完成。
因为大家在说系统而不仅仅是语言或者语言的runtime，系统首先就成为程序的依赖性，系统可能资源枯竭，starving，各个层面上的，内存不足，CPU跑满，io调度排队，包括文件系统和网络。另一方面，在实际的绝大多数系统应用中，非功能需求很少在早期出现在specification里，比如最多使用多少内存，或者能抗住多少请求，那请求和请求还不一样，能抗住多少什么样的请求；如果软件在专门做一层，存储，或者负载均衡，专业做这个领域的人员也许还能提出这种spec，并且知道测试和提升的办法。但大多数混在业务软件里的，压跟没有这类定义，都是遇到性能不行了才想这是怎么回事，怎么标定，怎么测试，怎么优化，或者怎么牺牲（例如保证有限可用性）。
一个应用软件的完备的spec，对于实际工程的资源投入而言，在大多数情况下就接近与无穷大。这是个工程现实，也很大意义上肯定了测试驱动而不是验证（Verification）驱动，因为测试驱动很灵活，就是哪里塌了哪里测，有的放矢。
很难证明的情况很多，证明一个算法不死锁活锁就干翻绝大多数程序员了；而且这些证明通常不在语言层面完成，可能要使用Process Calcluli，或者类似SPIN，TLA+这样先construct一个小模型，证明之后再Code Gen框架代码，再填充细节。
而且一些直觉上很简单的东西，比如『请你证明一下你的程序不会使用超过450MB内存』，Java程序员只会低声回答你给我滚。这虽然是个玩笑，但是也说明更多层的抽象会让verification也更困难，包括前面说的操作系统抽象也有同样的问题。
这些还都和实时性无关。绝大多数语言都未提供对实时性的定义。
这段在说我理解的『程序满足spec』，测试是不完备的，但是有技巧和经验的自动化测试在行业里工作的不错；只有很特殊的软件需要verification，无论是证明器的，还是模型检查的。证明器的，大名鼎鼎的作品就是seL4。还有Xavier Leroy领衔的CompCert，验证过的C语言编译器。
seL4是一个明星项目。站在工程的角度看用verification的巨大优势，不仅仅在于『绝对』正确上，也在于它可以用一条证明，替代天文数字的测例。不过后者其实很难说proof-based verification做到了，因为seL4的proof script的代码量也是seL4的源码量的几十倍，这个倍率，用test suite也可以做到相当好的质量了，而且写test suite容易招聘得多。
CompCert至今闭源。实际上国内学术界如果有人出头做一个copycat是有价值的，因为在很多领域真的需要编译器绝对正确，而编译的代码效率不够高可以用更高主频的处理器解决。但这也是一个艰苦的工作，工作量不小。也意味着类似的工作，很难在商业公司完成。
而且不要忘了这两个项目有个很好的特点是spec够小。高度抽象的软件都有一个特点就是小接口，但是deep，内部逻辑复杂。但小接口，或者小spec集合，才能给verification提供可能性。
如果是个GUI程序，CSS特效加持着各种动画飞来飞去，这怎么验证？我听说过有国外大媒体公司像素级验证web开发结果的（对照photoshop稿），但这么变态的要求也还不是全部，也只能挑典型分辨率，目标配置，还有动画呢？验证帧率吗？要是动画是交互的，要开发一个机器人去对打和录屏吗？
不多举例子了，观点已经很清楚了，我们都同意implementation should meet specification，但很多的时候不是practical的，spec不完备甚至无法完备；就算能完备成本上也没有必要。可以理解为verified software在今天看仍然不是普适的，只适用于有抽象稳定接口的系统软件，而且规模不大。你看数据库这么广泛使用的工业软件，都没有一个流行数据库证明过了。
++++
登录后可查看完整内容，参与讨论！
立即登录