In this page we will document the annotation generation part based on the usage of the BlockLibrary specification language. The basics of the approach can be summarized as the following:

Specification of the blocks using the BlockLibrary approach:

- Specification of the BlockType
- Specification of the semantics variation points (BlockVariants)
- Specification of the semantics computation modes
- If the block is an annotation block then specify if it is a ‘’Matlab annotation block’’ or a ‘’Subsystem annotation block’‘.
The input Simulink model is imported in the toolset (GeneAuto or P).

For each block in the imported model, we find the matching block type and semantics computation mode. This information in attached in the model to obtain an annotated code model of the system.

Danger

This approach must be documented.

- Then follows an expansion mechanism in order to generate loops in the code. This step of the generation will be documented in the following.
- Finally the code and the annotations models are printed to the chosen output format (C+ACSL / ADA+Spark / Java+JML).

This process is summed up in the following drawing.

As described in the BlockLibrary metamodel documentation, an AnnotationBlockType can be of two types: MatlabAnnotationBlockType or SubSystemAnnotationBlockType. In both cases, the annotation block type has a scope parameter.

The scope parameter might have four possible values:

- auto: The scope is computed automatically (Default)
- preCondition: The annotation must be printed as a pre-condition
- invariant: The annotation must be printed as an invariant
- postCondition: The annotation must be printed as a post-condition

According to the input elements of the input signals plugged in the input ports of the annotation block, it might not be always possible to choose between the four possibilities (except for auto which is always possible to choose).

We summarize the various case in the following table. The columns are for splitting according to the Scope parameter value. Lines are for splitting according to where the annotation block is plugged-in in the model:

only inPortscase is when the annotation block is plugged-in on signals that are directly connected toinportblocks.only outPortscase is when the annotation block is plugged-in on signals that are directly connected tooutportblocks.any other combinationcase is for the others possibilities.

AUTO | PRE | INVARIANT | POST | |
---|---|---|---|---|

only inPorts | behavior 1 | behavior 1 | behavior 2 | behavior 4 |

only outPorts | behavior 3 | behavior 2 | behavior 2 | behavior 3 |

any other combination | behavior 2 | behavior 2 | behavior 2 | behavior 2 |

Here are details about the previous behaviors

behavior 1pre-condition of system (at function level)behavior 2invariant (assert) placed just after input initializationbehavior 3post-condition of system (at function level)behavior 4if plugged-in system is a subsystem thenbehavior 2else error

The following picture represents possible annotation blocks in various configurations on a dumb system.

In the P and GeneAuto toolsets, input models are transformed to system models which are then converted to code models. Each block will at least be converted to one expression in the code model. A block computation is translated to a block of code. This block of code can be simple (only one statement) or complex (more than one statement). If the statement is an operation on a complex data type (a vector or a matrix), the computation code will result in a set of loop constructs in order to perform the operation. This transformation is denoted as the expansion mechanism.

As an example, summing two vectors will result in a loop over the elements of the vectors that are summed element-wise. For a matrix summation, we will need to generate two nested loops to perform the calculation on each dimension.

Using the expansion mechanism, we produce loops in the generated code. These loops must be verified for correctness. By expanding an operation (block computation) as nested loops we will need to ensure that the operation is well performed in the loops. In order to verify loop using annotations it is mandatory to write loop invariant(s).

Loop invariants denote expressions that must hold true at each computation of the loop. They ensure that the computation will be correct when the loop will finish.

We note during our experiments that simple operations performed on complex data types (vectors or matrices), need very idiomatic loop invariants. As specification of the blocks in the block library is done using high level languages like Matlab, the constraint expressions will contain complex operations. The application of the expansion mechanism in these annotations will not produce loops constructs but invariants that must hold during the computation of the corresponding loop.

The forthcoming elements are examples of loop invariants generation for a set of statements constructs. We will sort them by type of operation.

