Edu/course/homepage/bkp/vt08/atelierb - Department of Information Technology

An introduction to using Atelier B

This introduction shows you how to use Atelier B, the main tool we will be using to analyse our B programs during the course. As always when introduced to a new language we will write a program that outputs the text Hello World! on the terminal. This introduction will only cover the most important functions. You'll find full documentation about the Atelier B user interface using this link (refer to the "Motif" user interface).

Index

Setting up the Atelier B project directories

A development in B is called a "project". The files of each B project are stored in a number of directories. To keep things in order, we suggest that you create one directory where you will store all of your B projects. Within this directory, create a subdirectory for each new project. For this example, create the subdirectory Hello.

All projects need the following three directories:

src -- where you should put the B machine files files of your project.
pdb -- where Atelier B puts its project database.
lang -- where Atelier B will put the generated C code and makefiles for your project.

Create these three directories in the directory Hello. You should now have the the following directories within your B directory: Hello/src, Hello/pdb, Hello/lang.

Running Atelier B

To start Atelier B give the command /it/sw/atelierb/bin/atelierb to a UNIX shell. Two windows will open, one is the Atelier B project window the other the Atelier B message window. The message window might be hidden under the project window when they open -- in that case you must move the project window aside. The project window will show a list of all Atelier B projects that you can access (including projects created by others, if they have named you a co-worker on the project).

The message window may have an error message about missing fonts. You can safely ignore that message for now!

Creating an Atelier B project

To create a new project, click Attach in the project window. Atelier B will open a dialog window where you enter the name of your project, the search path to the project database directory and the search path to the generated code directory.

As Atelier B is designed with multi-user development in mind, project names are shared over the entire computer system and not unique for each user. To avoid name clashes, your course project will be assigned a name by your instructor. Private projects you create (e.g. for practise) should have names beginning with your Unix user id. E.g. a project used by Jesper Bengtson should have a name beginning with jesperb.

Name the example project userid_Hello, point the Project Database Directory to your Hello/pdb-directory and the Translations Directory to your Hello/lang-directory. You don't need to specify the source code directory now -- you do this when you load your B machines into Atelier B.

The next step is to tell Atelier B where it should get any library machines used by the project. Built-in library machines are found in the project LIBRARY. In this example we will need a built-in library machine (for input/output). Select your project in the project window, click Library...->Add and select LIBRARY from the list provided.

If you want to delete a project, select it and click Detach. If you want to let other people work with your project, select the project and for each person, click Users...->Add, and enter the user id of the person. By checking "Read only" or "Read/write" you can choose if this person should have read only access or full access to the project. (NOTE that since B source code files are maintained by you and not by Atelier B, you must yourself set the appropriate protections for the source files if you want someone else to be able to modify them.)

Working with an Atelier B project

Now double click on the jesperb_Hello project to begin working with it.

The following component window will appear:

Before we can do anything more we need to add the source files. In Atelier B, there must be one source file for each component machine. There are several types of source files -- abstract machine files (suffix .mch), which contain the high level mathematical specifications of our programs, implementation files (suffix .imp) which contains the implementation machines which Atelier B can translate to code in C. The goal is to prove that the implementation files do exactly what the specification files dictate. If you do multi-step refinement, there will also be intermediate refinement machine files (suffix .ref).

Using your text editor of choice, create the file Hello.mch in your src-directory. This will be the specification of our Hello World!-program. The specification is, in this case, trivial since no actual computations are being made -- we are just writing text to the screen and as the screen is not part of the machine state, the writing is a side-effect not captured by the specification. Your file should look like this:

MACHINE Hello
OPERATIONS
  entry = skip
END

Note that the file must have the same name as the machine!

The implementation file contains the actual program. Create a file HelloI.imp in the source directory. Note that as the specification and implementation machines have different names, so must the two files (even without their suffixes). The file should look like this:

IMPLEMENTATION HelloI
REFINES Hello
IMPORTS BASIC_IO
OPERATIONS
  entry = STRING_WRITE("Hello World!\n")
END

This creates an implementation called HelloI which is a refinement of Hello. (We will cover in the course exactly what this means.) It also imports the BASIC_IO library machine which allows us to do some rudimentary input/output. The text Hello World! is written to the terminal via the operation STRING_WRITE.

