Jenis kepemilikan dan Logika Pemisahan

Jenis kepemilikan dan Logika Pemisahan tampaknya memiliki tujuan yang sama, kendali atas kepemilikan dan alias. Mungkin, saya juga harus menambahkan: kemampuan untuk menulis spesifikasi modular.

Apa yang diketahui tentang hubungan antara tipe kepemilikan dan Logika Pemisahan?

Baru-baru ini saya selesai menulis survei Jenis Kepemilikan dan menemukan sangat sedikit yang membahas hubungan antara kedua topik. Tiga makalah terdekat yang saya temui adalah sebagai berikut, yang anehnya datang dari konferensi yang sama:

• Yang Zhao dan John Boyland. Interpretasi izin mendasar untuk tipe kepemilikan. Dalam Simposium Internasional IEEE / IFIP Kedua tentang Aspek Teoretis dari Rekayasa Perangkat Lunak, TASE 2008, 17-19 Juni 2008, Nanjing, Cina. IEEE Computer Society, 2008., halaman 65–72.

• Shuling Wang, Luís Soares Barbosa, dan José Nuno Oliveira. Model relasional untuk logika pemisahan terbatas. Dalam In The Second IEEE / IFIP International Simposium tentang Aspek Teoretis Rekayasa Perangkat Lunak, TASE 2008, 17-19 Juni 2008, Nanjing, Cina. IEEE Computer Society, 2008., halaman 263–270.

• Shuling Wang dan Zongyan Qiu. Model generik untuk kurungan dan penerapannya. Dalam In The Second IEEE / IFIP International Simposium tentang Aspek Teoretis Rekayasa Perangkat Lunak, TASE 2008, 17-19 Juni 2008, Nanjing, Cina. IEEE Computer Society, 2008., halaman 57–64.

Makalah pertama mengkodekan dua gaya jenis kepemilikan, yaitu pemilik-sebagai-dominator dan pemilik-sebagai-kunci, dalam hal izin fraksional Boyland, yang merupakan sistem kemampuan yang dikembangkan untuk alasan tentang program.

Makalah kedua mengambil gagasan pengurungan yang serupa dengan yang digunakan dalam jenis kepemilikan dan menambahkannya ke logika pemisahan.

Makalah ketiga telah mengembangkan pendekatan semantik yang digunakan untuk menyandikan berbagai disiplin ilmu kurungan seperti jenis kepemilikan. Saya tidak yakin apakah sistem mereka mencakup logika pemisahan juga, dan saya tidak dapat mengaksesnya saat ini. Pendekatan mereka agak bersifat sementara; dapat dilihat sebagai lebih formal dan sistematis untuk makalah yang saya tulis beberapa waktu yang lalu dengan James Noble dan yang lainnya:

• Menuju model enkapsulasi James Noble, Robert Biddle, Ewan Tempero, Alex Potanin, Dave Clarke Lokakarya Internasional Pertama tentang Penguraian, Pengurungan dan Kepemilikan dalam Pemrograman Berorientasi Objek (IWACO), 2003.

Cara saya memahami perbedaannya adalah bahwa tipe kepemilikan membatasi bentuk grafik objek , dan sistem substruktural (seperti logika pemisahan) mengelola izin untuk mengakses heap .

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

Sebaliknya, sistem substruktural seperti tipe linear dan logika pemisahan bergantung pada gagasan sumber daya . Setiap wilayah tumpukan adalah sumber daya, dan jika Anda tidak memiliki sumber daya, Anda tidak dapat menyentuhnya. Ini membuat kondisi bingkai sangat mudah: mereka selalu tahan.

Satu perbedaan dangkal (yang bagaimanapun membuat saya bingung untuk waktu yang lama) adalah bahwa tipe kepemilikan adalah tipe, dan logika pemisahan adalah logika program. Untungnya, sementara tipe kepemilikan lahir dalam pengaturan tipe-teoretis, orang-orang telah menerapkan ide-ide ini ke logika program juga.

Dua karya utama teori yang saya tahu tentang ini adalah karya Kassios tentang bingkai dinamis , yang dimanfaatkan oleh Bannerjee dan Naumann (dan siswa mereka) secara sistematis dalam karya mereka pada logika regional .

Seperti yang saya pahami, pendekatan dasar mereka adalah mengambil logika Hoare, dan kemudian:

1. Tambahkan tipe baru variabel wilayah, yang Anda gunakan untuk mengaitkan objek dan wilayah.
2. Tambahkan sistem efek ke logika Hoare untuk melacak daerah membaca dan menulis sentuhan.
3. Gunakan efek untuk menentukan apakah suatu pernyataan menghargai frame atau tidak. Jika ya, Anda bisa membingkainya, dan jika tidak, Anda tidak bisa.

Setiap pendekatan memiliki kelebihan dan kekurangan.

• Kepemilikan membuat properti bingkai jauh lebih mudah digunakan daripada dalam pendekatan substruktural, karena Anda harus menghitung kondisi bingkai.

• Di sisi lain, algoritma pada DAG mendukung bukti induktif yang lebih cantik dalam gaya kepemilikan, karena Anda dapat memisahkan jejak dari struktur pointer. Dalam spec gaya pemisahan, hal yang alami adalah memberikan invarian induktif pada pohon spanning. Tetapi jika spanning tree yang dihitung algoritmanya berbeda dari yang dimiliki invarian Anda, Anda berada dalam dunia yang terluka.

Perasaan umum saya adalah pemisahan lebih mudah digunakan daripada kepemilikan, karena kita membutuhkan properti bingkai untuk hampir setiap perintah dalam program imperatif. (Dave Naumann berpendapat bahwa logika wilayah lebih dapat menerima otomatisasi, karena logika pernyataan tetap menjadi FOL tua yang biasa, dan agar Anda dapat menggunakan pembuktian teorema di luar rak dan pemecah SMT.)

EDIT: Saya baru saja menemukan makalah berikut oleh Matt Parkinson dan Alex Summers, Hubungan antara Logika Pemisahan dan Frame Dinamis Implisit , di mana mereka mengklaim memberikan logika yang menyatukan dua metode.