Dynamic Separation Logic and its Use in Education
Authors: Makarov E.M. 
Published: December 2024

Mathematical logic is widely used in hardware and software verification. Hoare logic is particularly suitable for reasoning about imperative programs. Its extension, separation logic, introduces the separating conjunction, which makes it possible to reason about programs working with pointers and mutable data structures. Dynamic logic, an example of modal logic, is yet another formalism used for verification. This article introduces propositional dynamic separation logic, which adds separating conjunction to dynamic logic. We describe syntax, semantics and Hilbert-style deductive system for propositional dynamic separation logic and prove its soundness. The definition of the logic is rather abstract. Thus, the programming language consists of so-called regular programs rather than while-programs, and the set of atomic commands can be arbitrary as long as they correspond to local actions. Special attention is devoted to the soundness of the frame rule, which allows writing program specification using a small footprint, i.e., specifying exactly the portion of the heap that the program reads or writes. Programs that perform tests are also treated differently from regular dynamic logic. The article also argues for the use of separation logic in computer science curriculum. It is more intuitive that other substructural logics and can be taught even in introductory logic courses. At the same time, it is an active research area with numerous verification tools built on its foundation. Therefore, it serves an excellent introduction to formal methods.

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