Logique BI
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].
Notes et références
[modifier | modifier le code]- ↑ O'Hearn et Pym, « The Logic of Bunched Implications », Bulletin of Symbolic Logic, vol. 5, no 2, , p. 215–244 (DOI 10.2307/421090, JSTOR 421090, S2CID 2948552, CiteSeerx 10.1.1.27.4742, lire en ligne)
- ↑ Le sigle BI vient de l'anglais « Bunched logic »
- ↑ O'Hearn, « On Bunched Typing », Journal of Functional Programming, vol. 13, no 4, , p. 747–796 (DOI 10.1017/S0956796802004495, lire en ligne)
- ↑ Ishtiaq et O'Hearn, « BI as an assertion language for mutable data structures », ACM SIGPLAN Notices, vol. 28th, no 3, , p. 14–26 (DOI 10.1145/373243.375719, CiteSeerx 10.1.1.11.4925, lire en ligne)
- ↑ Pym et Tofts, « A Calculus and logic of resources and processes », Formal Aspects of Computing, vol. 8, no 4, , p. 495–517 (DOI 10.1007/s00165-006-0018-z, S2CID 16623194, lire en ligne)
- ↑ Collinson et Pym, « Algebra and Logic for Resource-based Systems Modelling », Mathematical Structures in Computer Science, vol. 19, no 5, , p. 959–1027 (DOI 10.1017/S0960129509990077, S2CID 14228156, CiteSeerx 10.1.1.153.3899)
- ↑ Matthew Collinson, Brian Monahan et David Pym, A Discipline of Mathematical Systems Modelling, London, College Publications, (ISBN 978-1-904987-50-5)
