A toolkit for supporting formal verification of programs in the functional data-flow parallel programming language

The article is devoted to the architecture development of the toolkit for supporting formal verification of functional data-flow parallel programs in the Pifagor Language. The method ofdeduction based on Hoare logic is used for formal verification. A proof process is considered asa tree where each node is a program data-flow graph, whose edges are marked with formulasin a specification language. The tree root is the initial Hoare triple, namely the program data-flow graph with a precondition and a postcondition. In this article basic transformations of thedata-flow graph are considered: edge marking, equivalent transformation, splitting, folding of theprogram. By means of these transformations the initial triple is being transformed and finally isreduced to a set of formulas in the specification language. If all of these formulas are identicallytrue, then the program is correct. Architecture of the toolkit for supporting formal verification offunctional data-flow parallel programs is proposed, which allows to construct a proof three. Theimplementation of the toolkit is introduced and its main functionality is considered.