A LANGUAGE USING QUANTIFIERS FOR DESCRIPTION OF ASSERTIONS ABOUT SOME NUMBER TOTAL PASCAL FUNCTIONS
Nikolay K. Kosovskii · 2014
Mathematical models of N-finite (N 2) (especially for N= 2 16 typical for IBM-compatible personal computers) real, integer or Boolean valued computations are proposed in the frameworks of a finite-discrete mathematics. Such a mathematical model more precisely characterizes the contemporary practice of the computer use. Notions of an N-finite RAM (Random Access Machine), an N-finite RASP (Random Access Machine with Stored Program) and an N-finite Pascal program using integer operations modulo N with the reminders from the segment (-N/2, N/2 - 1 + (N mod 2)) are introduced. A formal N-finite quantifier logic language of modulo N arithmetic operations is defined. It allows formulating mathematical properties of such a non-recursive total Pascal function or predicate. It is proved that the problem of a formula identical truth in such a language containing arithmetic operations modulo N is a P-SPACE-complete one. So, the proof of a correctness of a non-recursive total Pascal program may be simplified with the use of the proposed language.