ICM 1998, Berlin, Aug. 18–27

Abstracts of Short Communications and Posters

Section:

14. Mathematical Aspects of Computer Science

1991 MS Classification: 68 Sharipbaev, Altynbek, International Computer Systems and Information Technologies Institute under IAB, Kazakhstan A verification of the Refal-programs The problem of verification of the Refal-programs is decided by two logic languages: first for the description of the semantics of the language Refal, second for the proof of the conditions of verification of the refal-programs. Exists algorithm, which for final number of steps finds out comparability of given input to the left parts of refal-rules. For any input X the formula π_{0}(X, P (X)) is true if and only if the formula [P, π_{0}](X) is executable. The program P is partially correct if and only if the formula ∀X(φ(X) ⊃ [P, Ψ](Y)). The program P is totally correct if and only if the formula ∃X(φ(X)&(P, ¬Ψ](X)) is not executable. Reference: V. F. Turchin, Refal-5, Programming Guide and Reference Manual, New England Publishing: Holyoke, Massachusetts, 1989.