计算机科学

控制复杂或生成式软件不能只靠逐行阅读，也不能只看测试是否通过。本文以转账系统为例，建立需求、契约、性质测试、实现分析、形式验证与运行监控组成的六层证据体系，说明每种方法各自能证明什么。

传统软件工程追求可理解性，却从未要求一个人理解全部系统。本文从结构化编程、信息隐藏、版本控制和大型系统协作出发，区分源码可见、局部可解释、全局可预测与系统可控制，重新界定所谓“白箱假设”。