: A mathematical notion of a computer program-function for some programming languages (in particular, for some versions of Pascal and Turbo/Visual Prolog) is introduced as a restriction of an algorithm class FP. Such a notion is useful for more adequate formalization of finite memory of computer intended for a program run. Complexity of logic-mathematical properties proof of such program-functions is investigated. A predicate language is introduced to formulate such a partial program properties. P-SPACE-completeness of elementary theories under a finite signature based on such a kind of functions with the use of halting predicate and predicates of conditional equality and conditional inequalities. This allows to use the first order language for description of logic-mathematical properties of computer program-functions by extension of the used program-functions by means of a special additional value in the case of infinite looping of a program-function. In many cases it allows to replace traditional mathema