Аннотация:
В работе предложены математические методы, предназначенные для формализации компьютерной реализации арифметических вычислений. Для построения формальных спецификаций моделей вычислений с учетом ресурсных ограничений разработан теоретико-модельный метод частичной интерпретации. С его помощью построены и проанализированы различные модели вычислений в целых и рациональных числах, в том числе в позиционных системах счисления. Архитектурные модели арифметики построены на базе языка конечнозначной логики Лукасевича и логик, обогащающих ее. Свойство слабой полноты этих логик позволило исследовать структурные характеристики операций, не зависящие от представления чисел. В частности, проанализированы механизмы обнаружения и обработки переполнения. Различные модели вычислений представлены в виде базисов логических функций. Предложен способ верификации отсутствия переполнения при вычислении арифметических выражений путем доказательства теорем многозначной логики.
Ключевые слова и фразы:машинная арифметика, частичная интерпретация, логика Лукасевича, переполнение, флаг переноса.