Provably Correct Software, Spring -08
Differences between B-Toolkit and Atelier B
The textbook is based on the B notation as implemented by the B-Toolkit, while we will use the tool Atelier B. There are differences, mainly because Atelier B implements a more recent version of the B notation. The differences are minor and mostly about implementations. This page lists differences which are deemed important for the course. Some things which are important but not mentioned in the textbook are also listed here, even if they actually do not differ between the B-Toolkit and Atelier B.
DEFINITIONS
In Atelier B you can define symbols ("macros") which are replaced by their definition when a B machine is parsed. This can be used to introduce shorthand notation without complicating the machine with additional constants. This works exactly like #define symbols in C. Different definitions are separated by semicolons. (Do not insert a semicolon (;) after the final definition! Such a semicolon will be treated as part of the definition -- which is probably not what you wanted.)
Example:
MACHINE Foo DEFINITIONS SMALL == 0..9; increment(x) == (x+1) ...... ...... xx:SMALL ...... ...... increment(yy)
The predicate xx:SMALL is handled exactly as if it was written xx:0..9. The expression increment(yy) is handled exactly as if it was written (yy+1).
Note that parameters in a definition must be a single character -- the only place in a B machine where single character identifiers are allowed!
VARIABLES and CONSTANTS clauses
In Atelier B there the are two kinds of constants and variables, abstract and concrete. The VARIABLES and CONSTANTS clauses declare abstract variables and concrete constants, respectively. These clauses are also called ABSTRACT_VARIABLES and CONCRETE_CONSTANTS. In the Atelier B documentation and messages, you will generally see the long clause names.
Concrete variables are used in implementations (see "State variables in implementations" below).
Abstract constants (declared in an ABSTRACT_CONSTANTS clause) are used if you have constants which are only used in specifications. Abstract constants can not be implemented, but for that reason the can also have types which are not implementable (which are not "concrete data" as defined in "State variables in implementations" below). If you have a constant which is a set, it will generally need to be an abstract constant.
Deferred sets and constants
In the B-Toolkit, implementations assign values to deferred sets and (concrete) constants using the PROPERTIES clause. In Atelier B, the VALUES clause is used instead. The value assigned to a constant must be "concrete scalar data" as defined in "State variables in implementations" below. The value assigned to a set must be one of the sets that "concrete scalar data" can belong to according to "State variables in implementations" below.
Example:
MACHINE Test SETS FOO CONSTANTS bar PROPERTIES card(FOO)>2 & bar:FOO ...
IMPLEMENTATION TestI REFINES Test VALUES FOO=0..20; bar=2 ...
Parameters
Atelier B requires that the parameter list of an abstract machine is repeated in any refinements of that machine, including an implementation. However, the CONSTRAINTS clause should not be repeated.
Atelier B does not allow parameters to be used in the PROPERTIES clause.
State variables in implementations
The B-Toolkit does not allow state variables in implementations. Instead, library machines with state are used. This can sometimes lead to unnecessarily clumsy implementations. In contrast, Atelier B allows a special kind of variables, called "concrete variables". They are declared in a CONCRETE_VARIABLES clause of the implementation machine and differ from ordinary variables only in that they can only hold "concrete data" which can be straightforwardly implemented on a computer.
Concrete data can be either scalars or arrays. A concrete scalar data item belongs to one of the following sets:
- INT (the implementable integers) or a subrange thereof.
- BOOL
- An enumerated set
A concrete scalar array is a total function A-->V, where the arguments and values are all fixed concrete scalar data. The function can have several arguments, in which case A is the cartesian product of sets of concrete scalar data. Note that arrays with dynamic size are not allowed as concrete variables, if you need that you must use a library machine (see below).
Examples:
CONCRETE_VARIABLES a, i;
INVARIANT a:0..10*0..5-->INT & i:NAT
INITIALISATION a:= (1..10)*(1..5)*{0}; i:=0
This declares
- a two-dimensional integer array a, with 10 rows and 5 columns, initialised to all zeroes
- an integer variable i restricted to natural numbers and initialised to 0.
For details, see the the B language reference manual, e.g. sections 3.4, 3.5, 3.6 and 7.18.
Note that it is also possible to have implementation state stored in library machines, just as in the B-Toolkit. See next section.
Library machines
The library machines of Atelier B are completely different from those of the B-Toolkit, so much of chapter 18 in the textbook is not directly applicable (although the ideas put forth in that chapter are certainly applicable also when using Atelier B). Fortunately, concrete variables (see above) eliminates much of the need for library machines.
The library machines of Atelier B are described in the Reusable Components Reference Manual. There are library machines for simple input/output as well as a number of machines which implement some additional mathematical operations, sets, sequences, functions and relations directly. Some of these machines can also do higher-level operations such as sorting and searching.
Note that some library machines use other library machines which you will have to import (IMPORTS clause) directly into your implementation. When you need to do this, it is stated in the description of the library machine.
Multiple copies of included/imported machines
If you need more than one copy of an included/imported machine (e.g. a library machine), you can include/import the machine several times by prefixing each occurence of the machine name with an instance name followed by a dot (e.g. a1.L_ARRAY1). Operations and variables of each machine copy are accessed by prefixing them with the relevant instance name and a dot (e.g. a1.STR_ARRAY1(3,0)).
Example:
IMPORTS a1.L_ARRAY1(0..100,10), a2.L_ARRAY1(NAT,5) INITIALISATION a1.SET_ARRAY(0,10,0); a2.SET_ARRAY(0,5,1) OPERATIONS .... .... ii <-- a1.VAL_ARRAY(kk)
The STRING type
The built-in STRING type in Atelier B is used only to pass arguments to the STRING_WRITE operation of the BASIC_IO library machine. You can not otherwise manipulate built-in strings. String constants are written between double quote marks.
If you want to work with strings as data, you must implement strings yourself, e.g. as sequences of characters. As the CHAR_READ and CHAR_WRITE operations of BASIC_IO represent characters as 8-bit codes, it is a good idea to do the same in your string implementation. Sequences of characters would then have type seq(0..255).