From ClearSy Tools

Contents 1 Introduction 2 Structure of the B0-ComenC components 2.1 Couple abstract machine - implementation 2.2 Clause CONSTRAINTS 2.3 Clause DEFINITIONS 2.4 Clause IMPORTS 2.5 Clause SEES 2.6 Clause SETS 2.7 Clause CONCRETE_CONSTANTS 2.8 Clause PROMOTES 2.9 Clause EXTENDS 2.10 Clause VALUES 2.11 Clause CONCRETE_VARIABLES 2.12 Clause INVARIANT 2.13 Clause INITIALISATION 2.14 Clause ASSERTIONS 2.15 Clauses OPERATIONS and LOCAL_OPERATIONS 2.16 Multi-components files 3 Structure of the B0-ComenC instructions 3.1 SKIP 3.2 BLOCK 3.3 VAR 3.4 IF 3.5 WHILE 3.6 ASSERT 3.7 CASE 3.8 Operation call 3.9 Sequencing 3.10 Valuation substitution 3.11 Valuation 3.12 Initialisation 3.13 Predicates 3.14 Expressions 3.15 Conditions 3.16 Identifiers 3.17 Literals 3.18 B language predefined constants 3.19 Reading an element of a table 4 Annex: Error messages

Introduction

B0-ComenC is the implementation language for the ComenC code-generation factory. This language is defined below, in delta regarding the B0 language.

B0-ComenC restrictions to B0 language are verified by the ComenC internal checker. In case of non compliance, error messages are displayed. These messages are listed in annex.

Structure of the B0-ComenC components

Couple abstract machine - implementation

Machines can't have scalar or set-based formal parameters. As multiple imports are forbidden, formal parameters are useless and as such ignored.

Exemple :

MACHINE Speed_Control
...
END

IMPLEMENTATION Speed_Control_1
REFINES Speed_Control
...
END

B0-ComenC internal checker verifies that implementations have no formal parameter. Machines are thus indirectly checked for not having formal parmaeters. The error message n°1 is generated if an implementation has one or more formal parameters.

Clause CONSTRAINTS

Clause CONSTRAINTS is forbidden as MACHINES have no formal parameters / sets.

Clause DEFINITIONS

Definition files are expanded during a preprocessing phase, perfomed by bpp tool.

Clause IMPORTS

Imported machines should not be renamed.

Example :

...
IMPORTS
    BASIC_CONSTANTS,
    Speed_Control
...

If a machine is imported several times, then the error message n°2 is generated.

Clause SEES

Seen machines should not be renamed. The error message n°2 is generated if this rule is not fulfilled.

Clause SETS

The clause SETS of a B specification allows to declare abstract sets and enumerated sets. Enumerated sets should have at most 660 elements.

If this rule is not fulfilled, the error message n°4 is generated.

Clause CONCRETE_CONSTANTS

Constants declared in the clause CONCRET_CONSTANTS are either:

• scalar data
• 1-D or 2D tables
• integer intervals

Indexes of tables should be intervals having 0 as as lower bound, and a literal integer as upper bound. Integer intervals improve lisibility of B code, as they allow to manipulate sets with significant names (for example SPEED) instead of default integer sets (for example: INT, NAT and NAT1).

Example :

CONSTANTS
    SPEED,
    Position,
    Stop
PROPERTIES
    SPEED<: INT &
    Position : INT &
    Stop: BOOL

If this rule is not fulfilled, then the error message n°5 is generated.

Clause PROMOTES

Nothing specific to B0Comenc.

Refer to B0 language reference manual for the complete clause description.

Clause EXTENDS

Machines extended by a B0Comenec implementation can't be renamed (as for imported and seen machines). If this rule is not fulfilled, the the error message n°2 is generated.

Clause VALUES

An abstract set can't be valued by a predefined set (INT, NAT or NAT1). If this rule is not fullfilled, then the error message n°16 is generated.

Clause CONCRETE_VARIABLES

Scalar variables and 1D or 2D tables are declared within the clause CONCRETE_VARIABLES.

Indexes of tables should be intervals where lower bound is 0 and upper bound is a literal integer.

Example :

VARIABLES
    Speed,
    Position
INVARIANT
    Speed: SPEED&
    Position : INT

If this rule is not fulfilled, then the error message n°7 is generated.

Clause INVARIANT

Nothing specific to B0Comenc.

Refer to B0 language reference manual for the complete clause description.

Clause INITIALISATION

Variables are initialised through valuation substitution (ex: xx := yy), or seen or imported machine procedure calls. VAR, IF, WHILE and CASE substitutions are prohibited.

Example :

CONCRETE_VARIABLE
    VarTab1, varTab2
INVARIANT
    VarTab1 : (0..2)*(0..5) --> BOOL &
    VarTab2 : (0..1) --> INT
INITIALISATION
    varTab1 := (0..2)*(0..5)*{FALSE} ;
    varTab2 := { 0 |> 0, 1 |> 1 }

