> <\/strong>the B0 Checker carries out verifications specific to the BO language used in the installations (a sub-division of B language) to ensure that they can be translated.
\nthe project checker checks all the components of a project to control its architecture (the links between the components). The project must have been checked before the final translation of the project.<\/p>\nB models can be saved in pdf, rtf and LaTeX formats.<\/p>\n
> AUTOMATIC TRANSLATORS<\/h5>\n
The installations make up the coding stage for a development in B language. They are written using a B language sub-assembly, similar to an imperative programming language. In order to facilitate code generation on any target system, the installations are translated automatically to standard programming language. The programmes obtained can then be compiled and assembled on the target machine to produce the executable software.<\/p>\n[\/vc_column_text][\/vc_column_inner][vc_column_inner width=”1\/2″][vc_column_text]\n
> THE GRAPHIC REPRESENTATION OF PROJECTS<\/h5>\n
It is used for the graphic representation of the components of a project and their links, by positioning them automatically on the graph. The user can choose different display options, for example the type of links to be viewed, the view of the whole dependence graph of a project or the dependence graph of a component.<\/p>\n
> PROOF TOOLS<\/h5>\n
– the automatic generation of the proof obligations using the components in B language
\n– a B component is correct when its proof obligations are demonstrated
\n– proof in automatic mode: most of the proof obligations are demonstrated without user intervention
\n-the proof in interactive mode used when the automatic mode has failed: the user guides the prover in its proof obligation demonstration using interactive commands (lemma additions, proof by case etc.)
\n– the predicate prover: predicate demonstration: demonstration of rules added by the user
\n– viewing poof obligations, their origin and their status (trivial, proved, non-proved)
\n– the management of a validated rule base including more than 2 200 rules<\/p>\n
> PROJECT MANAGEMENT<\/h5>\n
Atelier B offers large size project management services (including for example 500 components). In particular:
\n– Atelier B used by several users in a network. These users can work on the same project at the same time
\n– to archive and restore a whole project
\n– to architecture a project or several sub-projects or libraries. As such, Atelier B enables large and modular developments by several developer teams
\n– to view the overall status of a project, by supplying for each component, its status (passed to Type Checker, translated to C or to Ada), the number of proof obligations and the percentage proved
\n– to generate automatically the dependencies between the project\u2019s components. As such, to carry out an action (passage through the Type Checker, through the proof obligation generator etc.) on a selection of components, Atelier B reports the action(s) required for the components on which it depends.<\/p>\n[\/vc_column_text][\/vc_column_inner][\/vc_row_inner][\/vc_column][\/vc_row][vc_row full_width=”stretch_row” css=”.vc_custom_1468918934495{padding-top: 55px !important;padding-bottom: 55px !important;}”][vc_column width=”2\/6″ css=”.vc_custom_1468919851744{padding: 50px !important;}”][vc_column_text]\n
IN
\nADDITION<\/h2>\n[\/vc_column_text][vc_column_text css=”.vc_custom_1469552766313{margin-top: 25px !important;}”]\n
DISCOVER B COMPILER<\/p>\n[\/vc_column_text][\/vc_column][vc_column width=”1\/6″][vc_single_image image=”2300″ img_size=”150×150″ alignment=”center”][\/vc_column][vc_column width=”3\/6″][vc_column_text]\n
> <\/strong>B compiler is, with the Theoreme generator and the Theoreme demonstrator, one of the main tools of Atelier B. It allows syntax analysis of B models and to check types coherence and construction rules and B model projects visibility…<\/p>\n[\/vc_column_text][vc_btn title=”SEE MORE +” style=”outline-custom” outline_custom_color=”#eb690b” outline_custom_hover_background=”#ffffff” outline_custom_hover_text=”#ffffff” align=”left” i_align=”right” i_icon_fontawesome=”fa fa-long-arrow-right” add_icon=”true” css=”.vc_custom_1469562812700{margin-top: 15px !important;}” link=”url:http%3A%2F%2Fwww.atelierb.eu%2Fen%2Foutil-atelier-b%2Fle-compilateur-b%2F||”][\/vc_column][\/vc_row][vc_row full_width=”stretch_row_content_no_spaces” css=”.vc_custom_1469092736351{margin-bottom: -60px !important;background-image: url(https:\/\/www.atelierb.eu\/wp-content\/uploads\/sites\/3\/2016\/07\/footer-visu2.jpg?id=2296) !important;background-position: center !important;background-repeat: no-repeat !important;background-size: cover !important;}”][vc_column][vc_empty_space height=”350″][\/vc_column][\/vc_row]\n","protected":false},"excerpt":{"rendered":"[vc_row full_width=”stretch_row” css=”.vc_custom_1469175789322{padding-top: 95px !important;padding-bottom: 70px !important;background-image: url(https:\/\/www.atelierb.eu\/wp-content\/uploads\/sites\/3\/2016\/07\/visu-header-pages.jpg?id=2315) !important;background-position: center !important;background-repeat: no-repeat !important;background-size: cover !important;}”][vc_column][st_customheading heading=”ATELIER B TOOL” heading_color=”#ffffff” content_align=”text-default”][\/vc_column][\/vc_row][vc_row full_width=”stretch_row” css=”.vc_custom_1468915214859{padding-top: 55px !important;padding-bottom: 55px !important;background-color: #fabb00 !important;}”][vc_column width=”2\/6″][st_customheading heading=”PRESENTATION” heading_color=”#ffffff” content_align=”text-default”][\/vc_column][vc_column width=”1\/6″][vc_single_image image=”2297″ img_size=”130×130″ alignment=”center”][\/vc_column][vc_column width=”3\/6″][vc_column_text] Atelier B is a tool enabling the operational use of B method. In a coherent environment, it provides […]<\/p>\n","protected":false},"author":1,"featured_media":0,"parent":0,"menu_order":0,"comment_status":"closed","ping_status":"open","template":"","meta":{"amp_status":""},"yoast_head":"\n
Atelier B | Atelier B<\/title>\n<meta name=\"description\" content=\"Atelier B is a tool enabling the operational use of B method. In a coherent environment, it provides many functions for managing projects in B\" \/>\n<meta name=\"robots\" content=\"index, follow\" \/>\n<meta name=\"googlebot\" content=\"index, follow, max-snippet:-1, max-image-preview:large, max-video-preview:-1\" \/>\n<meta name=\"bingbot\" content=\"index, follow, max-snippet:-1, max-image-preview:large, max-video-preview:-1\" \/>\n<link rel=\"canonical\" href=\"https:\/\/www.atelierb.eu\/atelier-b-tools\/\" \/>\n<meta property=\"og:locale\" content=\"fr_FR\" \/>\n<meta property=\"og:type\" content=\"article\" \/>\n<meta property=\"og:title\" content=\"Atelier B | Atelier B\" \/>\n<meta property=\"og:description\" content=\"Atelier B is a tool enabling the operational use of B method. In a coherent environment, it provides many functions for managing projects in B\" \/>\n<meta property=\"og:url\" content=\"https:\/\/www.atelierb.eu\/en\/atelier-b-tools\/\" \/>\n<meta property=\"og:site_name\" content=\"Atelier B\" \/>\n<meta property=\"article:modified_time\" content=\"2017-03-24T14:20:13+00:00\" \/>\n<meta name=\"twitter:card\" content=\"summary\" \/>\n<script type=\"application\/ld+json\" class=\"yoast-schema-graph\">{\"@context\":\"https:\/\/schema.org\",\"@graph\":[{\"@type\":\"WebSite\",\"@id\":\"https:\/\/www.atelierb.eu\/en\/#website\",\"url\":\"https:\/\/www.atelierb.eu\/en\/\",\"name\":\"Atelier B\",\"description\":\"Atelier de G\\u00e9nie Logiciel\",\"potentialAction\":[{\"@type\":\"SearchAction\",\"target\":\"https:\/\/www.atelierb.eu\/en\/?s={search_term_string}\",\"query-input\":\"required name=search_term_string\"}],\"inLanguage\":\"fr-FR\"},{\"@type\":\"WebPage\",\"@id\":\"https:\/\/www.atelierb.eu\/en\/atelier-b-tools\/#webpage\",\"url\":\"https:\/\/www.atelierb.eu\/en\/atelier-b-tools\/\",\"name\":\"Atelier B | Atelier B\",\"isPartOf\":{\"@id\":\"https:\/\/www.atelierb.eu\/en\/#website\"},\"datePublished\":\"2011-10-31T14:04:43+00:00\",\"dateModified\":\"2017-03-24T14:20:13+00:00\",\"description\":\"Atelier B is a tool enabling the operational use of B method. In a coherent environment, it provides many functions for managing projects in B\",\"breadcrumb\":{\"@id\":\"https:\/\/www.atelierb.eu\/en\/atelier-b-tools\/#breadcrumb\"},\"inLanguage\":\"fr-FR\",\"potentialAction\":[{\"@type\":\"ReadAction\",\"target\":[\"https:\/\/www.atelierb.eu\/en\/atelier-b-tools\/\"]}]},{\"@type\":\"BreadcrumbList\",\"@id\":\"https:\/\/www.atelierb.eu\/en\/atelier-b-tools\/#breadcrumb\",\"itemListElement\":[{\"@type\":\"ListItem\",\"position\":1,\"item\":{\"@type\":\"WebPage\",\"@id\":\"https:\/\/www.atelierb.eu\/\",\"url\":\"https:\/\/www.atelierb.eu\/\",\"name\":\"Accueil\"}},{\"@type\":\"ListItem\",\"position\":2,\"item\":{\"@type\":\"WebPage\",\"@id\":\"https:\/\/www.atelierb.eu\/en\/atelier-b-tools\/\",\"url\":\"https:\/\/www.atelierb.eu\/en\/atelier-b-tools\/\",\"name\":\"Atelier B\"}}]}]}<\/script>\n<!-- \/ Yoast SEO plugin. -->","_links":{"self":[{"href":"https:\/\/www.atelierb.eu\/en\/wp-json\/wp\/v2\/pages\/14\/"}],"collection":[{"href":"https:\/\/www.atelierb.eu\/en\/wp-json\/wp\/v2\/pages\/"}],"about":[{"href":"https:\/\/www.atelierb.eu\/en\/wp-json\/wp\/v2\/types\/page\/"}],"author":[{"embeddable":true,"href":"https:\/\/www.atelierb.eu\/en\/wp-json\/wp\/v2\/users\/1\/"}],"replies":[{"embeddable":true,"href":"https:\/\/www.atelierb.eu\/en\/wp-json\/wp\/v2\/comments\/?post=14"}],"version-history":[{"count":6,"href":"https:\/\/www.atelierb.eu\/en\/wp-json\/wp\/v2\/pages\/14\/revisions\/"}],"predecessor-version":[{"id":3162,"href":"https:\/\/www.atelierb.eu\/en\/wp-json\/wp\/v2\/pages\/14\/revisions\/3162\/"}],"wp:attachment":[{"href":"https:\/\/www.atelierb.eu\/en\/wp-json\/wp\/v2\/media\/?parent=14"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}