Русская Википедия:Логика разделения

Материал из Онлайн справочника
Перейти к навигацииПерейти к поиску

Логика разделения, сепарационная логика (Шаблон:Lang-en) — формальная система, субструктурная логика, применимая к верификации программ, содержащих изменяемые структуры данных и указатели, расширение логики Хоара. Разработана Шаблон:Нп2, Шаблон:Нп2, Самином Иштиаком (Шаблон:Lang-en) и Хонсёком Яном (Шаблон:Lang-en)Шаблон:Sfn[1][2][3] на основе работ Шаблон:Нп2[4]. Язык утверждений логики разделения является специальным случаем Шаблон:Нп2[5].

Развитием логики разделения для параллельных вычислений с общей памятью является параллельная логика разделенияШаблон:Переход, разработанная О’Хирном и Шаблон:Нп2.

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

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

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

В 2000—2002 годах Джон Рейнольдс и Питер О’Хирн придумали расширение логики Хоара — логику разделения. Первоначальной идеей было упрощение рассуждений об императивных программах низкого уровня с общей изменяемой структурой данныхШаблон:Sfn. Сам термин связан с основной идеей данной логики — описанием разделения хранилища (Шаблон:Lang-en) на непересекающиеся компоненты. Термин используется как в отношении исчисления предикатов, расширенного оператором разделения, так и для результата расширения хоаровской логикиШаблон:Sfn.

Описание

Ключевой особенностью логики разделения является возможность локальных рассуждений (local reasoning) благодаря наличию в утверждениях пространственных связок (Шаблон:Lang-en) между частями кучиШаблон:Sfn.

Файл:Separation logic store and heap.svg
Соответствует утверждению <math>x \mapsto 4 * 4 \mapsto y * y \mapsto 6</math>[6]

Логика позволяет работать с утверждениями вида <math>s, h \models P</math>, где:

Для преодоления громоздких описаний запретов на использование одного и того же адреса разными объектами, введена новая логическая операция — разделяющая конъюнкция (disjoint conjunction), обозначаемая <math>P\ *\ Q</math> (или <math>P\ \land\!*\ Q</math>[7]) и утверждающая, что каждое из условий <math>P</math> и <math>Q</math> выполняются в своей части кучи (адресуемого хранилища)Шаблон:Sfn[8]. То есть, <math>P\ *\ Q</math> истинна для кучи <math>h</math>, если существуют две части этой кучи <math>h_1</math> и <math>h_2</math>, для которых выполнено[9]:

  • Области <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.

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

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

в котором никакая свободная переменная (Шаблон:Lang-en) в <math>R</math> не изменяется (Шаблон:Lang-en) под влиянием команды <math>C</math>. Используя это правило, можно добавлять произвольные предикаты о переменных и частях кучи, которые не изменяются командой <math>C</math>. При этом О’Хирн назвал объём занимаемой кучи, затрагиваемой командой, термином Шаблон:Lang-en («отпечаток»). Назначением правила фрейма является расширение рассуждения с более локального описания команды на более глобальное описание объемлющей команды — команды с бо́льшим отпечаткомШаблон:Sfn.

Установив, что логика разделения является примером логики пучковых импликаций, Ян и Иштиак ввёл разделяющую импликацию (Шаблон:Lang-enШаблон:Sfn, Шаблон:Lang-en). Обозначение <math>P -\!\!\!\ast\, Q</math> говорит о том, если куча была расширена непересекающейся с ней кучей, для которой верно <math>P</math>, то для получившейся в результате кучи будет верно <math>Q</math>Шаблон:Sfn.

Семантика логических связок (разделяющей конъюнкции и разделяющей импликации) подразумевает моноидную структуру кучиШаблон:Sfn.

Параллельная логика разделения (CSL)

Параллельная логика разделения (Шаблон:Lang-en) — версия логики, применимая для верификации параллельных алгоритмов с общей памятью. Изначально предложена Питером О’Хирном. В ней используется следующее правило[10]

