Logique BI
From Wikipedia, the free encyclopedia
La logique BI[1],[2] est un type de logique sous-structurelle créée par Peter O'Hearn et David Pym. Elle fournit des bases pour le raisonnement sur la composition des ressources , facilitant ainsi l'analyse compositionnelle des systèmes informatiques et autres.
La mise en forme de cet article est à améliorer ().
Sa sémantique, de type catégorielle et vérifonctionnelle[Quoi ?], peut être appréhendée à l'aide du concept de ressource. Sa théorie de la preuve considère les contextes Γ d'une dérivation Γ ⊢ A comme des structures arborescentes (bunches), et non comme des ensembles comme dans la plupart des systemes formels. La logique BI est associée à une théorie des types. Sa première application a consisté à contrôler l'aliasing et d'autres formes d'interférence dans les programmes impératifs[3]. Elle a ensuite trouvé des applications en vérification de programmes, où elle constitue la base du langage d'assertions de la logique de séparation[4], et en modélisation de systèmes, où elle permet de décomposer les ressources utilisées par les composants d'un système[5],[6],[7].
