RUS  ENG ЖУРНАЛЫ   ПЕРСОНАЛИИ   ОРГАНИЗАЦИИ   КОНФЕРЕНЦИИ   СЕМИНАРЫ   ВИДЕОТЕКА   ЛИЧНЫЙ КАБИНЕТ
Общая информация
Последний выпуск
Архив
Импакт-фактор

Поиск публикаций
Поиск ссылок

RSS
Последний выпуск
Текущие выпуски
Архивные выпуски
Что такое RSS



Модел. и анализ информ. систем:
Год:
Том:
Выпуск:
Страница:
Найти






Персональный вход:
Логин:
Пароль:
Запомнить пароль
Войти
Забыли пароль?
Регистрация


Модел. и анализ информ. систем, 2018, том 25, номер 6, страницы 637–666 (Mi mais654)  

Семантика, спецификация и верификация программ

Платформенно-независимая спецификация и верификация стандартной математической функции квадратного корня

Н. В. Шиловa, Д. А. Кондратьевb, И. С. Ануреевb, Е. В. Бодинb, А. В. Промскийb

a Автономная некоммерческая организация высшего образования “Университет Иннополис”, ул. Университетская, 1, г. Иннополис, Республика Татарстан, 420500, Россия
b Институт систем информатики имени А.П. Ершова СО РАН, пр. акад. Лаврентьева, 6, г. Новосибирск, 630090 Россия

Аннотация: Цель проекта “Платформенно-независимый подход к формальной спецификации и верификации стандартных математических функций” — инкрементальный комбинированный подход к спецификации и верификации стандартных математических функций, таких как sqrt, cos, sin и так далее. Платформенно-независимый подход предполагает простую аксиоматизацию машинной арифметики в терминах вещественной арифметики (то есть арифметики поля $\mathbb{R}$ вещественных чисел), не фиксируя ни основание системы счисления, ни формат машинного слова. Инкрементальность означает, что спецификация и верификация начинается с рассмотрения наиболее “простого” случая — элементарной спецификации и верификации простого алгоритма, работающего с вещественными числами, а заканчивается модификацией элементарной спецификации и алгоритма для машинной арифметики и верификацией алгоритма, работающего в машинной арифметике. А комбинированность подхода означает, что мы начинаем с рассмотрения “базового случая” — “ручной” верификации (с ручкой и бумагой) для алгоритма, работающего в вещественной арифметике, затем выполняем ручную верификацию алгоритма, работающего в машинной арифметике, используя верификацию для базового случая в качестве “конспекта” (proof-outlines), а заканчиваем — верификацией с использованием автоматизированной системы построения/поиска доказательства для того, чтобы исключить апелляцию к “очевидности” в ручной верификации. В статье платформенно-независимый инкрементальный комбинированный подход применяется для спецификации и верификации стандартной математической функции квадратного корня. В настоящий момент автоматизированная верификация разработанных алгоритмов выполнена только частично: с использованием системы ACL2 доказана реализуемость (существование) чисел с фиксированной запятой и таблицы начальных приближений квадратного корня.

Ключевые слова: числа с фиксированной запятой, числа с плавающей запятой, машинная арифметика, формальная верификация, частичная и тотальная корректность, тройки Хоара, метод Флойда, точная функция, квадратный корень, метод Ньютона, справочная таблица.

Финансовая поддержка Номер гранта
Российский фонд фундаментальных исследований 17-01-00789_а
Работа поддержана грантом РФФИ 17-01-00789.


DOI: https://doi.org/10.18255/1818-1015-637-666

Полный текст: PDF файл (1150 kB)
Список литературы: PDF файл   HTML файл

Тип публикации: Статья
УДК: 004.052
Поступила в редакцию: 10.09.2018
Исправленный вариант: 15.10.2018
Принята в печать:10.11.2018

Образец цитирования: Н. В. Шилов, Д. А. Кондратьев, И. С. Ануреев, Е. В. Бодин, А. В. Промский, “Платформенно-независимая спецификация и верификация стандартной математической функции квадратного корня”, Модел. и анализ информ. систем, 25:6 (2018), 637–666

Цитирование в формате AMSBIB
\RBibitem{ShiKonAnu18}
\by Н.~В.~Шилов, Д.~А.~Кондратьев, И.~С.~Ануреев, Е.~В.~Бодин, А.~В.~Промский
\paper Платформенно-независимая спецификация и верификация стандартной математической функции квадратного корня
\jour Модел. и анализ информ. систем
\yr 2018
\vol 25
\issue 6
\pages 637--666
\mathnet{http://mi.mathnet.ru/mais654}
\crossref{https://doi.org/10.18255/1818-1015-637-666}


Образцы ссылок на эту страницу:
  • http://mi.mathnet.ru/mais654
  • http://mi.mathnet.ru/rus/mais/v25/i6/p637

    ОТПРАВИТЬ: VKontakte.ru FaceBook Twitter Mail.ru Livejournal Memori.ru


    Citing articles on Google Scholar: Russian citations, English citations
    Related articles on Google Scholar: Russian articles, English articles
  • Моделирование и анализ информационных систем
    Просмотров:
    Эта страница:17
    Полный текст:5
    Литература:3

     
    Обратная связь:
     Пользовательское соглашение  Регистрация  Логотипы © Математический институт им. В. А. Стеклова РАН, 2019