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] several WP questions

Hi,
Instead of an axiomatic definition of the permutation, you should introduce the inverse indices array as a ghost variable, say ?rev?, maintain this array during the loop with ghost code and prove that rev[ind[i]]==i in suitable ranges.
We already used such a technique to prove a bubble-sort algorithm with permutation indices bookkeeping.
This is much easier than converting C-arrays to abstract lists : I?m afraid you will need, at some point, some frame lemmas to compare `arrayToList{A}` and `arrayToList{B}` when you have memory updates between points `A` and `B`.
L.



> Le 12 f?vr. 2015 ? 18:48, Marko Sch?tz Schmuck <MarkoSchuetz at web.de> a ?crit :
> 
> Dear All,
> 
> verifying an implementation of partition I have something like
> 
> /*@ axiomatic List {
>  @ type listInt;
>  @ logic listInt nil;
>  @ logic listInt cons(integer x, listInt xs);
>  @ logic listInt append(listInt xs, listInt ys);
>  @ logic listInt arrayToList{L}(int *arr, integer length);
>  @ logic boolean member(integer elem, listInt xs);
>  @ axiom appendNil:
>  @   \forall listInt ys; append(nil, ys) == ys;
>  @ axiom appendCons:
>  @   \forall listInt xs, ys; \forall integer x; append(cons(x, xs), ys) == cons(x, append(xs, ys));
>  @ axiom arrayToListNull{L}:
>  @   \forall int *arr; \forall integer i; i == 0 ==> arrayToList{L}(arr, i) == nil;
>  @ axiom arrayToListN{L}:
>  @   \forall int *arr; \forall integer length, newLength; length > 0 && newLength == length-1
>  @   ==> arrayToList{L}(arr, length) == cons(\at(arr[0], L), arrayToList{L}(arr+1, newLength));
>  @ axiom memberNil:
>  @   \forall integer elem; !member(elem, nil);
>  @ axiom memberConsHead:
>  @   \forall integer elem; \forall listInt xs; member(elem, cons(elem, xs));
>  @ axiom memberConsTail:
>  @   \forall integer elem, x; \forall listInt xs; member(elem, xs) ==> member(elem, cons(x, xs));
>  @ predicate permutationLists(listInt a, listInt b);
>  @ axiom permutationListsNil:
>  @   permutationLists(nil, nil);
>  @ axiom permutationListsCons:
>  @   \forall listInt a1, a2, a3, ta, b1, b2, b3, tb; ta == append(a1, append(a2, a3))
>  @   && tb == append(b1, append(b2, b3)) && a2 != nil && a2 == b2
>  @   && permutationLists(append(a1, a3), append(b1, b3))
>  @   ==> permutationLists(ta, b1);
>  @}
>  @*/
> 
> /*@
>  @predicate permutation{L1, L2}(int *a, int *b, integer count) =
>  @  permutationLists(arrayToList{L1}(a, count), arrayToList{L2}(b, count));
>  @
>  @predicate property(integer x);
>  @*/
> 
> /*@ assigns \nothing;
>  @ ensures \result == \true <==> property(x);
>  @*/
> int property(int x);
> 
> /*@ requires length >= 0 && \valid(arr+(0..length-1)) && \valid(ind+(0..length-1));
>  @ ensures 0 <= \result < length;
>  @ ensures \forall int i; 0 <= i <= \result ==> property(arr[ind[i]]);
>  @ ensures \forall int i; \result + 1 <= i < length ==> !property(arr[ind[i]]);
>  @ assigns ind[0..length-1];
>  @*/
> int partition(int *arr, int *ind, int length) {
>  int gr = 0, j = length-1;
>  /*@ loop invariant 0 <= gr <= j+1 <= length ;
>    @ loop invariant \forall integer i; 0 <= i < gr ==> property(arr[ind[i]]);
>    @ loop invariant \forall integer i; j+1 <= i < length ==> !property(arr[ind[i]]);
>    @ loop invariant permutationLists(append(arrayToList{Here}(ind, gr), arrayToList{Here}(ind+j+1, length-j)), arrayToList{Here}(arr, gr + length - j));
>    @ loop variant j - gr;
>    @*/
>  while (gr <= j) {
>    if (property(arr[gr + length - 1 - j])) {
>      ind[gr] = gr + length - 1 - j;
>      //@ assert ind[gr] == gr + length - 1 - j && property(arr[gr + length - 1 - j]) && property(arr[ind[gr]]);
>      gr++;
>    } else {
>      ind[j] = gr + length - 1 - j;
>      j--;
>    }
>  }
>  return gr-1;
> }
> 
> Frama-C Neon/WP failed to discharge the second part of the invariant,
> so I started experimenting with some assertions. When I write the
> assertion as above the PO is not discharged. When I turn on 'split'
> the first of the three generated POs is discharged. When I write the
> three assertions as separate assertions:
> 
>      //@ assert ind[gr] == gr + length - 1 - j;
>      //@ assert property(arr[gr + length - 1 - j]);
>      //@ assert property(arr[ind[gr]]);
> 
> then the first and the last are discharged.
> 
> Any hints on how I should deal with this and how I could get the
> invariant proved?
> 
> Thanks and best regards,
> 
> Marko_______________________________________________
> Frama-c-discuss mailing list
> Frama-c-discuss at lists.gforge.inria.fr
> http://lists.gforge.inria.fr/cgi-bin/mailman/listinfo/frama-c-discuss