--- layout: fc_discuss_archives title: Message 16 from Frama-C-discuss on October 2015 ---
> 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