|
|
||
|
The screenshots below demonstrate complete sessions of working with FMT in the Mathematica environment. Images are linked to their full-resolution versions.
Go back to the project homepage.
Swap
The following example is a model of the basic swap operation that exchanges values of its two parameters. The window on the left is a Mathematica notebook where 1. the FMT package is loaded, 2. new model is created, 3. package "Tools" is declared in the model, 4. the swap operation is declared with post-condition promising the exchange of values, and 5. the body of swap is defined. This workflow is conceptually similar to how it would be done in a regular programming language, but the actual source code, in Ada, is 6. generated at the end. The center window shows the proof statements that were 7. generated and 8. checked. The two windows on the right are text editors showing the generated code for both the package specification and body.
Average with bug
Below, on the left, the average operation is defined with a bug. It was supposed to compute the mean of two non-negative integers, but the engineer naively copied the formula from post-condition and reused it in the operation body. The problem is - the sum of x and y can overflow the integer type before it is divided by two. The right window shows the proof check results, where one of the checks failed. The gray box shows counter-examples, which are possible values that expose the bug (this assuming 32-integers, which is a default configuration).
Average fixed
The same average example, but fixed - the engineer used a different formula that does not cause overflows and is still correct with regard to post-conditions. The center window shows that all generated proofs are correct. Two windows on the right show the C++ header and implementation for this operation.
Visualization and analysis
Below there are several operations defined that call each other. The center window shows a sample of visualization and reporting: the internal grammar representation for the main operation and the call matrix with detected recursive call graphs. Two windows on the right show generated code in C.
Metaprogramming
Metaprogramming refers to "programs that write programs" and in FMT allows to automate the model design. The left window is a complete session defining a package with 50 variables, the right window shows generated Ada code for this package. In a real-life project the model architecture could be automatically generated from higher-level requirements, descriptions stored in external configuration files, databases or models defined in other notations.
Metaprogramming relies on programming features of the Mathematica environment and requires additional knowledge of the Wolfram language.
Code synthesis
Code synthesis is similar to metaprogramming in that it can automate some modeling activities, but is related to operation definitions instead of model design. The left window defines the halfTrue operation that returns True if 4 of its 8 inputs are True. The synthesis relies on the standard BooleanCountingFunction that returns the required expression. The other window shows the generated code in C++. Certainly, it would be difficult to write it by hand and get it right!
Seamless integration with Mathematica
This is another code synthesis example, but mixed with regular Mathematica features. On the left a list of 8-bit sine-wave samples is computed and validated with a plot. Then the synthesis capability of FMT is used to generate the loop with calls to writeDac operation with values from the prepared list. On the right the generated code in C. This example shows that the software engineering process can be freely mixed with general technical computing that supports it in a single, content-rich document. The notebook file on the left is both the model definition and the requirement documentation combined.
Go back to the project homepage.