Types de propriété et logique de séparation

Les types de propriété et la logique de séparation semblent avoir des objectifs, un contrôle sur la propriété et un alias similaires. Je devrais peut-être aussi ajouter: la possibilité d'écrire des spécifications modulaires.

Que sait-on de la relation entre les types de propriété et la logique de séparation?

J'ai récemment terminé d'écrire une enquête sur les types de propriété et j'ai trouvé très peu de choses qui discutent de la relation entre les deux sujets. Les trois articles les plus proches que j'ai rencontrés sont les suivants, qui proviennent curieusement de la même conférence:

• Yang Zhao et John Boyland. Une interprétation d'autorisation fondamentale pour les types de propriété. In Second IEEE / IFIP International Symposium on Theoretical Aspects of Software Engineering, TASE 2008, 17-19 juin 2008, Nanjing, Chine. IEEE Computer Society, 2008., pages 65–72.

• Shuling Wang, Luís Soares Barbosa et José Nuno Oliveira. Un modèle relationnel pour la logique de séparation confinée. In In Second IEEE / IFIP International Symposium on Theoretical Aspects of Software Engineering, TASE 2008, 17-19 juin 2008, Nanjing, Chine. IEEE Computer Society, 2008., pages 263–270.

• Shuling Wang et Zongyan Qiu. Un modèle générique de confinement et son application. In In Second IEEE / IFIP International Symposium on Theoretical Aspects of Software Engineering, TASE 2008, 17-19 juin 2008, Nanjing, Chine. IEEE Computer Society, 2008., pages 57–64.

Le premier article code deux types de types de propriété, à savoir les propriétaires en tant que dominateurs et les propriétaires en tant que verrous, en termes d'autorisations fractionnaires de Boyland, qui sont un système de capacités développé pour raisonner sur les programmes.

Le deuxième article prend des idées de confinement similaires à celles utilisées dans les types de propriété et les ajoute à la logique de séparation.

Le troisième article a développé une approche sémantique qui est utilisée pour coder diverses disciplines de confinement telles que les types de propriété. Je ne sais pas si leur système couvre également la logique de séparation, et je ne peux pas y accéder pour le moment. Leur approche est plutôt ad hoc; cela peut être vu comme plus formel et systématique à un article que j'ai écrit il y a quelque temps avec James Noble et d'autres:

• Vers un modèle d'encapsulation James Noble, Robert Biddle, Ewan Tempero, Alex Potanin, Dave Clarke The First International Workshop on Aliasing, Confinement and Ownership in Object-Oriented Programming (IWACO), 2003.

La façon dont je comprends la différence est que les types de propriété contraignent la forme du graphique d'objet et que les systèmes sous-structurels (comme la logique de séparation) gèrent les autorisations d'accès au tas .

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

En revanche, les systèmes sous-structurels comme les types linéaires et la logique de séparation reposent sur l'idée de ressources . Chaque région du tas est une ressource, et si vous ne possédez pas la ressource, vous ne pouvez pas la toucher. Cela rend les conditions de cadre très faciles: elles tiennent toujours.

Une différence superficielle (qui m'a néanmoins longtemps dérouté) était que les types de propriété étaient des types et que la logique de séparation était une logique de programme. Heureusement, alors que les types de propriété sont nés dans un cadre de théorie des types, les gens ont également appliqué ces idées aux logiques de programmation.

Les deux principaux travaux théoriques que je connais à ce sujet sont les travaux de Kassios sur les cadres dynamiques , que Bannerjee et Naumann (et leurs étudiants) ont systématiquement exploités dans leur travail sur la logique régionale .

Si je comprends bien, leur approche de base est de prendre la logique Hoare, puis:

1. Ajoutez un nouveau type de variables de région, que vous utilisez pour associer des objets et des régions.
2. Ajoutez un système d'effets à la logique Hoare pour suivre les régions en lecture et en écriture tactile.
3. Utilisez les effets pour déterminer si une assertion respecte ou non le cadre. Si c'est le cas, vous pouvez l'encadrer, et si ce n'est pas le cas, vous ne pouvez pas.

Chaque approche présente des avantages et des inconvénients.

• La propriété rend les propriétés du cadre beaucoup moins pratiques à utiliser que dans les approches sous-structurelles, car vous devez calculer les conditions du cadre.

• D'un autre côté, les algorithmes des DAG prennent en charge de plus belles preuves inductives dans un style de propriété, car vous pouvez dissocier l'empreinte de la structure du pointeur. Dans une spécification de style séparation, la chose naturelle est de donner un invariant inductif sur un arbre couvrant. Mais si l'arbre couvrant que l'algorithme calcule est toujours différent de celui de votre invariant, vous êtes dans un monde de souffrance.

Mon sentiment général est que la séparation est plus facile à utiliser que la propriété, car nous avons besoin des propriétés de trame pour presque toutes les commandes d'un programme impératif. (Dave Naumann fait valoir que la logique de région est plus adaptée à l'automatisation, car la logique d'assertion reste un ancien FOL, et vous pouvez donc utiliser des prouveurs de théorèmes et des solveurs SMT standard.)

EDIT: Je viens de trouver l'article suivant de Matt Parkinson et Alex Summers, The Relationship between Separation Logic and Implicit Dynamic Frames , où ils prétendent donner une logique unifiant les deux méthodes.