Logique de séparation

Définition

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.

Sources:

https://fr.wikipedia.org/wiki/Logique_de_s%C3%A9paration

Serban, C. (2018). Raisonnement automatisé pour la logique de séparation avec des définitions inductives (Doctoral dissertation, Grenoble Alpes).
https://tel.archives-ouvertes.fr/tel-01908769/document

Français

logique de séparation

Source:

https://fr.wikipedia.org/wiki/Logique_de_s%C3%A9paration

Anglais

Separation logic

In computer science, separation logic[1] is an extension of Hoare logic, a way of reasoning about programs. It was developed by John C. Reynolds, Peter O'Hearn, Samin Ishtiaq and Hongseok Yang,[1][2][3][4] drawing upon early work by Rod Burstall.[5] The assertion language of separation logic is a special case of the logic of bunched implications (BI).[6]