Виды собственности и логика разделения, похоже, имеют схожие цели, контроль над владением и алиасами. Возможно, стоит также добавить: возможность написания модульных спецификаций.
Что известно об отношениях между типами собственности и разделительной логикой?
Ответы:
Я недавно закончил писать опрос о типах собственности и нашел очень мало, где обсуждаются отношения между этими двумя темами. Три самые близкие статьи, с которыми я столкнулся, - следующие, которые любопытно прибывают из той же самой конференции:
Ян Чжао и Джон Бойленд. Фундаментальное разрешение интерпретации для типов собственности. Во втором Международном симпозиуме IEEE / IFIP по теоретическим аспектам разработки программного обеспечения, TASE 2008, 17-19 июня 2008 г., Нанкин, Китай. IEEE Computer Society, 2008., стр. 65–72.
Шулинг Ван, Луис Соарес Барбоса и Хосе Нуно Оливейра. Реляционная модель для логики ограниченного разделения. Во втором Международном симпозиуме IEEE / IFIP по теоретическим аспектам разработки программного обеспечения, TASE 2008, 17-19 июня 2008 г., Нанкин, Китай. IEEE Computer Society, 2008., с. 263–270.
Шулин Ван и Цунъян Цю. Универсальная модель для заключения и ее применение. Во втором Международном симпозиуме IEEE / IFIP по теоретическим аспектам разработки программного обеспечения, TASE 2008, 17-19 июня 2008 г., Нанкин, Китай. IEEE Computer Society, 2008., стр. 57–64.
В первом документе кодируются два стиля владения, а именно «владельцы как доминанты» и «владельцы как замки», с точки зрения дробных разрешений Бойленда, которые представляют собой систему возможностей, разработанную для рассуждения о программах.
Вторая статья берет идеи ограничения, подобные тем, которые используются в типах собственности, и добавляет их к логике разделения.
В третьей статье разработан семантический подход, который используется для кодирования различных дисциплин, таких как виды собственности. Я не уверен, охватывает ли их система логику разделения, и я не могу получить к ней доступ в данный момент. Их подход является довольно специальным; это можно рассматривать как более формальную и систематическую статью, которую я написал недавно с Джеймсом Ноблом и другими:
источник
Насколько я понимаю, разница заключается в том, что типы владения ограничивают форму графа объектов , а субструктурные системы (например, логика разделения) управляют разрешениями на доступ к куче .
В оригинальной работе над типами собственности идея состоит в том, чтобы поддерживать инвариант владельцев в качестве доминирующих . Объект находится во власти с помощью объекта , если каждый путь от корневого набора к содержит . Так что можно добраться только от . Таким образом, система спроектирована так, чтобы объявления классов параметризировались их владельцами, а затем этот факт дает вам производное условие фрейма для : его состояние не может измениться, если не будет вызван метод для его владельца .о d о d о d о d
Напротив, субструктурные системы, такие как линейные типы и логика разделения, полагаются на идею ресурсов . Каждый регион кучи - это ресурс, и если вы не обладаете этим ресурсом, вы не можете его коснуться. Это делает условия кадра очень легкими: они всегда выполняются.
Одним поверхностным отличием (которое, тем не менее, смущало меня долгое время) было то, что типы собственности были типами, а логика разделения - программной логикой. К счастью, хотя типы собственности были рождены в теоретико-типовой среде, люди применили эти идеи и к программной логике.
Две основные части теоретической работы, которую я знаю по этому вопросу, - это работа Кассиоса над динамическими кадрами , которую систематически использовали Баннерджи и Науманн (и их ученики) в своей работе по региональной логике .
Насколько я понимаю, их основной подход - взять логику Хоара, а затем:
Каждый подход имеет свои преимущества и недостатки.
Собственность делает свойства фрейма значительно менее удобными для использования, чем в субструктурных подходах, так как вам приходится вычислять условия фрейма.
С другой стороны, алгоритмы в группах обеспечения доступности баз данных поддерживают более симпатичные индуктивные доказательства в стиле владения, поскольку вы можете отделить след от структуры указателя. В спецификации в стиле разделения естественным является дать индуктивный инвариант на остовном дереве. Но если связующее дерево, которое вычисляет алгоритм, отличается от того, которое имеет ваш инвариант, вы попадете в мир боли.
Мой общий смысл заключается в том, что разделение проще в использовании, чем владение, поскольку нам нужны свойства фрейма почти для каждой команды в императивной программе. (Дейв Науман утверждает, что региональная логика более поддается автоматизации, поскольку логика утверждений остается простым старым FOL, и поэтому вы можете использовать готовые средства проверки теорем и решатели SMT.)
РЕДАКТИРОВАТЬ: Я только что нашел следующую статью Мэтта Паркинсона и Алекса Саммерса, «Отношения между логикой разделения и неявными динамическими фреймами» , где они утверждают, что дают логику, объединяющую два метода.
источник