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

Version du 18 mai 2019 à 22:43

Domaine

Intelligence artificielle
Logique formelle
Raisonnement automatique
Langage de programmation
Programmation logique
Résolution de problèmes

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 n.f.

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

Version du 18 mai 2019 à 22:42 (voir la source) Jacques (discussion \| contributions) Aucun résumé des modifications Balise : Éditeur de wikicode 2017 ← Modification précédente		Version du 18 mai 2019 à 22:43 (voir la source) Jacques (discussion \| contributions) Aucun résumé des modifications Balise : Éditeur de wikicode 2017 Modification suivante →
Ligne 20 :		Ligne 20 :

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

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