Please enable JavaScript.
Coggle requires JavaScript to display documents.
Code Generation, B0 (Substitutions, Types, Values, Expressions and…
Code Generation
Generated from the implementation
This implementation has to be proved
It must comply with the subset of the B language
B0
Types have to be concrete and substitutions have to be deterministic
Basic Machine
There is no formal guarantee that the source code of a basic machine is correct
It should be tested against its formal specification by using traditional testing means
To avoid errors in basic machines
Write trivial implementation, then generate the skeleton of the implementation with the code generator, then complete the skeleton manually
Only declare concrete data in the basic machine in order to ease code association
Focused on the C language
Is the most important byproduct of a B project
B0
Substitutions
s1; s2
VAR
v1, v2
IN
S
END
var := expr imp
var(ident) := expr_imp
skip
IF
C1
THEN
S1
ELSIF
C2
THEN
S2
ELSE
SN
END
CASE
X
OF EITHER
V1
THEN
S1
OR
V2
THEN
S2
ELSE
SN
END
WHILE
C
DO
S
INVARIANT
I
VARIANT
V
END
var1, var2 <-- op(expr_imp1, expr_imp2)
Types
Variables
Scalar types
Arrays
Cartesian products of arrays
Functions of functions
Implementable B0 Types
Defined or enumerated
SETS
or subsets
INT
or subsets
BOOL
Concrete constants
Subsets of
INT
Subsets of defined sets
Values
Concrete constants and defined sets have to be valued in the clause
VALUES
Expressions and Predicates
Not possible to use f(x), +, -, *, / in a condition
Translation profiles
Profile C9X
Profile LIGHT
Profile 01
Do not mix more than one profile