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

  • Subject: [Frama-c-discuss] several WP questions
  • From: MarkoSchuetz at web.de (Marko Schütz Schmuck)
  • Date: Thu, 12 Feb 2015 13:48:32 -0400
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>