这个是 @裴喜龙 老师给的系统正确性论述。
系统正确性的三个层次：程序正确性、逻辑计算正确性、模型正确性。
程序正确性，是程序正常工作，无异常退出。
逻辑计算正确性，是程序与设计的一致性，如果出现不一致，则是出错。
模型正确性，是设计与需求层面的事，对客观事务的理解出错了，
程序正确性由测试解决，是代码上的事，是程序实现技术上的事，是运行时、操作系统的事。
在cdl语言级支持Frama-C，是解决“逻辑计算正确性”，用于验证程序逻辑与设计的一致性的。
++++
第一个程序正确性，如果确定定义为『程序正常工作，无异常退出。』个人理解，这个只要语言的类型系统sound就够了，这个应该就是safe的定义。最早这样表述的应该是Robin Milner，在他的ML语言的工作中。
第二个逻辑计算正确性，是程序与设计的一致性；这个用我熟悉的表达方式，似乎是应该表达为『程序满足Specification的要求』；specification和implementation在字面上容易理解，但specification可能很难定义，或者很难证明，或者这个证明不一定在语言层面完成。
因为大家在说系统而不仅仅是语言或者语言的runtime，系统首先就成为程序的依赖性，系统可能资源枯竭，starving，各个层面上的，内存不足，CPU跑满，io调度排队，包括文件系统和网络。另一方面，在实际的绝大多数系统应用中，非功能需求很少在早期出现在specification里，比如最多使用多少内存，或者能抗住多少请求，那请求和请求还不一样，能抗住多少什么样的请求；如果软件在专门做一层，存储，或者负载均衡，专业做这个领域的人员也许还能提出这种spec，并且知道测试和提升的办法。但大多数混在业务软件里的，压跟没有这类定义，都是遇到性能不行了才想这是怎么回事，怎么标定，怎么测试，怎么优化，或者怎么牺牲（例如保证有限可用性）。
一个应用软件的完备的spec，对于实际工程的资源投入而言，在大多数情况下就接近与无穷大。这是个工程现实，也很大意义上肯定了测试驱动而不是验证（Verification）驱动，因为测试驱动很灵活，就是哪里塌了哪里测，有的放矢。
登录后可查看完整内容，参与讨论！
立即登录