« Logique de séparation » : différence entre les versions


Aucun résumé des modifications
Balise : Éditeur de wikicode 2017
Ligne 2 : Ligne 2 :
== Domaine ==
== Domaine ==
[[Category:Vocabulary]]<br/>
[[Category:Vocabulary]]<br/>
[[Category:Intelligence artificielle]]Intelligence artificielle<br/>
[[Category:Intelligence artificielle]]
[[Category:Coulombe]]Coulombe<br/>
[[Category:Coulombe]]<br/>


== Définition ==
== 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.
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:<br/>


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


== Français ==
== Français ==
logique de séparation
'''logique de séparation'''


Source:<br/>
https://fr.wikipedia.org/wiki/Logique_de_s%C3%A9paration<br/>
Serban, C. (2018). Raisonnement automatisé pour la logique de séparation avec des définitions inductives (Thèse de doctorat, Grenoble Alpes).<br/>
https://tel.archives-ouvertes.fr/tel-01908769/document


== Anglais ==
== Anglais ==


=== Separation logic ===
'''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]


<br/>
<br/>
<br/>
<br/>
[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). ]
<br/>
<br/>
<br/>
<br/>

Version du 17 avril 2019 à 22:31

Domaine



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.


Français

logique de séparation


Anglais

Separation logic



source: wikipedia


source : Serban, C. (2018). Raisonnement automatisé pour la logique de séparation avec des définitions inductives (Thèse de doctorat, Grenoble Alpes).