title: Frama-c loop invariant
body: <p>I just tried to prove a sort function in frama-c. However, when I proved the outer loop. </p>
  
  <pre><code>loop invariant 0 &lt;= i &lt;l;
  loop invariant 0 &lt; i &lt; l ==&gt; \forall int a,b; 0&lt;=b &lt;=l-i-1 &lt;=a &lt; l ==&gt; 
  t[a]&gt;=t[b];
  </code></pre>
  
  <p>There is always with the orange bullets. I refer to many examples and I cannot find the reason. Is there someone that can help me? Thanks!!
  The following is my source code:</p>
  
  <pre><code>/*@ predicate Swap{L1,L2}(int *a, integer l, integer i, integer j) =
   \at(a[i],L1) == \at(a[j],L2) &amp;&amp;
   \at(a[j],L1) == \at(a[i],L2) &amp;&amp;
   \forall integer k; k != i &amp;&amp; k != j
       ==&gt; \at(a[k],L1) == \at(a[k],L2);
   */
  
  
  /*@ predicate Sorted{L}(int *a, integer l, integer h) =
   \forall integer i,j; l &lt;= i &lt;= j &lt; h ==&gt; a[i] &lt;= a[j] ;
  */
  
  /*@ requires \valid(t + (0..l-1));
  requires 0 &lt;= i &lt; l;
  requires 0 &lt;= j &lt; l;
  assigns t[i],t[j];
  ensures Swap{Old,Here}(t,l,i,j);
  */
  
  
  void swap(int *t, int l, int i,int j){
  int tmp;
  tmp = t[i];
  t[i] = t[j];
  t[j] = tmp;
  return;
  }
  
  
   /*@ requires l &gt;0;
  requires \valid(t + (0..l-1));
  
  
  ensures (\forall integer a; 0&lt;=a &lt;l
   ==&gt; (\exists integer b; 0&lt;= b &lt; l
   ==&gt; \at(t[b],Old)== \at(t[a],Here) ));
  ensures Sorted{Here}(t, 0, l-1);
   */
  void sort(int *t, int l) { 
  int i;
  int j;
  i=j=0;
  
  /*@ loop invariant 0 &lt;= i &lt;l;
  loop invariant 0 &lt; i &lt; l ==&gt; \forall int a,b; 0&lt;=b &lt;=l-i-1 &lt;=a &lt; l ==&gt; 
  t[a]&gt;=t[b];
   */
  for (i=0;i&lt;l;i++) {
  
  
   /*@ 
  loop invariant 0&lt;= j &lt; l; 
  loop invariant 0 &lt; j &lt; l ==&gt;\forall int a; 0&lt;= a &lt;= j ==&gt; t[a]&lt;=t[j];     
   */
  for (j=0;j&lt;l-1;j++) {
  
    if (t[j] &gt; t[j+1]){ 
  
      swap(t,l ,j, j+1);}
      }
    }
  }
  </code></pre>
  
  <p>and I use </p>
  
  <pre><code>frama-c-gui -wp sort.c
  </code></pre>