Введение

В информатике логика разделения является расширением логики Хоара, способом рассуждения о программах. Она была разработана Джоном К. Рейнольдсом, Питером О’Харном, Самином Иштиаком и Хонсеком Яном, опираясь на ранние работы Рода Берсталла. Язык утверждений логики разделения является частным случаем логики связующих импликаций (BI). Обзорная статья в журнале CACM, написанная О’Харном, описывает развитие этой области до начала 2019 года.

Утверждения: операторы и семантика

Логические утверждения разделения описывают "состояния", состоящие из хранилища и кучи, примерно соответствующие состоянию локальных (или выделенных в стеке) переменных и динамически выделенных объектов в общих языках программирования, таких как C и Java. Хранилище – это функция, отображающая переменные в значения. Куча – это частичная функция, отображающая адреса памяти в значения. Две кучи и являются раздельными (обозначаются как ⊓) если их области определения не пересекаются (т.е. для каждого адреса памяти , по крайней мере, одна из и не определена). Логика позволяет доказывать суждения вида , где – хранилище, – куча, а – утверждение относительно данного хранилища и кучи. Утверждения логики разделения (обозначаемые как , , ) содержат стандартные булевы связки и, кроме того, , , и , где и – выражения. Константа утверждает, что куча пуста, т.е. не определена для всех адресов. Бинарный оператор принимает адрес и значение и утверждает, что куча определена ровно в одной точке, отображая данный адрес в данное значение. Т.е. когда (где обозначает значение выражения , вычисленное в хранилище ) и в противном случае не определена. Бинарный оператор (произносится как "звезда" или разделяющая конъюнкция) утверждает, что кучу можно разделить на две раздельные части, в которых выполняются, соответственно, его два аргумента. Т.е. когда существует такая , что и и и . Бинарный оператор (произносится как "волшебная палочка" или разделяющее следствие) утверждает, что расширение кучи раздельной частью, удовлетворяющей его первому аргументу, приводит к куче, удовлетворяющей его второму аргументу. Т.е. когда для каждой кучи , такой что , также выполняется . Операторы и имеют некоторые свойства, общие с классическими операторами конъюнкции и импликации. Их можно комбинировать с помощью правила вывода, аналогичного modus ponens, и они образуют сопряжение, т.е. если и только если для ; точнее, сопряженные операторы – это и .

Решимость и сложность

Проблема выполнимости для фрагмента логики разделения, не содержащего кванторов, многосортного и параметризованного по сортам местоположений и данных, может быть доказана PSPACE-полной. Алгоритм решения этого фрагмента, основанный на DPLL(T), был интегрирован в cvc5. Расширяя этот результат, выполнимость для аналога класса Бернейса — Шёнфинкеля для логики разделения с неинтерпретированными ячейками памяти также может быть доказана PSPACE-полной, в то время как проблема становится неразрешимой при использовании интерпретированных ячеек памяти (например, целых чисел) или дополнительных чередованиях кванторов.