形式规范重构的模型检查验证

"这篇论文探讨了在重构过程中如何确保模型检查的正确性，特别是针对使用Object-Z编写的面向对象规范。作者通过实验展示了如何利用模型检查器SAL来验证简单的类型重构是否保持行为一致。文章指出，重构是改变软件系统内部结构的过程，而不影响其外部行为，这一过程在现代软件开发中被广泛应用到程序、UML模型以及正式规范的重构。为了保证重构的安全性，文章强调了行为保留的重要性，并提出在代码或模型重构后，应当通过广泛的测试来确保行为的一致性。在本文中，作者专注于那些只影响单个方法的重构类型，并利用SAL工具进行形式验证，以实现对重构正确性的正式证明。" 文章开始介绍了重构的概念，它是一种用于改进代码或模型结构的技术，以提高可读性和可重用性，而不会改变其对外部行为的影响。重构的流行得益于Opdyke的博士论文和Fowler的著作，现在已被广泛应用于程序、UML模型和正式规范。重构的目标是优化面向对象的结构，类似于经典的命令式程序模块化。 接下来，文章指出，虽然“改善结构”的标准可能存在争议，但保持行为不变的条件更为明确且重要。这确保了重构后的代码或模型对用户（无论是人还是其他软件系统）来说仍然是透明的。对于代码重构，通常需要通过详尽的测试来检查行为一致性。 论文的核心部分讨论了在Object-Z规格上使用模型检查器SAL进行形式验证的方法。作者选择了只影响单个方法的重构类型进行研究，通过SAL工具，他们能够证明这些类型的重构在保持行为一致性方面的正确性。SAL是一个模型检查器，它可以自动检查规格是否满足特定的逻辑属性，因此非常适合用于验证重构的正确性。 文章的结论部分可能讨论了实验的结果和未来的研究方向，包括可能扩展验证的重构类型或者探索其他形式验证技术在重构验证中的应用。尽管这部分内容没有给出，但可以推测，作者可能已经展示了他们的方法在实际案例中的有效性，并提出了进一步研究的可能性，以增强重构过程中正确性保证的方法和工具。 这篇论文为理解如何在重构过程中保证模型检查的正确性提供了重要的见解，特别是在形式规范领域，这对于确保软件系统的稳定性和可靠性具有关键意义。通过形式验证，开发者可以更有信心地进行重构，减少因结构改变导致的潜在错误。