Динамическая логика разделений и ее использование в образовании

  • Evgeny Maratovich Makarov Национальный исследовательский Нижегородский государственный университет им. Н.И. Лобачевского http://orcid.org/0000-0003-0399-0946

Аннотация

Математическая логика широко применяется для верификации программ и аппаратного обеспечения. Одной из логик, наиболее подходящих для верификации императивных программ, является логика Хоара. Ее расширение, логика разделений, использует разделяющую конъюнкцию, которая позволяет рассуждать о программах, использующих указатели и изменяемые структуры данных. Еще одним формализмом, используемым в верификации, является динамическая логика — частный случай модальной логики. Данная статья описывает пропозициональную динамическую логику разделений, которая добавляет разделяющую конъюнкцию к динамической логике.
Мы описываем синтаксис, семантику и исчисление в гильбертовском стиле для пропозициональной динамической логики разделений и доказываем ее корректность. Определение логики является достаточно абстрактным. Так, используемый язык программирования состоит из так называемых регулярных программ вместо программ с обычными конструкциями if и while. Множество атомарных программ может быть произвольным при условии, что они порождают локальные действия. Особое внимание уделяется корректности правила кадра, позволяющего писать локальные спецификации программ, то есть указывать участки памяти, которые непосредственно читаются или изменяются программой. Условные операторы также рассматриваются отлично от стандартной динамической логики.
Статья также содержит аргументы в пользу использования логики разделений в изучении компьютерных наук. Данная логика более проста, чем другие субструктурные логики, и может преподаваться даже в начальных курсах математический логики. В то же время, логика разделений является областью активных исследований с большим количеством применений. На основе этой логики построено много инструментов для верификации. Поэтому она является отличным введением в формальные методы.

Сведения об авторе

Evgeny Maratovich Makarov, Национальный исследовательский Нижегородский государственный университет им. Н.И. Лобачевского

старший преподаватель кафедры алгебры, геометрии и дискретной математики, Институт информационных технологий, математики и механики

Опубликована
2020-11-30
Как цитировать
MAKAROV, Evgeny Maratovich. Динамическая логика разделений и ее использование в образовании. Международный научный журнал «Современные информационные технологии и ИТ-образование», [S.l.], v. 16, n. 3, nov. 2020. ISSN 2411-1473. Доступно на: <http://sitito.cs.msu.ru/index.php/SITITO/article/view/696>. Дата доступа: 21 apr. 2021
Раздел
Теоретические вопросы информатики, прикладной математики, компьютерных наук