WikiSort.ru - Не сортированное

Логика разделения, сепарационная логика (англ. separation logic) в информатике — формальная система, предназначенная для верификации программ, содержащих изменяемые структуры данных и указатели, расширение логики Хоара. Разработана Джоном Рейнольдсом (англ. John C. Reynolds), Питером О’Хирном (англ. Peter O'Hearn), Самином Иштиаком (англ. Samin Ishtiaq) и Хонсёком Яном (англ. Hongseok Yang)^[1][2][3][4] на основе работ Рода Бёрстола (англ. Rod Burstall)^[5]. Язык утверждений логики разделения является специальным случаем логики пучковых импликаций (англ. logic of bunched implications)^[6].

Технологии, основанные на логике разделения, позволяют разрабатывать системы для верификации крупных программных проектов^[7].

Предпосылки создания

Логика Хоара имеет ряд ограничений, работая только с изменяемыми переменными и не поддерживая процедуры или код первого класса. Тем не менее, самое большое ограничение — это отсутствие поддержки указателей, что наиболее актуально для спецификации императивных программ. В случае использования указателей и кучи от изменяемых переменных можно отказаться, присваивая локальным переменным значение-указатель лишь один раз^[8].

В 2000—2002 годах Джон Рейнольдс и Питер О’Хирн придумали расширение логики Хоара — логику разделения. Первоначальной идеей было упрощение рассуждений об императивных программах низкого уровня с общей изменяемой структурой данных^[9]. Сам термин связан с основной идеей данной логики — описанием разделения хранилища (англ. storage) на непересекающиеся компоненты. Термин используется как в отношении исчисления предикатов, расширенного оператором разделения, так и для результата расширения хоаровской логики^[1].

Описание

Ключевой особенностью логики разделения является возможность локальных рассуждений (local reasoning) благодаря наличию в утверждениях пространственных связок (англ. spatial connectives) между частями кучи^[10].

Логика позволяет работать с утверждениями вида ${\displaystyle s,h\models P}$ , где:

• ${\displaystyle s}$  — память (например, в виде стека^[1]), конечное частичное функциональное отображение из переменных в целые,
• ${\displaystyle h}$  — куча, конечное частичное функциональное отображение из целых в целые, а
• ${\displaystyle P}$  — утверждение о памяти и куче, то есть, о состоянии программы^[12].

Для преодоления громоздких описаний запретов на использование одного и того же адреса разными объектами, введена новая логическая операция — разделяющая конъюнкция (disjoint conjunction), обозначаемая ${\displaystyle P\ *\ Q}$ (или ${\displaystyle P\ \land \!*\ Q}$ ^[13]) и утверждающая, что каждое из условий ${\displaystyle P}$ и ${\displaystyle Q}$ выполняются в своей части кучи (адресуемого хранилища)^[9][14]. То есть, ${\displaystyle P\ *\ Q}$ истинна для кучи ${\displaystyle h}$ , если существуют две части этой кучи ${\displaystyle h_{1}}$ и ${\displaystyle h_{2}}$ , для которых выполнено^[15]:

• Области ${\displaystyle h_{1}}$ и ${\displaystyle h_{2}}$ не пересекаются;
• ${\displaystyle h}$ является объединением ${\displaystyle h_{1}}$ и ${\displaystyle h_{2}}$ ;
• ${\displaystyle P}$ верно для всех адресов из ${\displaystyle h_{1}}$ ;
• ${\displaystyle Q}$ верно для всех адресов из ${\displaystyle h_{2}}$ .

Выше под ${\displaystyle h_{1}}$ и ${\displaystyle h_{2}}$ понимаются частичные функции, дающие значения, соответствующие адресу в куче.

Для утверждения, что куча пуста, введён предикат ${\displaystyle emp}$ (при этом очевидно выполняется ${\displaystyle P\ *\ emp\ \Leftrightarrow \ P}$ ), а для обозначения указателя — ${\displaystyle e\mapsto x}$ . Например, в следующей, являющейся одной из аксиом, тройке Хоара

${\displaystyle \{E\mapsto -\}\ [E]:=F\ \{E\mapsto F\}}$

предусловием является неиспользованность ячейки памяти, которая в результате операции присваивания указывает на F, что и утверждается в постусловии^[12].

Ключевым для локальных рассуждений является введённое О’Хирном рамочное правило (frame rule)^[1]:

${\displaystyle {\frac {\{P\}\ C\ \{Q\}}{\{P\ast R\}\ C\ \{Q\ast R\}}}~{\mathsf {mod}}(C)\cap {\mathsf {fv}}(R)=\emptyset }$ ,

в котором никакая свободная переменная (англ. free variable) в ${\displaystyle R}$ не изменяется (англ. modified) под влиянием команды ${\displaystyle C}$ . Используя это правило, можно добавлять произвольные предикаты о переменных и частях кучи, которые не изменяются командой ${\displaystyle C}$ . При этом О’Хирн назвал объём занимаемой кучи, затрагиваемой командой, термином англ. footprint («отпечаток»). Назначением рамочного правила является расширение рассуждения с более локального описания команды на более глобальное описание объемлющей команды — команды с бо́льшим отпечатком^[1].

Установив, что логика разделения является примером логики пучковых импликаций, Ян и Иштиак ввёл разделяющую импликацию (англ. separating implication^[1], англ. magic wand). Обозначение ${\displaystyle P-\!\!\!\ast \,Q}$ говорит о том, если куча была расширена непересекающейся с ней кучей, для которой верно ${\displaystyle P}$ , то для получившейся в результате кучи будет верно ${\displaystyle Q}$ ^[7].

Семантика логических связок (разделяющей конъюнкции и разделяющей импликации) подразумевает моноидную структуру кучи^[7].

Локальные рассуждения можно понимать и в терминах передачи принадлежности (англ. ownership transfer). Легче всего рассмотреть передачу принадлежности на примере правил монитора Хоара (можно увидеть, что логика разделения подходит и для распределённых систем). Для входа процесса в критическую секцию применяется разделяющая конъюнкция с ${\displaystyle I_{r}}$ , где ${\displaystyle I_{r}}$  — инвариант ресурса r. По выходу из критической секции логический вывод следует в обратном направлении^[16]:

${\displaystyle {\frac {\{P\ast I_{r}\}\ C\ \{Q\ast I_{r}\}}{\{P\}\ {\mathsf {with}}\ r\ {\mathsf {do}}\ C\ \{Q\}}}}$ ,

По аналогии можно рассматривать и процесс обработки процессом сообщения, отправленного другим процессом с делегированными данному процессу ресурсами, определяемыми отпечатками^[16].

Применение и реализации

Логика разделения нашла применение в автоматических и интерактивных верификаторах программного обеспечения, написанного в императивном и объектно-ориентированном стиле. Для этого были разработаны соответствующие дополнения к существующим инструментам верификации, например, таких как:

• Ynot^[17] — библиотека для верификации императивных программ для Coq.
• Predator^[18] — это анализатор программ на основе логики разделения для анализа программ, содержащих динамические списки^[19].

Другие системы, использующие логику разделения: Smallfoot, Space Invader, THOR, SLAyer, HIP, jStar, Xisa, VeriFast, Infer, SeLoger, SLP. Тем не менее, по состоянию на 2014 год отсутствуют практичные доказатели теорем, реализующие полную логику разделения, то есть включающие разделяющую импликацию^[7].

По характеру использования системы можно разделить следующим образом^[20]:

• Пользователь вручную пишет как спецификацию, так и доказательства, используя тактики: интерактивные системы доказательства теорем Coq, HOL4, Isabelle/HOL.
• Пользователь пишет спецификацию и инварианты циклов: самостоятельные инструменты для верификации Smallfoot, HIP, Verifast, Jstar.
• Пользователь пишет только спецификацию (или даже ничего не пишет): инструменты для анализа формы (англ. shape analysis) Space Invader, THOR, Xisa, SLAyer.

Примечания

Литература

• Reynolds J. C. Separation Logic: A Logic for Shared Mutable Data Structures // LICS '02: Proceedings of the 17th Annual IEEE Symposium on Logic in Computer Science — Washington, DC, USA: IEEE Computer Society, 2002. — P. 55–74. — ISBN 978-0-7695-1483-3 — doi:10.1109/LICS.2002.1029817
  <a href='https://wikidata.org/wiki/Track:Q22237680'></a><a href='https://wikidata.org/wiki/Track:Q669561'></a><a href='https://wikidata.org/wiki/Track:Q3719620'></a><a href='https://wikidata.org/wiki/Track:Q22237685'></a>
• Reynolds J. C. An Overview of Separation Logic // Verified Software: Theories, Tools, Experiments: First IFIP TC 2/WG 2.3 Conference, VSTTE 2005, Zurich, Switzerland, October 10-13, 2005, Revised Selected Papers and Discussions / B. Meyer, J. Woodcock — Berlin: Springer Berlin Heidelberg, 2008. — P. 460–469. — (Lecture Notes in Computer Science; Vol. 4171) — ISBN 978-3-540-69147-1 — ISSN 0302-9743 — doi:10.1007/978-3-540-69149-5_49
  <a href='https://wikidata.org/wiki/Track:Q22244830'></a><a href='https://wikidata.org/wiki/Track:Q924044'></a><a href='https://wikidata.org/wiki/Track:Q3719620'></a><a href='https://wikidata.org/wiki/Track:Q64'></a><a href='https://wikidata.org/wiki/Track:Q22244855'></a><a href='https://wikidata.org/wiki/Track:Q6199027'></a><a href='https://wikidata.org/wiki/Track:Q92946'></a><a href='https://wikidata.org/wiki/Track:Q21587985'></a>
• Parkinson M., Bierman G. Separation Logic and Abstraction // POPL '05: Proceedings of the 32nd ACM SIGPLAN-SIGACT symposium on Principles of programming languages Long Beach, CA, USA January 12-14, 2005 — New York, NY, USA: ACM, 2005. — P. 247–258. — ISBN 978-1-58113-830-6 — doi:10.1145/1040305.1040326
  <a href='https://wikidata.org/wiki/Track:Q22244929'></a><a href='https://wikidata.org/wiki/Track:Q22244930'></a><a href='https://wikidata.org/wiki/Track:Q22244879'></a><a href='https://wikidata.org/wiki/Track:Q22244875'></a>
• Lee, Wonyeol and Park, Sungwoo. A Proof System for Separation Logic with Magic Wand (англ.) // SIGPLAN Not.. — ACM, 2014. — Vol. 49, no. 1. — P. 477--490. — ISSN 0362-1340.
• Appel A., Dockins R., Hobor A. et al. Program Logics for Certified Compilers — Cambridge University Press, 2014. — 472 p. — ISBN 978-1-107-04801-0
  <a href='https://wikidata.org/wiki/Track:Q4756213'></a><a href='https://wikidata.org/wiki/Track:Q912887'></a><a href='https://wikidata.org/wiki/Track:Q27976169'></a><a href='https://wikidata.org/wiki/Track:Q27976168'></a><a href='https://wikidata.org/wiki/Track:Q27976173'></a><a href='https://wikidata.org/wiki/Track:Q27976187'></a>
• Ilya Sergey. 8.2 Basics of Separation Logic // Programs and Proofs: Mechanizing Mathematics with Dependent Types. — 2014. — (Lecture Notes).
• Peter W. O’Hearn. A Primer on Separation Logic (and Automatic Program Verification and Analysis) // Software Safety and Security; Tools for Analysis and Verification. — 2012. — Vol. 33. — P. 286—318.

Ссылки

• Cliff Jones (Newcastle University), Viktor Vafeiadis (MPI-SWS) Rely-guarantee thinking & separation logic (англ.) — презентация, хорошо иллюстрирующая понятия логики разделения
• Matthew Parkinson An Introduction to Separation Logic (англ.) — презентация, в которой иллюстрированы все основные аспекты логики разделения: аксиомы, примеры программ с соответствующими диаграммами, синтаксис

Эта статья входит в число добротных статей русскоязычного раздела Википедии.