--- layout: fc_discuss_archives title: Message 19 from Frama-C-discuss on October 2015 ---
> On 05 Oct 2015, at 17:32, Loïc Correnson <loic.correnson at cea.fr> wrote: > > Your function *is* doing something, and the post-condition is exactly your loop invariant with (i == end), hence it finally holds. > L. But shouldnât WP be unable to prove the loop invariant if the loop body is empty? The `swap(a+i, a+i)â effectively does nothing, you can just comment it out. You can go even further and remove everything inside the loop, leaving us with: /*@ @ requires end >= start >= 0; @ requires \valid(a+(start..end-1)); @ assigns a[start..end-1]; @ ensures \forall integer m; (start <= m < end) ==> a[m] <= a[end-1]; @ ensures Permut{Old,Here}(a, start, end-1); @*/ void bub_max(int* a, int start, int end) { /*@ @ loop assigns i, a[start..end-1]; @ loop invariant \forall integer m; (start <= m <= i) ==> a[m] <= a[i]; @*/ for (int i = start; i < end-1; i++) { // do nothing } which still verifies. If I completely remove the loop and thus the invariant, it doesnât verify. How can it possibly prove the loop invariant? As far as I understand the semantics of the loop invariant, this should not hold. -- Christoph