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


m (Remplacement de texte — « <small> féminin </small> » par «  »)
m (Remplacement de texte : « ↵<small> » par «  ==Sources== »)
 
(Une version intermédiaire par le même utilisateur non affichée)
Ligne 10 : Ligne 10 :




<small>
 
==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]


Ligne 16 : Ligne 17 :




[[Category:Intelligence artificielle]]
 
[[Catégorie:Logique formelle]]
[[Catégorie:Raisonnement automatique]]
[[Category:Langage de programmation]]
[[Category:Programmation logique]]
[[Category:Résolution de problèmes]]
[[Category:GRAND LEXIQUE FRANÇAIS]]
[[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

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