If this rule is not fulfilled, the the error message n°8 is generated.

Warning ! Initialising a table with a set of maplets is restricted to parenthesis-free declaration.
Incorrect :

    { (0 |> 0), (1 |> 1) }

Correct :

    { 0 |> 0, 1 |> 1 }

Clause ASSERTIONS

Nothing specific to B0Comenc.

Refer to B0 language reference manual for the complete clause description.

Clauses OPERATIONS and LOCAL_OPERATIONS

Operation output parameters can't be tables. Operation input parameters (global or local) can be tables, but are restricted to:

• 1D or 2D tables,
• tables of 1D tables.

Indexes of tables have to be intervals, where lower bound is 0 and upper bound is a literal integer.

Local operations should be declared before being used. For example, if a local operation op_loc1 calls another local operation op_loc2 (in the clause OPERATIONS), then op_loc2 should be defined before op_loc1 within the clause LOCAL_OPERATIONS.

If this rule is not fulfilled, then the error message n°20 is generated.

Multi-components files

Multi-components files (*.mod) are forbidden is B0ComenC.

If this rule is not fulfilled, then the error message n°19 is generated.

Structure of the B0-ComenC instructions

SKIP

Nothing specific to B0Comenc.

Refer to B0 language reference manual for the complete clause description.

BLOCK

Nothing specific to B0Comenc.

Refer to B0 language reference manual for the complete substitution description.

VAR

The VAR IN substitution should not introduce tables or strings as local variables.

If this rule is not fulfilled, then the error message n°13 is generated.

IF

Nothing specific to B0Comenc.

Refer to B0 language reference manual for the complete substitution description.

WHILE

Nothing specific to B0Comenc.

Refer to B0 language reference manual for the complete substitution description.

ASSERT

Nothing specific to B0Comenc.

Refer to B0 language reference manual for the complete substitution description.

CASE

Nothing specific to B0Comenc.

Refer to B0 language reference manual for the complete substitution description.

Operation call

Output parameters of an operation call should be distinct from input parameters.

For example:

 aa, bb <-- op(aa)

is forbidden.

If this rule is not fulfilled, then the error message n°10 is generated.

Sequencing

Nothing specific to B0Comenc.

Refer to B0 language reference manual for the complete description.

Valuation substitution

Valuating a table with an other table is only permitted in the clause INITIALISATION.

Affecting a table to an element of a table of table is prohibited.

For example, if :

    Tab : E1 --> (E2 --> E3) &
    ind : E1

The following is forbidden

    Tab(ind) := Tab2

If this rule is not fulfilled, then the error message n°14 is generated.

Valuation

Nothing specific to B0Comenc.

Refer to B0 language reference manual for the complete description.

Initialisation

Authorized initialisation instructions are operation calls and valuation substitutions. Within valuation substitutions, right hand-side expressions should be static.

Predicates

Nothing specific to B0Comenc.

Refer to B0 language reference manual for the complete description.

Expressions

Operators **, succ and pred are not allowed.

If this rule is not fulfilled, then error message n°9 or n°11 is generated.

Conditions

Conditions based on equality or non-equality of tables are forbidden.

If this rule is not fulfilled, then the error message n°15 is generated.

Identifiers

Nothing specific to B0Comenc.

Refer to B0 language reference manual for the complete description.

Literals

Nothing specific to B0Comenc.

Refer to B0 language reference manual for the complete description.

B language predefined constants

MAXINT and MAXINT predefined constants are forbidden in B0ComenC.

Reading an element of a table

A read access to an element of a table is allowed.

A read access to an element of a table of table (designating a table) is not permitted.

For example, if:

    Tab : E1 --> (E2 --> E3) &
    ind : E1

then the following is forbidden

    Val := Tab(ind)

If this rule is not fulfilled, then the error message n°16 is generated.

Annex: Error messages

Message #	String
1	unsupported formal parameters of abstract machines
2	unsupported renaming of abstract machine « %s »
3	Invalid array type « %s »
4	Enumerate Set « %s » too large
5	Invalid array type « %s »
6
7	Invalid interval minimal bound (literal integer 0 expected)
8	unsupported instruction in INITIALISATION clause
9	« %s » is not allowed
10	« %s » is used both as input and output parameter of called operation « %s »
11	« %s » is not allowed
12	Invalid initialisation of « %s » in « %s »
13	Invalid declaration of Array type « %s »
14	Invalid assignment of « %s » in « %s »
15	Invalid comparison of « %s » and « %s » (Array Type)
16	Explicit valuation of array « %s » is not allowed
17	Invalid range for array type (interval expected) : « %s »
18
19	Multicomponent file is not allowed
20	Local operation « %s » must be declare before « %s »
21	« %s » has not been initialised
22	LHS and RHS arrays are incompatible
23	« %s » is an array : it can not be on the right handside of an affectation