La mise en forme de cet article est à améliorer ().
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, 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,,.
