Logique de séparation
Cet article est une ébauche concernant l’informatique.
Vous pouvez partager vos connaissances en l’améliorant (comment ?) selon les recommandations des projets correspondants.
La logique de séparation (en anglais « Separation Logic »), attribuée à John C. Reynolds, est une extension de la logique de Hoare. Par rapport à cette dernière, elle permet de raisonner plus simplement sur les programmes qui manipulent des structures avec champs modifiables, et des pointeurs sur de telles structures.
Description modifier
Exemple modifier
L'exemple le plus classique est la structure de liste chaînée où le champ qui pointe sur le reste de la liste est modifiable en place. L'exemple classique de programme illustrant la logique de séparation sur un telle structure est le retournement en place.
Logique de séparation concurrente modifier
La logique de séparation concurrente est une extension de la logique de séparation pour les programmes concurrents. Les travaux sur cette logique ont permis à Stephen Brookes et Peter W. O'Hearn d'obtenir le prix Gödel en 2016[1].
Notes et références modifier
- « 2016 Gödel Prize », sur EATCS.
