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

我有一个简单的矩阵转置函数，我想用后置条件来验证它

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];
                }

}

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

您想要证明的属性实际上无法用 ACSL 提供的简单函数合约来表达。即函数契约指定在单个函数调用期间应该发生什么。你所追求的问题two相关函数调用。

Frama-C 有一个外部（且非常实验性）插件，可让您编写此类属性：RPP（关系属性证明器），可在https://github.com/lyonel2017/Frama-C-RPP https://github.com/lyonel2017/Frama-C-RPP，一些文章描述了该技术（称为自作曲），它是基于https://hal-cea.archives-ouvertes.fr/cea-01808885 https://hal-cea.archives-ouvertes.fr/cea-01808885 and https://hal-cea.archives-ouvertes.fr/cea-01835470 https://hal-cea.archives-ouvertes.fr/cea-01835470

请注意，在当前状态下，RPP 有许多限制，特别是在处理指针方面，这可能会成为矩阵的问题。不过，也可以手动进行自组合，然后照常使用 WP。