--- layout: fc_discuss_archives title: Message 17 from Frama-C-discuss on October 2015 ---
Your function *is* doing something, and the post-condition is exactly your loop invariant with (i == end), hence it finally holds. L. > Le 5 oct. 2015 à 17:19, Christoph Rauch <christoph.rauch at fau.de> a écrit : > > >> On 05 Oct 2015, at 16:54, Loïc Correnson <loic.correnson at cea.fr> wrote: >> >> Yes ! Indeed, there is nothing about the preservation of the elements in the array across the function. >> Something like : >> /*@ ⦠>> ensures >> \forall integer i ; start <= i < end ==> >> \exists integer j ; start <= j < end ==> a[i] == \old( a[j] ) ; >> */ >> (and the other way). > > Of course, that is a post-condition that should *also* hold in the final algorithm, and indeed I have formulated this using the Permut predicate from the Jessie tutorial. I only left it out here, because it didnât change the result and it shouldnât be a necessary condition. After all, the contract I gave would be fulfilled by a function that sets a[end-1] to INT_MAX. But doing nothing is not such a function and WP shouldnât be able to prove that the post-condition holds. > > -- > Christoph > _______________________________________________ > Frama-c-discuss mailing list > Frama-c-discuss at lists.gforge.inria.fr > http://lists.gforge.inria.fr/mailman/listinfo/frama-c-discuss