In order to add these two files to your project, press Components...->Add, go to the source code directory and select the components. (You can either add them one at time or simultaneously.)

Modifying an Atelier B project

You can add a new component at any time. If you later on want to remove a component, select it and press Components...->Suppress.

If you need to modify the B source code files, simply edit them in a text editor, then do type checking etc. again. Atelier B will recognise automatically that a file has been changed -- you do not need to add it again! Also, if you ask for a function (e.g. automatic proof) to be carried out on a modified component, Atelier B will automatically perform the needed prerequisite functions (e.g. type checking and proof obligation generation).

WARNING: If you double-click on a component name in the component window, Atelier B will open the source code of that component in an Emacs buffer. This appears convenient, however it will start a new Emacs every time -- even if the file is already open in Emacs -- so it is most likely not what you want! It is better that you keep your favorite text editor around and open files for editing yourself. Similarly, clicking the Atelier B Help buttons will open Netscape with the Atelier B documentation. Again, this appears convenient, but Atelier B will start a new Netscape every time! Starting Netscape takes time and that program doesn't like running multiple copies from the same account. It is better if you open the documentation in a web browser yourself, e.g. using this link.

Checking your Atelier B project

You now need to prove that your project is formally correct. The first thing you need to do is to syntax and type check the components. You can either do this to each individual component or several ones at once. Mark Hello then press Type Check. Hopefully everything will work out. If not, you will get an error message which is not always very descriptive. A detailed result of the syntax and type check can be found in the message window. Then do the same with the HelloI component. (You can select several components at once to check them in one go.)

Next, generate proof obligations for each component. Select in turn Hello and HelloI (or both at once) and press PO generate ...->differential.

Now you actually prove the generated proof obligations of each component -- i.e. prove that your program is correct. Select in turn Hello and HelloI (or both at once) and press Prove ...->Automatic (force 0). This should prove everything automatically, and you should see the following trace in the message window.

The + signs indicate a proof obligation which has been automatically proved. If Atelier B does not succeed in proving a proof obligation, a - sign will be displayed instead.

Most of the time, however, Atelier B will not be able to prove everything automatically and you will have to help it along. How that is done is outside the scope of this introduction.

Generating C code

The first thing you need to do when generating code is to check that your implementation only uses the B0 subset of of the Abstract Machine Notation which can be translated to into a programming language such as C. You do this by selecting the implementation component(s) and pressing B0 Check.

Finally, you generate the code. Select the implementation component and, press the Translator-button. If you have several implementation components, select the one corresponding to the main specification component. The following dialog window will appear:

The languages available with our license are C, C++, and Ada. Leave the settings as they are and press OK. Your code will now be generated and placed a c subdirectory of the project lang directory.

Compiling and running your C program

As long as the target language is C, the generated program code and makefile will be placed in the lang/c/ directory of your project -- in the example the Hello/lang/c directory. Connect to this directory and give the shell command make. The C files will be compiled and an executable file with the same name as your project (userid_Hello will be created. Give the shell command ./userid_Hello to run it and Hello World! should appear on your screen.

Status and reports

At any time you have the components window open, you can check the status of your project. Click Analysing ...->Project Status. You will get a table in the message window:

Here you can see the current state of your project. It tells us for each component and -- at the bottom - the entire project:

if the component has been syntax/type checked (TC)
if proof obligations have been generated (POG)
the number of obvious proof obligations (Obv)
the number of normal proof obligations (nPO)
the number of unproved proof obligations (nUn)
the percentage of proved proof obligations (%Pr)
whether a B0 check has been successfully done (B0C)
whether source code has been generated in the C, Ada, C++ or High Integrity Ada (HIA) languages

If the %Pr figure is 100 then we are happy as all proof obligations will have been formally proved.

You can typeset (with LaTeX) proof obligations or project component machines using proper mathematical symbols. To typeset proof obligations, select a component and click Analysing...->Show/Print PO. In the list, select the part of the component for which you want to see the proof obligations. To the right, you can select what proof obligations will be shown. Click Pretty Print! You can choose to print the typset PO's on a printer or see them in a window using a DVI file viewer. (You must quit the viewer yourself when you are done.) To typeset a component, select it and click Document...->Component. Again, you can choose to print the result or show it in a window.

Provably Correct Software, Spring -08