形式化方法中误导性基准测试的批判

一篇论文利用形式化方法验证操作系统代码时使用了误导性的统计数据。作者批判了单纯比较“证明代码比”的错误方法，因为它忽略了规范的完整性和复杂性。文章指出，证明大小与规范大小之间存在近似二次关系，而规范的复杂性远比代码大小更重要。通过对多个已验证系统的分析，作者展示了更全面的数据，包括代码大小、规范大小和证明大小，并强调了模块化在降低验证成本方面的作用，但同时也指出像seL4这样复杂的系统难以模块化。最终，作者呼吁研究界停止使用毫无意义的“证明代码比”指标。