- In the following:
- outVar or outVarX (X \(\in \mathbb{N}\)) might be outputs of a block or a temporary variable.
- inVar or inVarY (Y \(\in \mathbb{N}\)) might inputs of a block or a parameter of a block.

**Unary operations [-]**

- For one-dimension input
- un_op in [-]
- max_i the size of input vector

**Matlab code**

1 | ```
outVar = <un_op> inVar
``` |

**ACSL annotations**

1 2 3 4 5 6 7 | ```
/*@ loop invariant \forall integer n; 0 <= n < i ==> outVar[n] == <un_op> inVar[n];
loop invariant 0 <= i <= max_i;
loop variant max_i - i;
*/
for (int i=0; i<max_i; i++){
...
}
``` |

- For two-dimensions input
- un_op in [-]
- (max_i,max_j) the size of input matrix

**Matlab code**

1 | ```
outVar = <un_op> inVar
``` |

**ACSL annotations**

1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 | ```
/*@ loop invariant \forall integer n,m; 0 <= n < i && 0 <= m < max_j ==> outVar[n][m] == <un_op> inVar[n][m];
loop invariant 0 <= i <= max_i;
loop variant max_i - i;
*/
for (i=0; i<max_i; i++){
/*@ loop invariant \forall integer m,n; 0 <= n < i && 0 <= m < max_j ==> outVar[n][m] == <un_op> inVar[n][m];
loop invariant \forall integer n; 0 <= n < j ==> outVar[i][n] == <un_op> inVar[i][n];
loop invariant 0 <= j <= max_j;
loop invariant 0 <= i < max_i;
loop assigns j;
loop variant max_j - j;
*/
for (j=0; j<max_j; j++){
...
}
}
``` |

**Binary operations [+,-,.*,./]**

- For one-dimension inputs
- bin_op in [+,-,.*,./]
- max_i the size of input vectors

**Matlab code**

1 | ```
outVar = inVar1 <bin_op> inVar2
``` |

**ACSL annotations**

1 2 3 4 5 6 7 | ```
/*@ loop invariant \forall integer n; 0 <= n < i ==> outVar[n] == inVar1[n] <bin_op> inVar2[n];
loop invariant 0 <= i <= max_i;
loop variant max_i - i;
*/
for (int i=0; i<max_i; i++){
...
}
``` |

- For two-dimensions inputs
- bin_op in [+,-,.*,./]
- (max_i,max_j) the size of input matrices

**Matlab code**

1 | ```
outVar = inVar1 <bin_op> inVar2
``` |

**ACSL annotations**

1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 | ```
/*@ loop invariant \forall integer n,m; 0 <= n < i && 0 <= m < max_j ==> outVar[n][m] == inVar1[n][m] <bin_op> inVar2[n][m];
loop invariant 0 <= i <= max_i;
loop variant max_i - i;
*/
for (i=0; i<max_i; i++){
/*@ loop invariant \forall integer m,n; 0 <= n < i && 0 <= m < max_j ==> outVar[n][m] == inVar1[n][m] <bin_op> inVar2[n][m];
loop invariant \forall integer n; 0 <= n < j ==> outVar[i][n] == inVar1 <bin_op> inVar2[i][n];
loop invariant 0 <= j <= max_j;
loop invariant 0 <= i < max_i;
loop assigns j;
loop variant max_j - j;
*/
for (j=0; j<max_j; j++){
...
}
}
``` |

**Matrix multiplication**

- For two matrices inputs
- inVar1 matrix of size r1*c1
- inVar2 matrix of size r2*c2
- Possible only if c1 = r2

**Matlab code**

1 | ```
outVar = inVar1 * inVar2
``` |

**ACSL annotations**

1 2 3 4 5 6 7 8 9 10 11 | ```
/*@ TODO: Add annotations
*/
for(i=0;i<r1;i++)
{
for(j=0;j<c2;j++)
{
outVar[i][j]=0;
for(k=0;k<r1;k++)
outVar[i][j]+=inVar1[i][k]*inVar2[k][j];
}
}
``` |