|
|
||
|
The most basic correctness checks are those related to the modeling language grammar. These checks need to be completed before any other verification or code generation activity is performed, as without correct grammar nothing is guaranteed to be consistent.
Grammar checks are run by default for each newly defined (or replaced) operation - this default check can be switched off by means of configuration options, which can be useful for batch processing, but for interactive use from Mathematica notebooks it is recommended to leave them on.
When the automatic grammar check completes successfully, a green confirmation message is displayed:
In fact, this confirmation message reports also successful completion of names and flow checks.
The grammar check for all operations in the model can be invoked explicitly as well:
It is also possible to pick only some of the packages for the check:
and a single selected operation can be analyzed as well:
As described in the chapter on general FMT conventions, each of these reports exists also in the raw version, which can be useful for further algorithmic processing, for example:
This is a nested Association object, reporting grammar checks for all (or selected) packages and within each package, for all (or selected) operations.
Grammar checks become more interesting when there are actual errors - and since the grammar reduction process involves also expression reduction, proper typing is considered to be part of the grammar as well. For example, the following has a typing error:
The automatic grammar check failed and the subsequent name and flow checks were not even attempted. The same failure can be seen with checks invoked explicitly:
And the raw report indicates the problem as well:
These reports do not show the exact nature of the failure and other operations are needed to inspect the problem. This is facilitated by the interactive buttons that are displayed above, but only with output formatted for such display; raw reports do not contain any interactive elements. Pressing the “Show grammar reductions” button, which is displayed after detecting a problem with newly defined or replaced operation, is equivalent to running the following:
This diagram shows the consecutive steps of grammar reductions for the selected operation body. Here, the process got stuck after just three steps and the reason for it getting stuck is that the assignment operation expects compatible types on both sides. Since it is not possible to assign Boolean value to an integer variable, the process cannot continue any longer.
Everything that prevents the grammar reduction process from continuing is considered to be a grammar error and grammar-correct bodies are those that just reduce to a single symbol True.
The "Show details" button, which is displayed for showGrammarChecks, has a different effect - the reason is that showGrammarChecks performs checks for multiple operations (possibly for all operations within the given model) and the results can be mixed, when some checks pass and some others fail. This can be demonstrated with additional (good) operation:
Now, when the checks are requested for the whole model, the results for individual operations will be mixed, but the model as a whole is considered wrong:
Pressing the “Show details” button reveals more detailed report with results for each operation in the set:
The operations are grouped by package and for each operation a short summary is displayed - green “OK” if the grammar check is successful for that operation and red “Failed” otherwise, with accompanying button “show tree” to trigger the display of grammar reduction steps in a separate window.
This scheme allows the user to perform the most basic grammar checks with minimum commands - just following the buttons is sufficient to diagnose the problem.
A dedicated function exists to quickly display only the last step from the grammar reduction process:
Operations with correct grammar always reduce to a single symbol True:
The last step above is a result of a straightforward reduction of the whole assignment operation, when both involved types are found to be compatible.
It is beneficial to occasionally study such sequences of grammar reduction steps for correct operations to get the idea of how different constructs are represented (a dedicated reference chapter contains the whole list of such representations) and consequently, what can prevent them from moving forward. Things to consider are:
An important note, related mostly to type compliance, is that an operation that was once correct with respect to grammar checks might begin to fail after modifications performed in other parts of the model. For example, when the type definition is changed or a package-level data object is modified to use a different type, the operation body that relied on these entities might become incorrect. This means that grammar check reports should not be considered stable when other changes in the model are applied later on.
Those operations that have their grammar completely wrong - to the point that they are no longer proper Wolfram expressions (a typical error in this category is a bracket mismatch) - are not even analyzed with regard to FMT rules; such errors are reported directly by Mathematica.
Previous: Model synthesis, next: Name checks
See also Table of Contents.