×

Polyvariant mixed computation for analyzer programs. (English) Zbl 0544.68005

The two major characteristics of mixed computation - termination and depth - are, in general, conflicting. A class of low-level nonstructured programs with fixed partition of the memory into accessible and suspended parts is considered. The further assumption is that, for any fixed partial input data, all the variety of computation generates a finite set of accessible memory states. Under these assumptions a polyvariant mixed computation algorithm is presented which performs all nonsuspended computation and always terminates. The basic idea is to put into correspondence to every accessible memory state its own copy of the initial program. Then the control flow of this multiple program is rearranged in such a way that if a program instruction which corresponds to an accessible memory state S computes a memory state S’ then it appoints its successor in the program copy which corresponds to the state S’. The huge resulting program is called a resultant. The residual program is obtained from the resultant through a sequence of abundant reductions which delete all computation over accessible memory and all unreachable instructions. An iterative version of the mixed computation algorithm is also offered when only reachable instructions over actually computed memory states emerge. The general treatment is supplemented by a series of examples demonstrating useful properties of the mixed computation algorithm. One of those is embedding a control structure into the residual program which is not explicitly presented in the initial program but is encoded in the input data.

MSC:

68Q60 Specification and verification (program logics, model checking, etc.)
68N01 General topics in the theory of software
Full Text: DOI

References:

[1] Bird, R.S.: Tabulation techniques for recursive programs. ACM Comput. Surveys 12, 403-418 (1980) · Zbl 0466.68017 · doi:10.1145/356827.356831
[2] Ershov, A.P.: Mixed computation: potential applications and problems for study. Theor. Comput. Sci. 18, 41-67 (1982) · Zbl 0495.68011 · doi:10.1016/0304-3975(82)90111-6
[3] Ershov, A.P., Itkin, V.E.: Correctness of mixed computation in Algol-like programs. In: Mathematical foundations of computer science, 1977. J. Gruska (ed.). Lecture Notes in Computer Science, Vol. 53, pp. 59-77. Berlin-Heidelberg-New York: Springer 1977 · Zbl 0361.68009
[4] Futamura, Y.: Partial evaluation of computation process ? an approach to a compiler-compiler. Systems ? Computers ? Controls 2, 45-50 (1971)
[5] Futamura, Y.: Partial computation of programs. In: RIMS symposia of software science and engineering. Kyoto 1982 proceedings. E. Goto et al. (eds.), Lecture Notes in Computer Sciences, Vol. 147, pp. 1-35. Berlin-Heidelberg-New York: Springer 1983
[6] Harel, D.: On folk theorems. Comm. ACM 23, 379-389 (1980) · Zbl 0432.68009 · doi:10.1145/358886.358892
[7] Itkin, V.E.: On partial and mixed computation. In: Program optimization and transformation. A.P. Ershov (ed.). Part I, pp. 17-30. Novosibirsk: Computing Center of the Siberian Division of the Academy of Sciences 1983 (in Russian)
[8] Ostrovsky, B.N.: Obtaining language-oriented parsers systematically by mixed computation. In: Translation and program models. I.V. Pottosin (ed.), pp. 69-80. Novosibirsk: Computing Center of the Siberian Division of the Academy of Sciences 1980 (in Russian)
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.