--- layout: fc_discuss_archives title: Message 6 from Frama-C-discuss on August 2010 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] proving stack axioms with jessie



Well, I couldn't reproduce the soundness issue, so I can't confirm
that I eliminated it, but I suggest changing pop.spec so:


#include "stack.h"
#include "stack.pred"

/*@
   requires Valid(s);
   //ensures 0 == 1;  // jessie detects this

   behavior not_empty:
     assumes !Empty(s);
     assigns s->n;
     ensures s->n == \old(s->n) - 1;
//     ensures !Empty(s); // probably unsound

//     ensures \forall integer i; 0 <= i < s->n ==>
//        s->c[i] == \old(s->c[i]);
     ensures \result == 0;
//     ensures Valid(s); // probably unnecessary with assigns clause

   behavior empty:
     assumes Empty(s);
     assigns \nothing;
//     ensures Empty(s);
     ensures \result == -1;
//     ensures Valid(s);


*/
int pop(Stack* s);

The first clause I commented, "ensures !Empty(s);" is probably
unsound. The others should be unnecessary because they are implied by
the assigns clause that I recommend you use instead.

Pascal