From ClearSy Tools

Contents 1 Introduction 2 Hands On 3 Tutorial & examples 4 Online reference manuals 5 Sourceforge site 6 TODO List 7 References

Introduction

ComenC is a translator, transforming a B model ^[1] into a C program.
ComenC gathers experience gained during R&D projects ^[2] as well as application to industry-strength case-studies.

ComenC requires B models:

• typechecked
• 100% proved
• B0-checked: types used in the implementable model comply with the ones supported by ComenC

For those not familiar with B, here is a short introduction to B.

For those willing to go deeper into B, here are more extensive tutorials on B:

• Software development in B (under construction)
• System modeling in event B (under construction)

Hands On

• How to install ComenC
• How to use ComenC
• Minimum example
• Atelier B archive containing the BASIC_IO machine for comenc

Tutorial & examples

• Tutorial ComenC : an introduction to software development with ComenC (under construction)

• Some examples : some examples to experiment with ComenC (under construction)

Online reference manuals

These two documents are the online, english version of the two files included in the doc directory of the ComenC archive file. The second document is still under construction.

• B0-ComenC reference manual

• C-ComenC reference manual (on going translation from French to English)

Sourceforge site

ComenC is going open-source (GPL v3.0) and is hosted on sourceforge [3]. Source code files will be transfered to the forge during summer 2008.

TODO List

This section lists all annoying bugs reported and planned improvements.

• Constant translation: constants are translated as const <type> <name> that might lead to multiple declarations and compilation errors. Translating constants are pure definitions (MACROS) will solve this issue.

• No license file is provided with the ComenC archive.

References

1. ↑ The B language Reference Manual [1]
2. ↑ B Optimized Memory [2]