Biomedical Engineering Reference
In-Depth Information
formal specification. The formal notations and expressions are translated into equiv-
alent programming language code. A detailed translation process of the context and
concrete machine files are given in the following sections.
Process Context and Machine Files Using Lexical and Syntax Analysis
Context and machine files consist of static and dynamic properties of a system in the
form of modular architecture, which represents a system behaviour using formal no-
tations. To generate a source code into any programming language, it is required to
process the context and machine files separately using lexical and syntactic analysis.
Usually, the parsing of a formal model is divided into two stages: lexical analysis
and syntactic analysis. In real-world problem like code generation, lexical analysis
and syntactic analysis stages may be intertwined with each other [
34
]. We are very
thankful to the Rodin development team for providing source code of Rodin tool.
Source code of the Rodin tool is well-written and developed as in the form of a set
of plug-ins to design a complete tool. The Rodin tool has a set of library files of an
Abstract Syntax Tree (AST) which is mainly used for lexical and syntactic analysis
for Event-B notations at the time of modelling. We have used same library for lex-
ical and syntactic analysis of Event-B model for generating a source code into any
programming language (C, C++, Java and C#). To generate a source code into any
target programming language, input source (Event-B formal model) is always same.
Therefore, we have similar kinds of procedures to process context and machine files
using existing AST library of the Rodin tool.
Process Context Files
The context of Event-B model consists of
sets
,
enumerated sets
,
constants
,
arrays
and
constant functions
, associated with their respective type. The translation tool
supports all kinds of context components to generate a constant type with respect
to a programming language. An instance of the context consists in associating to
each name a value consistent with its declared type. The observational equivalence
is based on equivalence between Event-B values and target programming language
values. This equivalence on values is naturally extended on instances of context. The
observational equivalence between Event-B sets and target programming language
types is given in Table
7.5
.
Mapping Event-B Constant Types to Programming Language
•
Enumerated Sets
Event-B enumerated sets is semantically equivalent to a target programming lan-
guage enumerated type. It is very easy to translate into a target programming
language equivalent form due to equivalent semantical structure.
Search WWH ::
Custom Search