Доказательство правильности преобразования матрицы в Frama- C - PullRequest
Новая
       22

Доказательство правильности преобразования матрицы в Frama- C

0 голосов
/ 28 апреля 2020

Я пытаюсь доказать простую транспонирование матрицы в Frama- C. В настоящее время у меня есть: 

#define N 3
void transpose_matrix(int [N][N], int, int, int[N][N]);
int main()
{
        int r=N;
        int c=N;
/* Storing element of matrix entered by user in array a[][]. */
        int a[N][N]={
                {1,1,1},
                {2,2,2},
                {3,3,3}
               };


       int trans[N][N];
       transpose_matrix(a,r,c,trans);
    return 0;
}

/*@
requires 0 < r <= N;
requires 0 < c <= N;
*/

void transpose_matrix(int a[N][N], int r, int c, int trans[N][N]){
        int  i,j;
/* Finding transpose of matrix a[][] and storing it in array trans[][]. */
/*@
loop invariant 0 <= i < r;
loop assigns r;
loop variant r - i;
*/
        for(i=0; i<r; ++i)
/*@
loop invariant 0 <= j < c;
loop assigns c, trans[0..c-1][0..r-1];
loop variant c - j;
*/
                for(j=0; j<c; ++j)
                {
                        trans[j][i]=a[i][j];
                }
return;

}

Но я не знаю, как перенести это на следующий уровень и на самом деле доказать что-то простое в моей функции (например, transpose (transpose a) = a ).

Некоторое время назад я задал похожий вопрос, и мне показалось, что ответ звучит так: «Вы не можете, это не то, для чего предназначен Frama- C». Это действительно так? Или я мог бы создать доказательство, которое фактически проверяло бы правильность моего алгоритма, как я мог это сделать в PlusCal или Coq?

...