在FRAMA-C中验证矩阵转置函数

Question

我有一个简单的矩阵转置函数，我想用一个后置条件进行验证，使>]

matrix_transpose(matrix_transpose(original_matrix)==original_matrix
的语法是什么？我已经尝试过

ensures \result(\result)==a;
其中a是原始矩阵，但似乎不起作用。

编辑：这是我的代码

    void transpose_matrix(int[][10],int,int);
int main()
{       
        int r=3;
        int c=3;
        int a[10][10]={
                {1,1,1},
                {2,2,2},
                {3,3,3}
               };

        transpose_matrix(a,r,c);


    return 0;
}
/*@
ensures \result(\result)==a;
*/

void transpose_matrix(int a[][10], int r, int c){
        int  trans[10][10],i,j;
        for(i=0; i<r; ++i)
                for(j=0; j<c; ++j)
                {       
                        trans[j][i]=a[i][j];
                }

}
也许我没有以正确的方式考虑这个问题。 

我有一个简单的矩阵转置函数，我想用后置条件进行验证，以使matrix_transpose（matrix_transpose（original_matrix）== original_matrix的语法是什么...

Answer 1

您要证明的属性不能真正由ACSL提供的简单功能合同来表示。即，功能协定指定在单个功能调用期间应发生的情况。您关注的是与[[two

相关的函数调用。