VDM specification of an algorithm for graph decomposition

Complex software systems need a precise specification of their intended behaviour. While graph theory plays an important role in several aspects of building such software systems, formal methods provide a rigorous mathematical framework within which a system can be described. In this paper, an algorithm for decomposing a graph into disjoint paths is presented. Such decompositions are useful, particularly in implementing software testing. VDM representation of the proposed algorithm facilitates automation of testing process without any ambiguity.