Введение к работе
Актуальность темы. Одной из ключевых проблем теоретичес-ого и практического программирования является проблема ерификации. которая состоит в том, чтобы по заданным твэрждениям а и ft о программе р доказать истинность Р после ыполнения р при условии, что перед ее выполнением истинно «. общем случае проблема эта алгоритмически неразрешима, а оиск решений в частных случаях требует глубокого предваря-ельного анализа. В работах Флойда и Хоара было показано, то верификация программы сводится к нахождению существенных нвариантов для определенных ее точек, то есть таких утвер-дения, которые выполняются всякий раз при прохождении через ги точки процесса вычисления.
А. А. Летичевским был предложен метод автоматического оиска инвариантов из текста программы с учетом структуры лгебры данных. В работах его учеников этот метод был рименен к ряду конкретных алгебр. Указанные исследования роводились для программ с простои памятью.
В данной работе предлагается развитие метода автомати-эского поиска инвариантов применительно к программам с улевыми массивами, что принципиальным образом расширяет Зласть его применения. Последнее особенно актуально в зязи с получающими все более широкое распространение авто-атическими системами распознавания визуальных и речевых анных. составления экономических планов и расчетов, раз-їботки игровых стратегии и т. д., использующими булевые ассивы больших размеров.
Цель работы. Целью диссертационной работы является ізработка базовых алгоритмов для методов верификации и химизации программ» работающих с булевыми массивами. )лее конкретно
- построение математической модели для программ с
глевыми массивами;
- выбор представляющих практический интерес форм инва-
тнтов;
- разработка алгоритмов поиска инвариантов заданной
>рмы.
Методика исследований. Методологическим стержнем работы іляется техника отыскания неподвижных точек систем функцио-
нальных уравнений, заданных на частично упорядоченных мно жествах. Применение этой техники основано на всесторонне! использовании понятий и методов теории множеств, абстрактно: и булевой алгебры.
Научная новизна. Построена математическая модель дл: программ с булевыми массивами в рамках которой разработан) методы автоматического поиска инвариантов определенны: типов. Это существенно расширяет класс программ, к которьн можно применить имеющиеся методы верификации и оптимизации Описан класс линейных программ, допускающих зФФективнуї верификацию относительно условий, заданных в форме константны: равенств.
Практическая ценность работы. Полученные в работе резуль
таты могут быть использованы для создания автоматически:
систем диагностики и оптимизации прикладного и системное
программного обеспечения. Их можно использовать также дл,
организации параллельных процессов обработки информации
Результат по верификации линейных программ может послужит
основой автоматического проектирования тестов для аппаратны:
и программных средств. »
Аппробаїшя работы и публикации. Основные положения : результаты работы обсуждались и докладывались на семинара: по теории автоматов и автоматизации программирования Институте кибернетики им. В. М. Глушкова АН Украины, на семи нарах по теоретическому программированию в Киевском и Ереван ском госуниверситетах. на Закавказской научно-техническо конференции молодых ученых и специалистов "Информатика вычислительная техника", на общем семинаре Института пробле] информатики и автоматизации НАН Армении, на заседани Армянского Математического Общества.
По теме диссертации опубликованы 4 научные статьи.
Структура работы. Диссертационная работа состоит и введения, четырех глав', заключения и списка цитируемо литературы из 42 наименований. Объем работы составляет 7 страницы печатного текста.