Просмотр кода страницы Логика разделения

'''Логика разделения''', '''сепарационная логика''' ({{lang-en|separation logic}}) в информатике — формальная система, предназначенная для [[формальная верификация|верификации]] программ, содержащих изменяемые структуры данных и [[указатель (программирование)|указатели]], расширение [[Логика Хоара|логики Хоара]]. Разработана {{нп2|Рейнольдс, Джон Чарльз (математик)|Джоном Рейнольдсом|en|John C. Reynolds}}, {{нп2|О’Хирн, Питер|Питером О’Хирном|en|Peter O'Hearn}}, Самином Иштиаком ({{lang-en|Samin Ishtiaq}}) и Хонсёком Яном ({{lang-en|Hongseok Yang}}){{sfn|Reynolds|2002}}<ref name="sl1999">Intuitionistic Reasoning about Shared Mutable Data Structure. John Reynolds. Millennial Perspectives in Computer Science, Proceedings of the 1999 Oxford-Microsoft Symposium in Honour of Sir Tony Hoare</ref><ref name="popl01">BI as an Assertion Language for Mutable Data Structures. Samin Ishtiaq, Peter O’Hearn. POPL 2001.</ref><ref name="csl01">[http://www.eecs.qmul.ac.uk/~ohearn/papers/localreasoning.pdf Local Reasoning about Programs that Alter Data Structures.] {{Wayback|url=http://www.eecs.qmul.ac.uk/~ohearn/papers/localreasoning.pdf |date=20130927111107 }} Peter O’Hearn, John Reynolds, Hongseok Yang. CSL 2001</ref> на основе работ {{нп2|Бёрстол, Род|Рода Бёрстола|en|Rod Burstall}}<ref name="burstall">Some techniques for proving programs which alter data structures. R.M. Burstall. Machine Intelligence 7, 1972.</ref>. Язык утверждений логики разделения является специальным случаем {{нп2|логика пучковых импликаций|логики пучковых импликаций|en|Bunched logic|logic of bunched implications}}<ref name="bi">The Logic of Bunched Implications P.W. O’Hearn and D. J. Pym. Bulletin of Symbolic Logic , 5(2), June 1999, pp215-244</ref>.

Технологии, основанные на логике разделения, позволяют разрабатывать системы для верификации крупных программных проектов{{sfn|Lee, Park|2014}}.

== Предпосылки создания ==
[[Логика Хоара]] имеет ряд ограничений, работая только с изменяемыми переменными и не поддерживая процедуры или [[Объект первого класса|код первого класса]]. Тем не менее, самое большое ограничение — это отсутствие поддержки [[Указатель (тип данных)|указателей]], что наиболее актуально для спецификации [[императивное программирование|императивных программ]]. В случае использования указателей и [[Куча (память)|кучи]] от изменяемых переменных можно отказаться, присваивая [[локальная переменная|локальным переменным]] значение-указатель лишь один раз{{sfn|Programs and Proofs|2014}}.

В 2000—2002 годах Джон Рейнольдс и Питер О’Хирн придумали расширение логики Хоара — логику разделения. Первоначальной идеей было упрощение рассуждений об императивных программах низкого уровня с общей изменяемой структурой данных{{sfn|Reynolds|2008}}. Сам термин связан с основной идеей данной логики — описанием разделения хранилища ({{lang-en|storage}}) на непересекающиеся компоненты. Термин используется как в отношении [[исчисление предикатов|исчисления предикатов]], расширенного ''оператором разделения'', так и для результата расширения хоаровской логики{{sfn|Reynolds|2002}}.

== Описание ==
Ключевой особенностью логики разделения является возможность ''локальных рассуждений'' (local reasoning) благодаря наличию в утверждениях пространственных связок ({{lang-en|spatial connectives}}) между частями кучи{{sfn|Parkinson, Bierman|2005}}.

[[Файл:Separation logic store and heap.svg|300px|мини|Соответствует утверждению <math>x \mapsto 4 * 4 \mapsto y * y \mapsto 6</math><ref>''Chris Poskitt'' [http://chrisposkitt.com/files/teaching/SV_SeparationLogic_1-2.pdf Software Verification (Fall 2013) Lecture 5: Separation Logic Parts I - II]{{Недоступная ссылка|date=Июль 2018 |bot=InternetArchiveBot }}</ref>]]
Логика позволяет работать с утверждениями вида <math>s, h \models P</math>, где:
* <math>s</math> — память (например, в виде [[стек]]а{{sfn|Reynolds|2002}}), конечное [[функция (математика)#Частично определённые функции|частичное функциональное отображение]] из переменных в [[целое число|целые]], 
* <math>h</math> — куча, конечное частичное функциональное отображение из целых в целые, а 
* <math>P</math> — [[Высказывание (логика)|утверждение]] о памяти и куче, то есть, о состоянии программы{{sfn|A Primer on Separation Logic|2012}}.

Для преодоления громоздких описаний запретов на использование одного и того же адреса разными объектами, введена новая логическая операция — '''''разделяющая конъюнкция''''' (disjoint conjunction), обозначаемая <math>P\ *\ Q</math> (или <math>P\ \land\!*\ Q</math><ref>{{cite conference
 | author = Tjark Weber
 | year = 2004
 | conference = Lecture Notes in Computer Science
 | title = Towards Mechanized Program Verification with Separation Logic
 | booktitle = Computer Science Logic~-- 18th International Workshop, CSL 2004, 13th Annual Conference of the EACSL, Karpacz, Poland, September 2004, Proceedings
 | accessdate = 2013-12-06
 | pages = 250--264
 | id = weber04towards
 | publisher = Springer
}}
</ref>) и утверждающая, что каждое из условий <math>P</math> и <math>Q</math> выполняются в своей части кучи (адресуемого хранилища){{sfn|Reynolds|2008}}<ref>''Matthew J. Parkinson'' [http://www.cl.cam.ac.uk/techreports/UCAM-CL-TR-654.pdf Local reasoning for Java], 2005, UCAM-CL-TR-654, ISSN 1476—2986</ref>. То есть, <math>P\ *\ Q</math> истинна для кучи <math>h</math>, если существуют две части этой кучи <math>h_1</math> и <math>h_2</math>, для которых выполнено<ref>[http://lara.epfl.ch/w/sav07_lecture_24 Lecture 24: Pointer and shape analysis], LARA, EPFL</ref>:
* Области <math>h_1</math> и <math>h_2</math> не пересекаются;
* <math>h</math> является объединением <math>h_1</math> и <math>h_2</math>;
* <math>P</math> верно для всех адресов из <math>h_1</math>;
* <math>Q</math> верно для всех адресов из <math>h_2</math>.

Выше под <math>h_1</math> и <math>h_2</math> понимаются [[Функция (математика)#Частично определённые функции|частичные функции]], дающие значения, соответствующие адресу в куче.

Для утверждения, что куча пуста, введён предикат <math>emp</math> (при этом очевидно выполняется <math>P \ *\ emp\ \Leftrightarrow\ P</math>), а для обозначения указателя — <math>e \mapsto x</math>. Например, в следующей, являющейся одной из аксиом, [[Тройка Хоара|тройке Хоара]]

: <math>\{E \mapsto -\}\ [E] := F \ \{E \mapsto F\}</math>

предусловием является неиспользованность ячейки памяти, которая в результате операции присваивания указывает на ''F'', что и утверждается в постусловии{{sfn|A Primer on Separation Logic|2012}}.

Ключевым для локальных рассуждений является введённое О’Хирном '''''рамочное правило''''' (frame rule){{sfn|Reynolds|2002}}:

: <math>\frac{\{P\}\ C\ \{Q\}}{\{P \ast R\}\ C\ \{Q \ast R\}}~\mathsf{mod}(C) \cap \mathsf{fv}(R) =\emptyset</math>,

в котором никакая свободная переменная ({{lang-en|'''f'''ree '''v'''ariable}}) в <math>R</math> не изменяется ({{lang-en|'''mod'''ified}}) под влиянием команды <math>C</math>. Используя это правило, можно добавлять произвольные предикаты о переменных и частях кучи, которые не изменяются командой <math>C</math>. При этом О’Хирн назвал объём занимаемой кучи, затрагиваемой командой, термином {{lang-en|footprint}} («отпечаток»). Назначением рамочного правила является расширение рассуждения с более локального описания команды на более глобальное описание объемлющей команды — команды с бо́льшим отпечатком{{sfn|Reynolds|2002}}.

Установив, что логика разделения является примером логики пучковых импликаций, Ян и Иштиак ввёл '''''разделяющую импликацию''''' ({{lang-en|separating implication}}{{sfn|Reynolds|2002}}, {{lang-en|magic wand}}). Обозначение <math>P -\!\!\!\ast\, Q</math> говорит о том, если куча была расширена непересекающейся с ней кучей, для которой верно <math>P</math>, то для получившейся в результате кучи будет верно <math>Q</math>{{sfn|Lee, Park|2014}}.

Семантика логических связок (разделяющей конъюнкции и разделяющей импликации) подразумевает [[моноид]]ную структуру кучи{{sfn|Lee, Park|2014}}.

Локальные рассуждения можно понимать и в терминах '''''передачи принадлежности''''' ({{lang-en|ownership transfer}}). Легче всего рассмотреть передачу принадлежности на примере правил [[Монитор (синхронизация)#Семантика Хоара и Mesa|монитора Хоара]] (можно увидеть, что логика разделения подходит и для [[Распределённая система|распределённых]] систем). Для входа процесса в [[Критическая секция|критическую секцию]] применяется разделяющая конъюнкция с <math>I_r</math>, где <math>I_r</math> — инвариант ресурса ''r''. По выходу из критической секции логический вывод следует в обратном направлении<ref name="Lozes">Étienne Lozes [http://www.lsv.ens-cachan.fr/~lozes/draft-info.pdf|Towards Information as Resource in Separation Logic]{{Недоступная ссылка|date=Июль 2018 |bot=InternetArchiveBot }}, ANR project, draft</ref>:

: <math>\frac{\{P \ast I_r\}\ C\ \{Q \ast I_r\}}{\{P\}\ \mathsf{with}\ r\ \mathsf{do}\ C\ \{Q\}}</math>,

По аналогии можно рассматривать и процесс обработки процессом сообщения, отправленного другим процессом с делегированными данному процессу ресурсами, определяемыми отпечатками<ref name="Lozes" />.

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

* Ynot<ref>[http://ynot.cs.harvard.edu/ Ynot]</ref> — библиотека для верификации императивных программ для [[Coq]].
* Predator<ref>[http://www.fit.vutbr.cz/research/groups/verifit/tools/predator/ Predator]</ref> — это анализатор программ на основе логики разделения для анализа программ, содержащих динамические списки<ref>{{статья|автор=Мутилин В. С., Новиков Е. М., Хорошилов А. В.|заглавие=Обзор инструментов статической верификации Си программ в применении к драйверам устройств операционной системы Linux|издание=Труды Института системного программирования РАН|год=2012|том=22|номер=3|страницы=293-326}}</ref>.

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

По характеру использования системы можно разделить следующим образом<ref>''Cliff Jones'' (from U. Newcastle), ''Viktor Vafeiadis'' (from MPI-SWS) [https://www.mpi-sws.org/~viktor/rgsl-tutorial/part1.pdf Rely-guarantee thinking & separation logic]</ref>:
* Пользователь вручную пишет как [[язык спецификаций|спецификацию]], так и доказательства, используя тактики: интерактивные системы доказательства теорем Coq, HOL4, Isabelle/HOL.
* Пользователь пишет спецификацию и [[Инвариант цикла|инварианты циклов]]: самостоятельные инструменты для верификации Smallfoot, HIP, Verifast, Jstar.
* Пользователь пишет только спецификацию (или даже ничего не пишет): инструменты для {{нп2|анализ формы|анализа формы|en|shape analysis (program analysis)|shape analysis}} Space Invader, THOR, Xisa, SLAyer.

== Примечания ==
{{примечания|2}}

== Литература ==
* {{source|Q22237685|ref=Reynolds|ref-year=2002}} <!-- Separation Logic: A Logic for Shared Mutable Data Structures // LICS '02 -->
* {{source|Q22244855|ref=Reynolds|ref-year=2008}} <!-- An Overview of Separation Logic // Verified Software: Theories, Tools, Experiments -->
* {{source|Q22244930|ref=Parkinson, Bierman|ref-year=2005}} <!-- Separation Logic and Abstraction // POPL '05; ACM SIGPLAN Notices -->
* {{статья
 |автор         = Lee, Wonyeol and Park, Sungwoo
 |заглавие      = A Proof System for Separation Logic with Magic Wand
 |ссылка        = http://doi.acm.org/10.1145/2578855.2535871
 |язык          = en
 |издание       = SIGPLAN Not.
 |издательство  = ACM
 |тип           =
 |год           = 2014
 |том           = 49
 |номер         = 1
 |страницы      = 477--490
 |doi           = 
 |issn          = 0362-1340
 |ref           = Lee, Park
}}
* {{source|Q27976187|ref=Appel, Dockins, Hobor et al.|ref-year=2014}} <!-- Program Logics for Certified Compilers -->
* {{книга|автор=Ilya Sergey|заглавие=Programs and Proofs: Mechanizing Mathematics with Dependent Types|ссылка=http://ilyasergey.net/pnp/|год=2014|серия=Lecture Notes|ref=Programs and Proofs|часть=8.2 Basics of Separation Logic}}
* {{публикация|статья|автор=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|volume=33|pages=286—318|ref=A Primer on Separation Logic}}

== Ссылки ==
* ''Cliff Jones'' ([[Newcastle University]]), ''Viktor Vafeiadis'' ([[:en:Max Planck Institute for Software Systems|MPI-SWS]]) [https://www.mpi-sws.org/~viktor/rgsl-tutorial/part1.pdf Rely-guarantee thinking & separation logic]{{ref-en}} — презентация, хорошо иллюстрирующая понятия логики разделения
* Matthew Parkinson [http://www.cl.cam.ac.uk/~mjp41/MiniCourse.pdf An Introduction to Separation Logic]{{ref-en}} — презентация, в которой иллюстрированы все основные аспекты логики разделения: аксиомы, примеры программ с соответствующими диаграммами, синтаксис

{{Добротная статья|Теория информации и криптография}}


[[Категория:Математическая логика]]
[[Категория:Информатика]]
[[Категория:Формальные методы]]