La logique BILe sigle BI vient de l'anglais 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.
Sa sémantique, de type catégorielle et vérifonctionnelle, 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. 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, et en modélisation de systèmes, où elle permet de décomposer les ressources utilisées par les composants d'un système.
Notes et références
Catégorie:Logique mathématique