--- layout: fc_discuss_archives title: Message 8 from Frama-C-discuss on February 2015 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] several WP questions



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
-------------- next part --------------
A non-text attachment was scrubbed...
Name: not available
Type: application/pgp-signature
Size: 181 bytes
Desc: OpenPGP Digital Signature
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20150212/c3ae5274/attachment.sig>