Logique de séparation

Un article de Wikipédia, l'encyclopédie libre.
Aller à : navigation, rechercher

La logique de séparation (du terme 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.

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.