Функция транспонирования матрицы в FRAMA- C - PullRequest
Новая
       30

Функция транспонирования матрицы в FRAMA- C

1 голос
/ 07 апреля 2020

У меня есть простая матричная функция транспонирования, которую я хотел бы проверить с постусловием, таким как 

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

}

Возможно, я не думаю об этом правильно.

1 Ответ

2 голосов
/ 07 апреля 2020

Свойство, которое вы хотите доказать, на самом деле не может быть выражено с помощью простого контракта функции, предлагаемого ACSL. А именно контракт функции определяет, что должно произойти во время одного вызова функции. Что вас интересует, два вызова связанных функций.

Существует внешний (и очень экспериментальный) плагин Frama- C, который позволяет вам писать такие свойства : RPP (Relational Properties Prover), доступный по адресу https://github.com/lyonel2017/Frama-C-RPP, с некоторыми статьями, описывающими технику (известную как self-состав ), на которой он основан на https://hal-cea.archives-ouvertes.fr/cea-01808885 и https://hal-cea.archives-ouvertes.fr/cea-01835470

Обратите внимание, что в своем текущем состоянии RPP имеет много ограничений, особенно в отношении обработки указателей, что, вероятно, будет проблемой для матриц. Тем не менее, возможно, можно выполнить самостоятельную композицию вручную, а затем использовать WP как обычно.

...