--- layout: fc_discuss_archives title: Message 17 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



Several mistakes in your code:
 - loop assigns are incomplete : missing `rev`. Indeed, assigns must be completely proved _before_ any attempt to prove another property (otherwise, proof-obligations are inconsistent) ;
 - you need to specify that, during the loop, indices are monotonic. With proper renaming of variables, during loop:
   * P elements have been found with the desired property, and Q without.
   * 0 <= P && 0 <= Q && P+Q <= length
   * first indices ind[0..P-1] are all in range (0..P+Q-1)
   * last indices ind[length-Q..length-1] are all in range (0..P+Q-1)
   * ind[rev[k]] == k for all k in (0..P+Q-1)

The monotonicity of indices is necessary to apply the induction hypothesis ind[ref[k]]==k for small enough k?s.

L.

> Le 25 f?vr. 2015 ? 13:49, Marko Sch?tz Schmuck <MarkoSchuetz at web.de> a ?crit :
> 
> At Mon, 16 Feb 2015 11:29:02 +0100,
> Lo?c Correnson wrote:
>> 
>> 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.
> 
> thanks for the recommendation. I pursued this a bit, but got stuck
> again. The following PO is not discharged:
> 
> Goal Assigns (file partition-mine-momomorphic-ghost.c, line 17) in 'partition' (4/4):
> Effect at line 21
> partition-mine-momomorphic-ghost.c:21: warning from Typed Model:
> - Warning: Call assigns everything, looking for context inconsistency
>   Reason: Cast with incompatible pointers types (source: sint8*) (target: sint32*)
> Let x_0 = 4*(to_uint32 length_4).
> Let a_0 = (shift arr_6 0).
> Let a_1 = (shift ind_7 0).
> Assume {
>  (* Domain *)
>  Type: (is_sint32 length_4).
>  (* Heap *)
>  Have: (linked Malloc_4).
>  (* Pre-condition (file partition-mine-momomorphic-ghost.c, line 11) in 'partition' *)
>  (* Pre-condition: *)
>  Have: (0<=length_4) /\ (valid_rw Malloc_4 a_0 length_4)
>        /\ (valid_rw Malloc_4 a_1 length_4).
>  (* Pre-condition (file partition-mine-momomorphic-ghost.c, line 12) in 'partition' *)
>  (* Pre-condition: *)
>  Have: (separated a_0 length_4 a_1 length_4).
>  (* Pre-condition (file partition-mine-momomorphic-ghost.c, line 13) in 'partition' *)
>  (* Pre-condition: *)
>  Have: (4*length_4)<=4294967295.
>  (* Assertion 'rte,signed_overflow' (file partition-mine-momomorphic-ghost.c, line 20) *)
>  (* partition-mine-momomorphic-ghost.c:20: Assertion 'rte,signed_overflow': *)
>  Have: -2147483647<=length_4.
>  (* Assertion 'rte,unsigned_overflow' (file partition-mine-momomorphic-ghost.c, line 21) *)
>  (* partition-mine-momomorphic-ghost.c:21: Assertion 'rte,unsigned_overflow': *)
>  Have: 0<=x_0.
>  (* Assertion 'rte,unsigned_overflow' (file partition-mine-momomorphic-ghost.c, line 21) *)
>  (* partition-mine-momomorphic-ghost.c:21: Assertion 'rte,unsigned_overflow': *)
>  Have: x_0<=4294967295.
> }
> Prove: false.
> Prover Alt-Ergo returns Unknown
> 
> I suspect it is related to the implicit use of __builtin_alloca, but
> could not yet find or come up with a way to handle it.
> 
> Any hints, ideas?
> 
> Thanks in advance,
> 
> Marko
> 
>>> 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
>> 
>> _______________________________________________
>> Frama-c-discuss mailing list
>> Frama-c-discuss at lists.gforge.inria.fr <mailto:Frama-c-discuss at lists.gforge.inria.fr>
>> http://lists.gforge.inria.fr/cgi-bin/mailman/listinfo/frama-c-discuss <http://lists.gforge.inria.fr/cgi-bin/mailman/listinfo/frama-c-discuss>
> <partition-mine-momomorphic-ghost.c>_______________________________________________
> Frama-c-discuss mailing list
> Frama-c-discuss at lists.gforge.inria.fr <mailto:Frama-c-discuss at lists.gforge.inria.fr>
> http://lists.gforge.inria.fr/cgi-bin/mailman/listinfo/frama-c-discuss <http://lists.gforge.inria.fr/cgi-bin/mailman/listinfo/frama-c-discuss>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20150225/6907f0a7/attachment-0001.html>