« Logique de séparation » : différence entre les versions
m (Remplacement de texte — « Catégorie:Scotty2 » par « <!-- Scotty2 --> ») |
m (Remplacement de texte — « n.f. » par « nom fém. ») |
||
| Ligne 14 : | Ligne 14 : | ||
==Français== | ==Français== | ||
'''logique de séparation''' | '''logique de séparation''' nom fém. | ||
==Anglais== | ==Anglais== | ||
Version du 16 avril 2020 à 10:48
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 nom fém.
Anglais
Separation logic
Contributeurs: Claude Coulombe, Jacques Barolet, wiki
