|
Эта публикация цитируется в 2 научных статьях (всего в 2 статьях)
Семантика, спецификация и верификация программ
Платформенно-независимая спецификация и верификация стандартной математической функции квадратного корня
Н. В. Шиловa, Д. А. Кондратьевb, И. С. Ануреевb, Е. В. Бодинb, А. В. Промскийb a Автономная некоммерческая организация высшего образования “Университет Иннополис”,
ул. Университетская, 1, г. Иннополис, Республика Татарстан, 420500, Россия
b Институт систем информатики имени А.П. Ершова СО РАН,
пр. акад. Лаврентьева, 6, г. Новосибирск, 630090 Россия
Аннотация:
Цель проекта “Платформенно-независимый подход к формальной спецификации и верификации стандартных математических функций” — инкрементальный комбинированный подход к спецификации и верификации стандартных математических функций, таких как sqrt, cos, sin и так далее. Платформенно-независимый подход предполагает простую аксиоматизацию машинной арифметики в терминах вещественной арифметики (то есть арифметики поля $\mathbb{R}$ вещественных чисел), не фиксируя ни основание системы счисления, ни формат машинного слова. Инкрементальность означает, что спецификация и верификация начинается с рассмотрения наиболее “простого” случая — элементарной спецификации и верификации простого алгоритма, работающего с вещественными числами, а заканчивается модификацией элементарной спецификации и алгоритма для машинной арифметики и верификацией алгоритма, работающего в машинной арифметике. А комбинированность подхода означает, что мы начинаем с рассмотрения “базового случая” — “ручной” верификации (с ручкой и бумагой) для алгоритма, работающего в вещественной арифметике, затем выполняем ручную верификацию алгоритма, работающего в машинной арифметике, используя верификацию для базового случая в качестве “конспекта” (proof-outlines), а заканчиваем — верификацией с использованием автоматизированной системы построения/поиска доказательства для того, чтобы исключить апелляцию к “очевидности” в ручной верификации.
В статье платформенно-независимый инкрементальный комбинированный подход применяется для спецификации и верификации стандартной математической функции квадратного корня. В настоящий момент автоматизированная верификация разработанных алгоритмов выполнена только частично: с использованием системы ACL2 доказана реализуемость (существование) чисел с фиксированной запятой и таблицы начальных приближений квадратного корня.
Ключевые слова:
числа с фиксированной запятой, числа с плавающей запятой, машинная арифметика, формальная верификация, частичная и тотальная корректность, тройки Хоара, метод Флойда, точная функция, квадратный корень, метод Ньютона, справочная таблица.
Поступила в редакцию: 10.09.2018 Исправленный вариант: 15.10.2018 Принята в печать: 10.11.2018
Образец цитирования:
Н. В. Шилов, Д. А. Кондратьев, И. С. Ануреев, Е. В. Бодин, А. В. Промский, “Платформенно-независимая спецификация и верификация стандартной математической функции квадратного корня”, Модел. и анализ информ. систем, 25:6 (2018), 637–666
Образцы ссылок на эту страницу:
https://www.mathnet.ru/rus/mais654 https://www.mathnet.ru/rus/mais/v25/i6/p637
|
Статистика просмотров: |
Страница аннотации: | 165 | PDF полного текста: | 105 | Список литературы: | 21 |
|