Research on Formal Development of Non-recursive Algorithms of Graph Search

摘要

Formal method is key approach in developing safety critical systems. Graph search algorithms are very important software components. The paper tries to formally develop two non-recursive graph search algorithms, depth-first search and breadth-first search. This is a very challenge task because non-recursive graph search algorithms have low computing complexity with high logic complexity comparing with recursive graph search algorithms. The formal development of non-recursive algorithms involves formalization of specification, loop invariant and proof of the algorithmic programs. In this paper, we introduce PAR platform that support MDD of software with high reliability and safety. Specification language Radl of PAR platform was used to describe the program specification; Software modelling language Apla was used to describe algorithmic programs; the function of recursive definition was used to develop and denote the loop invariant, then the algorithmic programs was formally proofed. Finally, the correct algorithmic programs denoted by Apla were transformed to the programs of executable language; such as C++, Java, VB and C#, etc., based on the program generating systems in PAR platform. The most important innovation is defining recursive function to denote the loop invariant that makes the loop invariant precise and simple.