Frama-C-discuss mailing list archives

This page gathers the archives of the old Frama-C-discuss archives, that was hosted by Inria's gforge before its demise at the end of 2020. To search for mails newer than September 2020, please visit the page of the new mailing list on Renater.

[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] questions after attempting to use jessie on a matrix library

  • Subject: [Frama-c-discuss] questions after attempting to use jessie on a matrix library
  • From: agoodloe at gmail.com (Alwyn Goodloe)
  • Date: Wed, 7 Jul 2010 01:00:05 -0400
In my first trials with frama-c's jessie plugin,
I'm trying to use Frama-C/Jessie to verify a simple library of
matrix operations, but I have a few questions.  We will consider two of
the simplest functions.

The first simply allocates space for a m x n matrix. It seems
that the spec should be

/*@
  @ requires m > 0 && n >0 ;
  @ assigns \result;
  @ ensures \valid(\result) && (\forall int i;
  @   0<= i < m  ==>  \valid(\result+i*n + (0..n-1)));
 */


I've annotated the program as follows:

double** allocM (int m,int n)
{
        int  i = 0;
        double** p;
        p= malloc(m *sizeof(double *));

        /*@ assert \valid(p+ (0..m-1)); */

        if (p == NULL)
                {
                printf("out of memory\n");
                return NULL;
                }


        /*@  loop invariant \forall int k;
          @ 0 <= k < i <=m ==> \valid(p+k*n+ (0..n-1));
          @ loop variant  m-i;
          @ */

        for (i = 0; i<m;i++)
        {

             if (i < 0) break;

             /*@ assert 0 <= i <= m; */
                (p)[i] = malloc(n * sizeof(double *));
                /*@ assert \valid(p+i*n+(0..n-1)); */
                if((p)[i] == NULL)
                        {
                        return NULL;
                        }
        }
        return p;
}


==================================
The first question I have is this the right way to use
\valid in this context.
=============================
The second example is equally  simple it simply creates nxm matrix of ones.
Initially, my first thought was that it should be  annotated something like
:



/*@ requires m > 0 && n > 0;
  @  assigns \result;
  @  ensures  \valid(\result);
  @  ensures  \forall int i; \forall int j;
  @       0 <= i < m && 0 <= j <n ==> \result[i][j] == 1;
  @*/

double** ones(int m,int n)
{
    /*@ assert m > 0  && n > 0; */

    double **c = allocM(m,n);
    /*@ assert  \valid(c); */
    int i,j;

    /*@ loop assigns c[0..m-1][0..n-1];
      @ loop invariant \forall int k; \forall int l;
      @  (0<= i <=m && 0 <= j <= n) && ( 0 <= k < i && 0 <= l < j ==>
c[k][l] == 1);
      @*/

  for (i = 0; i<m; i++){
        for (j = 0; j<n;j++){
            c[i][j] = 1;
       /*@ assert c[i][j] == 1; */
        }
    }
    return c;
}

======================

 I didn't see any nested loop examples or multidimensional array examples
so I'm doing things a bit by trial and error.

 From my first trials it seems like you have to annotate each of the
nested loops separately??  I'm wondering if even simple nested loops is
too much for the automated provers because even after playing with the
invariant locations, the automated provers couldn't discharge even the
simple loop
invariant. I don't mind going to interactive proof, but just wanted
any feedback I could get.



Based on a dereferencing obligation is seems I need to show   \valid
c[i][j]
or actually something like \valid(c +i*m+j) before the c[i][j]
dereference???

I'm sure these questions are a bit silly but this really my first real try
with this tool.
==================

Any help is appreciated.








-- 
Alwyn E. Goodloe, Ph.D.
agoodloe at gmail.com

Computer Scientist
National Institute of Aerospace
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20100707/ece4224e/attachment.htm>