Rodzaje własności i logika separacji

Rodzaje własności i logika separacji wydają się mieć podobne cele, kontrolę nad własnością i aliasing. Być może powinienem również dodać: możliwość pisania specyfikacji modułowych.

Co wiadomo na temat związku między typami własności a logiką separacji?

Niedawno skończyłem pisać ankietę na temat typów własności i znalazłem bardzo niewiele, które omawiają związek między tymi dwoma tematami. Trzy najbliższe artykuły, na które natknąłem się, są następujące, które z ciekawością pochodzą z tej samej konferencji:

• Yang Zhao i John Boyland. Podstawowa interpretacja uprawnień dla typów własności. W drugim międzynarodowym sympozjum IEEE / IFIP na temat teoretycznych aspektów inżynierii oprogramowania, TASE 2008, 17–19 czerwca 2008 r., Nanjing, Chiny. IEEE Computer Society, 2008., strony 65–72.

• Shuling Wang, Luís Soares Barbosa i José Nuno Oliveira. Relacyjny model ograniczonej logiki separacji. W drugim Międzynarodowym Sympozjum IEEE / IFIP na temat teoretycznych aspektów inżynierii oprogramowania, TASE 2008, 17–19 czerwca 2008 r., Nanjing, Chiny. IEEE Computer Society, 2008., strony 263–270.

• Shuling Wang i Zongyan Qiu. Ogólny model zamknięcia i jego zastosowanie. W drugim Międzynarodowym Sympozjum IEEE / IFIP na temat teoretycznych aspektów inżynierii oprogramowania, TASE 2008, 17–19 czerwca 2008 r., Nanjing, Chiny. IEEE Computer Society, 2008., strony 57–64.

Pierwszy artykuł koduje dwa style typów własności, mianowicie właścicieli jako dominujących i właścicieli jako blokad, w kategoriach ułamkowych uprawnień Boylanda, które są systemem zdolności opracowanym do wnioskowania o programach.

Drugi artykuł zawiera pomysły dotyczące zamknięcia podobne do tych stosowanych w typach własności i dodaje je do logiki separacji.

W trzeciej pracy opracowano podejście semantyczne, które stosuje się do kodowania różnych dyscyplin ograniczających, takich jak typy własności. Nie jestem pewien, czy ich system obejmuje również logikę separacji, i nie mogę w tej chwili uzyskać do niej dostępu. Ich podejście jest raczej ad hoc; można to uznać za bardziej formalne i systematyczne w stosunku do artykułu, który napisałem jakiś czas temu z Jamesem Noble'em i innymi:

• W stronę modelu enkapsulacji James Noble, Robert Biddle, Ewan Tempero, Alex Potanin, Dave Clarke Pierwsze międzynarodowe warsztaty nt. Aliasowania, ograniczania i własności w programowaniu obiektowym (IWACO), 2003.

Rozumiem różnicę: typy własności ograniczają kształt wykresu obiektowego , a systemy podstrukturalne (takie jak logika separacji) zarządzają uprawnieniami dostępu do stosu .

$o$$d$$o$$d$$o$$d$$o$$d$

Z kolei systemy podstrukturalne, takie jak typy liniowe i logika separacji, polegają na idei zasobów . Każdy region sterty jest zasobem, a jeśli go nie posiadasz, nie możesz go dotknąć. Dzięki temu warunki kadru są bardzo łatwe: zawsze się trzymają.

Jedną powierzchowną różnicą (która jednak długo mnie myliła) było to, że typy własności były typami, a logika separacji była logiką programu. Na szczęście, podczas gdy typy własności rodziły się w środowisku teoretycznym, ludzie zastosowali te pomysły również w logice programowej.

Dwa główne prace teoretyczne, które znam na ten temat, to praca Kassiosa na temat dynamicznych ram , które Bannerjee i Naumann (i ich uczniowie) systematycznie wykorzystują w swojej pracy nad logiką regionalną .

Jak rozumiem, ich podstawowym podejściem jest przyjęcie logiki Hoare'a, a następnie:

1. Dodaj nowy typ zmiennych regionu, których używasz do kojarzenia obiektów i regionów.
2. Dodaj układ efektów do logiki Hoare, aby śledzić regiony odczytuje i zapisuje dotyk.
3. Użyj efektów, aby ustalić, czy asercja jest zgodna z ramką, czy nie. Jeśli tak, możesz to wrobić, a jeśli nie, nie możesz.

Każde podejście ma zalety i wady.

• Własność sprawia, że ​​właściwości ramki są znacznie mniej wygodne w użyciu niż w podejściach podkonstrukcyjnych, ponieważ trzeba obliczyć warunki ramki.

• Z drugiej strony algorytmy w DAG obsługują ładniejsze dowody indukcyjne w stylu własności, ponieważ można oddzielić ślad od struktury wskaźnika. W specie w stylu separacji naturalną rzeczą jest nadanie indukcyjnego niezmiennika na drzewie rozpinającym. Ale jeśli drzewo rozpinające, które oblicza algorytm, jest zawsze inne niż drzewo niezmiennika, czeka cię świat bólu.

W moim ogólnym odczuciu separacja jest łatwiejsza w użyciu niż własność, ponieważ potrzebujemy właściwości ramki dla prawie każdego polecenia w programie imperatywnym. (Dave Naumann argumentuje, że logika regionu jest bardziej podatna na automatyzację, ponieważ logika asercji pozostaje zwykłym starym FOL, a więc można używać gotowych dowodów twierdzeń i solverów SMT).

EDYCJA: Właśnie znalazłem następujący artykuł Matta Parkinsona i Alexa Summersa, The Relation between Separation Logic and Implicit Dynamic Frames , w którym twierdzą, że podają logikę łączącą obie metody.