Abstract: Mathematical models of N-finite (N  2) (especially for N= 216 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.

Keywords: P-SPACE-completeness, RAM, RASP, Pascal, correctness of a Pascal program.

ACM Classification Keywords: F.2.m Analysis of Algorithms and Problem Complexity Miscellaneous.

Link:

A LANGUAGE USING QUANTIFIERS FOR DESCRIPTION OF ASSERTIONS ABOUT SOME NUMBER TOTAL PASCAL FUNCTIONS

Nikolay Kosovskii

http://www.foibg.com/ijita/vol21/ijita21-02-p02.pdf