摘要
图结构是一种非线性结构，在数据结构中无疑是重要的内容之一，远比链式结构和树结构要复杂。图结构可以清晰表明不同数据对象之间的关系。因此图结构被广泛应用于计算机科学、数学、工业等各大领域。如网络设计、路径规划、关系处理、电子电路设计、电网潮流管理等。但由于不同数据对象之间关系的复杂多样造就了对于图结构算法推导的困难。 图结构算法推导可以用非形式化或形式化方法实现。可见文献中大多是一些非形式化解决方案，非形式化方法解决图结构问题的规模受限，在一些较难解决的问题中不能保证正确性。现有形式化方法推导图结构算法存在推导过程复杂、难以理解且不易于形式化证明等问题。我们找到了一种形式化推导和证明的较优方案。在对图结构问题进行深入的探讨研究之后，开发出一套针对寻找图结构算法循环不变式的策略。利用递归定义技术寻找其递推关系，并就图搜索及图的最短路径两类问题给出了对应的开发循环不变式方法。再在此基础上写出抽象的Apla代码，对其进行形式化验证。最后将抽象的Apla代码转变为可执行的C++代码。这一套完整的过程实现了对图结构算法的精化，从抽象的形式化规约一步步推演出具体的可执行程序。 文章的最后利用三个实例验证了该方法的可行性和正确性。该方法在确保正确性的基础上，便于软件开发人员明白图结构算法是如何生成的。本文提出的方法不仅可以推导和证明已知的图结构算法，对未知图结构算法的推导也可以加以指导。
NETL