© B-Core
(UK) Limited, Last updated: 22 Feb 2002
These tools provide tailored, purpose-built specifications and implementations of objects built as structured data with a rich set of operations to manipulate that data. The data is described in a declarative manner in the `.bse' file, and the operations produced may be filtered through editing (manually, or automatically through an optional SUPPORTS clause) a generated `.ops' file.
An input of, for example, `fifi.bse' would produce an output, to the CFG directory, of four configured Abstract Machine source files fifi.mch, fifiCtx.mch, fifiI.imp and fifiCtxI.imp; it also outputs related analysed and type files to the ANL and TYP directories. The Ctx machines provide contextual information regarding sets, constants and properties, and are not present if the base description comprises a single GLOBAL base.
Abstract Machines produced by the tool are standard specifications which can be imported or included into other machines. The output source file provides the state and operations available on the state. Since these are generated machines, you can assume that they are syntactically correct, well-typed and internally consistent - hence no proof obligations are generated.
The generation of these machines takes place in two stages: first a `.ops' construct is generated (through the `gbo' directive); this comprises a file of operation headers which will dictate which operations will subsequently be produced by the `gbm' directive.
The `.ops' file may be edited to reduce the number of operations produced in line with the user's requirements (it is recommended that operations not required are commented out rather than removed). This `.ops' construct is dependent on the `.bse' construct, and all generated machines are dependent on the `.ops' construct.
The general form of a system description is given in a BNF-like syntax
as follows:
the syntax exp1 | exp2 indicates exp1 or exp2
(choice),
<< exp >> indicates zero or more occurrences of exp
(repetition) and
[| exp |] indicates optionality.
system_description ::= SYSTEM system_name [| SUPPORTS imp_name << , imp_name >> |] [| SETS enum_set_decl << ; enum_set_decl >> |] IS system_body END
system_name ::= Identifier imp_name ::= Identifier
enum_set_decl ::= { Identifier << , Identifier >> }
system_body ::= GLOBAL global_dec_list END << ; base_body >> | base_body << ; base_body >>
base_body ::= BASE base_name base_clause END |
base_name ::= Identifier
base_clause ::= MANDATORY mand_dec_list | OPTIONAL opt_dec_list | MANDATORY mand_dec_list OPTIONAL opt_dec_list
opt_dec_list ::= opt_dec << ; opt_dec >>
mand_dec_list ::= mand_dec << ; mand_dec >>
opt_dec ::= Identifier: STRING[dim] | Identifier: SEQ(Identifier)[dim] | Identifier: SET(Identifier)[dim] | Identifier: Identifier
mand_dec ::= Identifier [| (ID) |]: STRING[dim] | Identifier [| (ID) |]: FSTRING[dim] | Identifier: SEQ(Identifier)[dim] | Identifier: SET(Identifier)[dim] | Identifier: Identifier
global_dec_list ::= global_dec << ; global_dec >>
global_dec ::= Identifier: STRING[dim] | Identifier: FSTRING[dim] | Identifier: SEQ(Identifier)[dim] | Identifier: SET(Identifier)[dim]
dim ::= Bnumberwhere Identifier is a B Identifier.
An example system description is:
SYSTEM
example
SUPPORTS
fifiI, mimiI
SETS
SEX = { female , male }
IS
GLOBAL
gl1 : SEQ(base1)[10];
gl2 : SET(base1)[15];
gl3 : FSTRING[8]
END;
BASE
base1
MANDATORY
base1_mand1 : PERSON;
base1_mand2 : SEX;
base1_mand3 ( ID ) : STRING[15]
END;
BASE
base2
MANDATORY
base2_mand1 : base1;
base2_mand2 : SEQ(base1)[5];
base2_mand3 : SET(base2)[2];
base2_mand4 : STRING[10]
OPTIONAL
base2_opt1 : NAT;
base2_opt2 : SEQ(base2)[10];
base2_opt3 : SET(PERSON)[25];
base2_opt4 : STRING[12]
END
END
This stipulates a module (state machine) consisting of three simple data
structures gl1, gl2 and gl3, and two complex
data structures base1 and base2. Complex data structures
may have mandatory (MANDATORY) and optional (OPTIONAL)
attributes. this example would produce a module parameterised over the
set PERSON and the numbers max_base1 and max_base2,
(the maximum number of objects to be stored in each base).
The optional SUPPORTS clause indicates that the generated system is to support the two implementations fifiI and mimiI, and as a consequence the generated `.ops' file will automatically have those operations not required by the two implementations commented out.
The optional SETS clause prevents the generated machines from being parameterised over the set SEX; instead the (enumerated) set is declared inside the generated Context machine.
Note the optional ID tag for the base1_mand2 field; this sets the identifier field for the base base1 as base1_mand2. So when the operation to print an object from base2 is invoked - print_BaseObj_base2 - all references to base1 objects will include the value of the field base1_mand2. Thus it is sensible to ID-tag fields of type STRING or FSTRING, and only one tag per base is permitted.
In general, system description may contain a GLOBAL clause and/or one or any number of BASE clauses. Each clause contains one or several declarations. The declarations may be of the following forms:
basename <: basename_ABSOBJECTis generated together with operations which changes the value of basename.
The generated machine is parameterised by:
An FSTRING differs from a STRING in the manner in which it is implemented; the former is stored, in compressed form, inside the `fnc_obj' machine itself, (whereas the latter is of variable length and stored in the `str_obj' machine, and its token stored in the `fnc_obj' machine). Further, operations for direct copying and testing for equality are provided for FSTRINGs having the same length.
The Base Generator tools also perform BASE language syntax checking; the MiniRemake option is provided if an error is found.
© B-Core
(UK) Limited, Last updated: 22 Feb 2002