--- layout: fc_discuss_archives title: Message 10 from Frama-C-discuss on June 2017 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] matrix addition



I want to prove the correctness of a simple function which adds two 3-by-3 matrices. Using wp plug-in, I can prove the assign clause but I can't prove the ensures clause (I use the real model for computing weakest preconditions). Did I forget a precondition, is it a known problem ?

Regards,

Arthur

/*@
requires \valid(A[0]+(0..2)) && \valid(A[1]+(0..2)) && \valid(A[2]+(0..2)) && \valid(B[0]+(0..2)) && \valid(B[1]+(0..2)) && \valid(B[2]+(0..2)) && \valid(result[0]+(0..2)) && \valid(result[1]+(0..2)) && \valid(result[2]+(0..2));
requires \separated(A[0]+(0..2), A[1]+(0..2), A[2]+(0..2), B[0]+(0..2), B[1]+(0..2), B[2]+(0..2), result[0]+(0..2), result[1]+(0..2), result[2]+(0..2));
assigns result[0][0..2], result[1][0..2], result[2][0..2];
ensures \forall integer p, q; 0 <= p <= 2 && 0 <= q <=2 ==> result[p][q] == A[p][q] + B[p][q];
@*/
void matrix_addition(float A[3][3], float B[3][3], float result[3][3]){
    
    /*@
    loop assigns i, result[0][0..2], result[1][0..2], result[2][0..2];
    loop invariant 0 <= i <= 3;
    loop invariant \forall integer k; 0 <= k < i ==> result[k][0] == A[k][0] + B[k][0] && result[k][1] == A[k][1] + B[k][1] && result[k][2] == A[k][2] + B[k][2];
    loop variant 2-i;
    @*/
    for (int i=0; i<3; i++){
        
        /*@
        loop assigns j, result[i][0..2];
        loop invariant 0 <= j <= 3;
        loop invariant \forall integer n; 0 <= n < j ==> result[i][n] == A[i][n] + B[i][n];
        loop variant 2-j;
        @*/
        for (int j=0; j<3; j++){
            
            result[i][j] = A[i][j] + B[i][j];
            //@ assert result[i][j] == A[i][j] + B[i][j];
        }
        
    }
    
}


--
  
Arthur CLAVIÈRE
Elève ingénieur SUPAERO - 2A
ISAE SUPAERO - Institut Supérieur de l'Aéronautique et de l'Espace
10 avenue Edouard Belin - BP 54032 - 31055 TOULOUSE CEDEX 4 FRANCE - http://www.isae-supaero.fr
Tel +33 5 61 33 80 80 - Fax (+33) 5 61 33 83 30
Plan d'accès/Access map
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20170619/d6ca8c1c/attachment.html>