Verification of programs with mutual recursion in the Pifagor language

M. S. Ushakova ; A. I. Legalov

Modelirovanie i analiz informacionnyh sistem, Tome 25 (2018) no. 4, pp. 358-381.

Résumé

In the article, we consider verification of programs with mutual recursion in the data driven functional parallel language Pifagor. In this language the program could be represented as a data flow graph, that has no control connections, and has only data relations. Under these conditions it is possible to simplify the process of formal verification, since there is no need to analyse resource conflicts, which are present in the systems with ordinary architectures. The proof of programs correctness is based on the elimination of mutual recursions by program transformation. The universal method of mutual recursion of an arbitrary number of functions elimination consists in constructing the universal recursive function that simulates all the functions in the mutual recursion. A natural number is assigned to each function in mutual recursion. The universal recursive function takes as its argument the number of a function to be simulated and the arguments of this function. In some cases of the indirect recursion it is possible to use a simpler method of program transformation, namely, the merging of the functions code into a single function. To remove mutual recursion of an arbitrary number of functions, it is suggested to construct a graph of all connected functions and transform this graph by removing functions that are not connected with the target function, then by merging functions with indirect recursion and finally by constructing the universal recursive function. It is proved that in the Pifagor language such transformations of functions as code merging and universal recursive function construction do not change the correctness of the initial program. An example of partial correctness proof is given for the program that parses a simple arithmetic expression. We construct the graph of all connected functions and demonstrate two methods of proofs: by means of code merging and by means of the universal recursive function.

Détail

Keywords: data driven functional parallel programming, Pifagor programming language, correctness of recursions, elimination of mutual recursion, universal recursive function.

Bibliographie

[1] Nepomnyashchiy V. A., Ryakin O. M., Prikladnye metody verifikatsii programm, Radio i svyaz, M., 1988, 255 pp. (in Russian)

[2] Boyer R.S., Moore J.S., A computational logic, Academic Press, New York, 1979, 420 pp. | MR | Zbl

[3] Vazou N., Seidel E.L., Jhala R., Vytiniotis D., Peyton-Jones S., “Refinement Types for Haskell”, SIGPLAN Not., 49:9 (2014), 269–282 | DOI | MR

[4] Giesl J., “Termination of nested and mutually recursive algorithms”, Journal of Automated Reasoning, 19:1 (1997), 1–29 | DOI | MR | Zbl

[5] Legalov A. I., “Functional language for creating of architectural independent parallel programs”, Computational Technologies, 10:1 (2005), 71–89 (in Russian) | Zbl

[6] Kropacheva M. S., Legalov A. I., “Formal Verification of Programs in the Functional Data-Flow Parallel Language”, Automatic Control and Computer Sciences, 47:7 (2013), 373–384 | DOI

[7] Ushakova M. S., Legalov A. I., “Automation of Formal Verification of Programs in the Pifagor Language”, Modeling and Analysis of Information Systems, 22:4 (2015), 578–589 | DOI | MR

[8] Giesl J., “Termination of nested and mutually recursive algorithms”, Journal of Automated Reasoning, 19:1 (1997), 1–29 | DOI | MR | Zbl

[9] Bevers E., Lewi J., “Proving termination of (conditional) rewrite systems”, Acta Informatica, 30:6 (1993), 537–568 | DOI | MR | Zbl

[10] Plumer L., Termination Proofs for Logic Programs, Lecture Notes in Artificial Intelligence, 446, 1990, 142 pp. | MR | Zbl

[11] Giesl J., “Termination Analysis for Functional Programs Using Term Orderings”, International Static Analysis Symposium, LNCS, 983, 1995, 154–171 | MR

[12] Walther C., “On Proving the Termination of Algorithm by Machine”, Artificial Intelligence, 71:1 (1994), 101–157 | DOI | MR | Zbl

[13] Kushnirenko A. G., Lebedev G. V., Programmirovanie dlya matematikov, Nauka, M., 1988, 384 pp. (in Russian)

[14] Goloveshkin V. A., Ul'yanov M. V., Teoriya rekursii dlya programmistov, Fizmatlit, M., 2006, 296 pp. (in Russian)

[15] Mal'tsev A. I., Algoritmy i rekursivnye funktsii, Nauka, M., 1986, 368 pp. (in Russian) | MR

[16] Hoare C. A. R., “An axiomatic basis for computer programming”, Communications of the ACM, 10:12 (1969), 576–585 | DOI | MR

[17] Ushakova M. S., “Semantics of program data types for functional data-flow parallel programming language Pifagor”, Educational resources and technologies, 2016, no. 2(14), 263–269 (in Russian)

[18] Shilov N. V., Osnovy sintaksisa, semantiki, translyatsii i verifikatsii programm, Izdatelstvo SO RAN, Novosibirsk, 2009, 340 pp. (in Russian)