About Us Products Articles News Contact Support

Code generation

After the model is specified, all checks completed and analyses done to confirm that interesting properties meet the engineer’s expectations, the model can be translated into the actual source code in one of the three supported target programming languages: Ada, C or C++.

Code generation is a process that relies on grammar only and in fact does not involve any intermediate verification activity - this means that it is possible to force the generation of code for the model that is incorrect with regard to some checks, but such a practice is not recommended, unless careful analysis of reported errors is performed to justify their acceptance.

Source code can be generated with the following invocation:

where “Ada”, “C” or “C++“ in the second argument names the target language.

The choice of target language has impact not only on the actual generated text, but also on names of created files. The following table summarizes the file naming rules:

Every involved package is implemented in its own set of files and the root part of the file name is derived from the package name. For example, package “MyPackage`” is specified in file my_package.ads if Ada is chosen as a target language.

By default the whole model is taken for processing, but it is possible to constrain the set of packages that are selected for code generation:

Files are stored in the current working directory, which is not necessarily the same in which Mathematica notebooks are stored. The target directory can be specified just for the single invocation:

It is also possible to set the current working directory as a session property, with the standard SetDirectory function, which will take effect for multiple file operations.

Code can be also generated as a plain text value, without involving file storage - this is the raw-format equivalent of other functions within the toolkit:

The following example implements a trivial package with an empty operation:

The source code for this model (without storing it in any file) can be generated with:

The code is an Association object with two entries:

Thus the package specification can be seen as:

package My_Package is
   
   -- Operation declarations.
   
   procedure Do_Nothing;
   
end My_Package;

and analogously, the package implementation:

package body My_Package is
   
   -- Operation definitions.
   
   procedure Do_Nothing is
   begin
      null;
   end Do_Nothing;
   
end My_Package;

A quick-and-dirty way to peek at the generate code, useful for simple checks within the interactive sessions, might be:

These file contents can be further manipulated as regular text objects, whereas the saveCode function automatically exports them to appropriately named files.

The code generation process is configurable by means of translation options for the following parameters:

• Indent size - the number of spaces inserted at the beginning of indented lines.
• Max line length - a soft limit that guides the process of line breaking.
• File naming policy - rules for transforming package names into file names.
• Symbol name translations - rules for generating names for all model entities. By default these rules follow the Standard_Naming for Ada and camelCaseConvention for C and C++.
• Integer target type - the option that is relevant for C and C++ only, defines the target type that is used to represent the model-level integer type. By default it is “int32_t” for C and “std::int32_t” for C++.
• Array copy operation - the generated invocation for array copy, also relevant only for C and C++, and by default implemented in terms of standard “memmove” function.
• File header comment - to allow customization of complete file headers.

A separate chapter on customization provides usage examples for all configurable parameters.

The Formal Methods Toolkit is accompanied by a set of examples - one of them, in the notebook file ExampleCodeGen.nb, is a full interactive unit test involving all possible modeling constructs with code generations for all supported target programming languages. This example notebook can be used as a supplementary material to this documentation.

Previous: All checks, next: Customization

See also Table of Contents.