Logique de séparation


Révision datée du 22 mai 2020 à 11:33 par Pitpitt (discussion | contributions) (Remplacement de texte — « <small> loc. nom. fém. </small> » par « <small> féminin </small> »)

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 féminin

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