Logique BI
From Wikipedia, the free encyclopedia
La mise en forme de cet article est à améliorer ().
La mise en forme du texte ne suit pas les recommandations de Wikipédia : il faut le « wikifier ».
Les points d'amélioration suivants sont les cas les plus fréquents. Le détail des points à revoir est peut-être précisé sur la page de discussion.
- Les titres sont pré-formatés par le logiciel. Ils ne sont ni en capitales, ni en gras.
- Le texte ne doit pas être écrit en capitales (les noms de famille non plus), ni en gras, ni en italique, ni en « petit »…
- Le gras n'est utilisé que pour surligner le titre de l'article dans l'introduction, une seule fois.
- L'italique est rarement utilisé : mots en langue étrangère, titres d'œuvres, noms de bateaux, etc.
- Les citations ne sont pas en italique mais en corps de texte normal. Elles sont entourées par des guillemets français : « et ».
- Les listes à puces sont à éviter, des paragraphes rédigés étant largement préférés. Les tableaux sont à réserver à la présentation de données structurées (résultats, etc.).
- Les appels de note de bas de page (petits chiffres en exposant, introduits par l'outil «
Source - Les liens internes (vers d'autres articles de Wikipédia) sont à choisir avec parcimonie. Créez des liens vers des articles approfondissant le sujet. Les termes génériques sans rapport avec le sujet sont à éviter, ainsi que les répétitions de liens vers un même terme.
- Les liens externes sont à placer uniquement dans une section « Liens externes », à la fin de l'article. Ces liens sont à choisir avec parcimonie suivant les règles définies. Si un lien sert de source à l'article, son insertion dans le texte est à faire par les notes de bas de page.
- La présentation des références doit suivre les conventions bibliographiques. Il est recommandé d'utiliser les modèles {{Ouvrage}}, {{Chapitre}}, {{Article}}, {{Lien web}} et/ou {{Bibliographie}}. Le mode d'édition visuel peut mettre en forme automatiquement les références.
- Insérer une infobox (cadre d'informations à droite) n'est pas obligatoire pour parachever la mise en page.
Pour une aide détaillée, merci de consulter Aide:Wikification.
Si vous pensez que ces points ont été résolus, vous pouvez retirer ce bandeau et améliorer la mise en forme d'un autre article.
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.
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].