<math> \frac{\{P_1\} C_1 \{Q_1\} \quad \{P_2\} C_2 \{Q_2\}}{\{P_1 * P_2\}\; C_1 \parallel C_2 \;\{Q_1 * Q_2\}}</math>,

которое позволяет строить выводы в присутствии независимых потоков выполнения, обращающихся к отдельному хранилищу. Правила доказательства О’Хирна адаптировали ранний подход Тони Хоара к параллелизму[11], заменив использование ограничений области видимости для обеспечения разделения рассуждениями в логике разделения. В дополнение к распространению подхода Хоара на указатели в куче, О’Хирн показал, что логика параллельного разделения может динамически отслеживать передачу владения областями кучи между процессами. Так, примеры в его статье включают буфер передачи указателя и менеджер памяти.

Локальные рассуждения можно понимать и в терминах передачи принадлежности (Шаблон:Lang-en). Легче всего рассмотреть передачу принадлежности на примере правил монитора Хоара (можно увидеть, что логика разделения подходит и для распределённых систем). Для входа процесса в критическую секцию применяется разделяющая конъюнкция с <math>I_r</math>, где <math>I_r</math> — инвариант ресурса r. По выходе из критической секции логический вывод следует в обратном направлении[12]:

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

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

Модель для параллельной логики разделения была впервые представлена Шаблон:Нп2 в сопроводительной статье к статье О’Хирна[13]. Шаблон:Нп2 логики была сложной проблемой. В частности, контрпример Джона Рейнольдса показал несостоятельность более ранней, неопубликованной версии логики. Вопрос, поднятый примером Рейнольдса, кратко описан в статье О’Хирна и более подробно у Брукса.

О’Хирн и Брукс — сообладатели премии Гёделя 2016 года за изобретение логики параллельного разделения[14].

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

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

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

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

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

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

Примечания

Шаблон:Примечания

Литература

Ссылки

Шаблон:Добротная статья

Партнерские ресурсы
Криптовалюты
Магазины
Хостинг
Разное

  1. ↑ 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
  2. ↑ BI as an Assertion Language for Mutable Data Structures. Samin Ishtiaq, Peter O’Hearn. POPL 2001.
  3. ↑ Local Reasoning about Programs that Alter Data Structures. Шаблон:Wayback Peter O’Hearn, John Reynolds, Hongseok Yang. CSL 2001
  4. ↑ Some techniques for proving programs which alter data structures. R.M. Burstall. Machine Intelligence 7, 1972.
  5. ↑ The Logic of Bunched Implications P.W. O’Hearn and D. J. Pym. Bulletin of Symbolic Logic , 5(2), June 1999, pp215-244
  6. ↑ Chris Poskitt Software Verification (Fall 2013) Lecture 5: Separation Logic Parts I - IIШаблон:Недоступная ссылка
  7. ↑ Шаблон:Cite conference
  8. ↑ Matthew J. Parkinson Local reasoning for Java Шаблон:Wayback, 2005, UCAM-CL-TR-654, ISSN 1476—2986
  9. ↑ Lecture 24: Pointer and shape analysis Шаблон:Wayback, LARA, EPFL
  10. ↑ Шаблон:Cite journal
  11. ↑ Шаблон:Cite journal
  12. ↑ 12,0 12,1 Étienne Lozes Information as Resource in Separation LogicШаблон:Недоступная ссылка, ANR project, draft
  13. ↑ Шаблон:Cite journal
  14. ↑ European Association for Theoretical Computer Science 2016 Gödel Prize Шаблон:Wayback
  15. ↑ Шаблон:Cite web
  16. ↑ Шаблон:Cite web
  17. ↑ Шаблон:Статья
  18. ↑ Cliff Jones (from U. Newcastle), Viktor Vafeiadis (from MPI-SWS) Rely-guarantee thinking & separation logic Шаблон:Wayback
Источник — http://wikihandbk.com/ruwiki/index.php?title=Русская_Википедия:Логика_разделения&oldid=10281631