« Logique de séparation » : différence entre les versions
m (Remplacement de texte : « ↵<small> » par «  ==Sources== »)
 
(21 versions intermédiaires par 3 utilisateurs non affichées)
Ligne 1 : Ligne 1 :
==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.


== Domaine ==
==Français==
[[Category:Vocabulary]]<br/>
'''logique de séparation''' 
[[Category:Intelligence artificielle]]Intelligence artificielle<br/>
[[Category:Coulombe]]Coulombe<br/>


== Définition ==
==Anglais==
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/>
'''Separation logic'''


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


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


Source:<br/>
==Sources==
[https://fr.wikipedia.org/wiki/Logique_de_s%C3%A9paration Source: wikipedia]


https://fr.wikipedia.org/wiki/Logique_de_s%C3%A9paration<br/>
[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).]


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


== Anglais ==


=== Separation logic ===
[[Category:GRAND LEXIQUE FRANÇAIS]]
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/>
<br/>
<br/>
<br/>

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

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).

Récupérée de « https://datafranca.org/wiki/index.php?title=Logique_de_séparation&oldid=90141 »

Contributeurs: Claude Coulombe, Jacques Barolet, wiki