Approximation of abstract semantics by formal models of programs

V. A. Zakharov

Diskretnaya Matematika, Tome 10 (1998) no. 4, pp. 119-141.

Résumé

Solving problems of analysis and optimization of computing programs in algorithmic systems is complicated by non-recursiveness of functional properties of programs. According to Rice's theorem, in a universal programming language any property of programs which depends only on the functions computed by them is algorithmically undecidable. Therefore the following approach is used. The initial complex semantics $\sigma$ of programs is replaced by a simpler semantics $\omega$ or by a class of semantics $\Omega$. If the satisfiability of some property of programs in the semantics $\omega$, or in each of semantics of the class $\Omega$, implies its satisfiability in the semantics $\sigma$, then we say that the semantics $\omega$, or the class $\Omega$, approximates $\sigma$ with respect to this property. If for a given semantics $\sigma$ we choose a suitable approximation, in which the property of programs under investigation is algorithmically decidable, then it is possible to construct an effective procedure which partly solves the problem of analysis of functional properties of programs in the semantics $\sigma$.One of the central problems of theoretical programming is the problem of functional equivalence of programs, and the present paper is devoted to the study of approximation of semantics with respect to this property of programs.