Головная страница ИПМ Библиотеки, издания  •  Поиск публикаций  English 
Публикация

Диссертация, Москва, 2017
На соискание ученой степени: кандидат физико-математических наук
Специальность: 05.13.11 - математическое и программное обеспечение вычислительных машин, комплексов и компьютерных сетей
Диссертационный совет: Д 002.024.01
Автор: Гречаник С.А.
Доказательство свойств функциональных программ методом насыщения равенствами
Аннотация:
Цель работы — исследовать возможность применения комбинации методов насыщения равенствами и многорезультатной суперкомпиляции для выявления и доказательства свойств программ на нестрогом функциональном языке первого порядка. Настоящая работа показывает, что на основе метода насыщения равенствами и преобразований из суперкомпиляции можно построить систему преобразования функциональных программ, применимую для доказательства эквивалентности. Показано, что при этом удаётся избежать проблемы, связанной с комбинаторным взрывом количества функций, отличающихся только порядком аргументов. Также было показано, что можно сформулировать принцип индукции как специальное преобразование, работающее в рамках системы насыщения.
Ключевые слова:
функциональные программы, метод насыщения равенствами, суперкомпиляция, многорезультатная суперкомпиляция
Язык публикации: русский,  страниц: 215
Направление исследований:
Программирование, параллельные вычисления, мультимедиа
Полный текст на русском языке: Сведения об авторах:
  • Гречаник Сергей Александрович,  ,  ИПМ им. М.В. Келдыша РАН