« Logique de séparation » : différence entre les versions
m (Remplacement de texte — « <!-- Coulombe2 --> » par « ») |
m (Remplacement de texte : « ↵<small> » par « ==Sources== ») |
||
| (5 versions intermédiaires par le même utilisateur non affichées) | |||
| Ligne 1 : | Ligne 1 : | ||
==Définition== | ==Définition== | ||
La logique de séparation ( ''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. | La logique de séparation ( ''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. | ||
==Français== | ==Français== | ||
'''logique de séparation''' | '''logique de séparation''' | ||
==Anglais== | ==Anglais== | ||
| Ligne 22 : | Ligne 11 : | ||
==Sources== | |||
[https://fr.wikipedia.org/wiki/Logique_de_s%C3%A9paration Source: wikipedia] | [https://fr.wikipedia.org/wiki/Logique_de_s%C3%A9paration Source: wikipedia] | ||
[https://tel.archives-ouvertes.fr/tel-01908769/document Source : Serban, C. (2018). Raisonnement automatisé pour la logique de séparation avec des définitions inductives (Thèse de doctorat, Grenoble Alpes).] | [https://tel.archives-ouvertes.fr/tel-01908769/document Source : Serban, C. (2018). Raisonnement automatisé pour la logique de séparation avec des définitions inductives (Thèse de doctorat, Grenoble Alpes).] | ||
[[Category:GRAND LEXIQUE FRANÇAIS]] | |||
Dernière version du 28 janvier 2024 à 09:55
Définition
La logique de séparation ( 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.
Français
logique de séparation
Anglais
Separation logic
Sources
Contributeurs: Claude Coulombe, Jacques Barolet, wiki
