在软件工程中，确保软件系统正确可靠地运行至关重要。这对于诸如网上银行、电子商务和实时系统等关键系统尤其重要。一种用于验证此类系统属性的有前景的技术是“证明分数”，它使用一种称为“项重写”的方法。

证明分数由声明和重写组成，如果所有组件的求值结果都符合预期，则问题得到解决。这种方法在自动化和人工之间取得了平衡：机器处理诸如代换、简化和归约之类的常规任务，而人类则专注于最有趣的任务，例如确定证明策略。此外，即使是部分完成的证明也能提供有价值的反馈，通常可以指明下一步该尝试什么。

这项技术已通过代数规范语言(尤其是 OBJ 系列，例如 OBJ3、CafeOBJ 和 Maude)付诸实践，这些语言旨在通过术语重写来执行。证明分数的一个关键优势在于，它们使用与系统规范语言相同的语法和求值机制，从而使验证过程顺畅且紧密集成。

因此，该方法已成功应用于各种系统和协议。然而，该方法也存在一些缺点，使其主要局限于学术环境。

为了理解这一差距，由尾形和弘教授领导的研究团队与日本先端科学技术大学院大学(JAIST)的助理教授 Duong Dinh Tran 共同对证明分数的过去、现在和未来进行了研究。“证明分数已经证明了其能够验证系统(包括我们每天依赖的系统)是否符合其设计。”

Ogata教授和Tran助理教授解释说：“在这项研究中，我们分析了证明分数的过去和现在，以了解其当前面临的挑战，并找到提高其适用性的方法。” 他们的研究发表在《ACM计算调查》杂志上。

证明分数最初由研究员 Joseph A. Goguen 于 20 世纪 90 年代提出。自那时起，它已在多种 OBJ 语言中得到实现。在本研究中，研究人员探索了证明分数的理论基础，并分析了其在不同 OBJ 语言中的实现。

研究人员还研究了证明分数成功应用的几个案例，包括通信、身份验证和电子商务协议、实时系统、现代密码协议以及后量子密码协议，这些加密方法旨在抵御即将到来的强大量子计算机。

这项分析揭示了证明分数的优势。最值得注意的是，用于描述系统的语法也可以用来证明系统的属性。与高度抽象的传统定理证明方法不同，证明分数的这一特性确保了证明的每一步都基于系统的形式化定义，从而使证明更加透明易懂。此外，证明分数以程序形式编写，因此与程序一样灵活。

然而，这项分析也揭示了它们的主要弱点，即证明分数是由人为编写的，人为必须确保所有可能的情形都得到处理，这使得它们容易出现人为错误。之前的所有实现都没有在遗漏某个情形时向用户发出警告，这在处理大型证明时尤其成问题。这也是证明分数未能得到更广泛采用的主要原因之一。

虽然已经开发出一些证明助手来弥补这一缺陷，但它们通常会削弱证明乐谱的优势。不过，有一款名为 CiMPG 的 CafeOBJ 证明助手，它保留了证明乐谱的优点。

研究人员还强调了其他悬而未决的问题，包括需要更简单、更人性化、更易于阅读的证明，让研究人员以外的更广泛的受众能够访问，以及需要更多的公共图书馆。

为了解决这些悬而未决的问题，研究人员建议现代系统应该提供一个集成开发环境，就像那些流行的编程语言所使用的那样，为编写和管理证明分数提供图形化、交互式的支持。他们还建议研究 Maude 的最新功能。

研究人员表示：“证明分数对于塑造我们未来社会的新兴安全关键系统至关重要。从网上银行和电子商务中使用的通信协议，到区块链和后量子密码学，它们在创建可靠系统方面的潜力巨大。”

总体而言，这项研究不仅强调了证明分数的关键作用，而且还制定了使其更加实用和广泛使用的路线图。

更多信息： Adrián Riesco 等人，《证明分数：一项调查》，ACM 计算调查(2025)。