--- layout: fc_discuss_archives title: Message 16 from Frama-C-discuss on February 2015 ---
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 > http://lists.gforge.inria.fr/cgi-bin/mailman/listinfo/frama-c-discuss -------------- next part -------------- A non-text attachment was scrubbed... Name: partition-mine-momomorphic-ghost.c Type: application/octet-stream Size: 1712 bytes Desc: not available URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20150225/614030ea/attachment.obj> -------------- 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/20150225/614030ea/attachment.sig>