简化系统规格证明：应用改进技术于理论计算机科学

"本文介绍了一种改进的证明技术，用于简化在理论计算机科学中系统规格的证明过程，特别是针对大规格系统。该技术利用抽象和细化，通过构建更抽象的模型来简化证明步骤。" 在系统形式化开发中，构建抽象规范并逐步细化至具体设计是关键步骤。在此过程中，需要证明规范满足特定性质，如一致性、无死锁等。这些证明往往复杂，尤其是对于大型系统。本文作者D.阿提亚、S.王和J.C.P.伍德考克提出了一个新方法，旨在使这些证明变得更易处理。 该技术分为三个主要步骤： 1. 构建一个更抽象的模型A，这个模型比原始规范S更易于证明性质P。 2. 在模型A中证明性质P。 3. 证明规范S与模型A之间存在细化关系，即S是A的一个实例。 这个方法的创新之处在于，它允许使用像Z这样的形式化方法，即使对于涉及并发行为的证明。Z通常用于顺序程序的规格描述，但在本文中，所有证明都在Z中完成，包括那些关于并发系统性质的证明，如无死锁。 文章详细介绍了Circus规格语言，这是一种结合了Z和CSP特性的形式化规格描述语言。Circus适用于描述复杂的并发系统，而本文将改进的证明技术应用于不同复杂度的Circus规范，展示其有效性。 在第三部分，作者展示了如何应用这项技术到实际案例中，通过两个具有不同复杂度的例子，进一步阐述了技术的具体运用和优势。这些例子可能包括从简单的系统到更复杂的系统，以此证明该技术的普适性和实用性。 最后一节，作者讨论了使用这项技术的实际经验，可能包括遇到的挑战、技术的优势以及未来的研究方向。这项工作提供了一种新的、实用的方法，以简化系统规格的证明，对于促进形式化方法在大型系统开发中的应用具有重要意义。