Automation of Formal Veriﬁcation of Programs in the Pifagor Language - M. S. Ushakova; A. I. Legalov (Моделирование и анализ информационных систем)
Nowadays, due to software sophistication, programs correctness is more often proved by means of formal veriﬁcation. The method of deduction based on Hoare logic could be used for any programminglanguage and it has the capability of partial automation of the proof process. However, the method of deduction is not widely used for veriﬁcation of parallel programs because of high complexity of theprocess. The usage of the functional data-ﬂow paradigm of parallel programming allows to decrease the complexity of the proof process. In this article a proof process of correctness of functional data-ﬂow parallel programs in the Pifagor language is considered. The proof process of a program correctness is considered as a tree where each node is a program data-ﬂow graph, whose edges are marked with formulas in a speciﬁcation language. The tree root is the initial program data-ﬂow graph with a precondition and a postcondition, which describe restrictions on input variables and correctness conditions of the result of the program execution, respectively. Basic transformations of the data-ﬂow graph are edge marking, equivalent transformation, splitting, folding of the program. By means of these transformations the data-ﬂow graph is transformed and ﬁnally is reduced to a set of formulas in the speciﬁcation language. If all these formulas are identically true, the program is correct. Several modules is distinguished in the system: “Program correctness prover”, “Axioms and theorems library management system” and “Errors analysis and output of information about errors”. According to this architecture, the toolkit for supporting formal veriﬁcation was developed. The main functionality of the system implementation is considered.