Derivation And Formal Proof Of Some Graph Structure Algorithms

Graph structure is a kind of nonlinear structure,which is undoubtedly one of the important contents in data structure,which is much more complex than chain structure and tree structure.The graph structure can clearly show the relationship between different data objects.Therefore,graph structure is widely used in computer science,mathematics,industry and other fields.Such as network design,path planning,relationship processing,electronic circuit design,power flow management and so on.However,the complexity and diversity of the relationship between different data objects makes it difficult to derive the graph structure algorithm.The derivation of graph structure algorithm can be realized by informal or formal methods.It can be seen that there are mostly some informal solutions in the literature.the scale of non-formal methods to solve graph structure problems is limited,and the correctness can not be guaranteed in some difficult problems.The existing formal methods for deriving graph structure algorithms have some problems,such as the derivation process is complex,difficult to understand and difficult to formal proof.We have found a better scheme for formal derivation and proof.After an in-depth discussion and study of the graph structure problem,a set of strategies for finding the cyclic invariants of the graph structure algorithm are developed.The recursive definition technique is used to find its recursive relation,and the corresponding development loop invariant methods are given for graph search and the shortest path of graph.On this basis,the abstract Apla code is written and formal verification is carried out.Finally,the abstract Apla code is transformed into executable C++code.This complete process realizes the refinement of the graph structure algorithm and deduces the concrete executable program step by step from the abstract formal specification.At the end of the paper,three examples are used to verify the feasibility and correctness of the method.On the basis of ensuring the correctness,this method is convenient for software developers to understand how the graph structure algorithm is generated.The method proposed in this paper can not only deduce and prove the known graph structure algorithm,but also guide the derivation of the unknown graph structure algorithm.