请求解决Frama-C AstraVer验证C循环排序函数的剩余Safety与Behavior验证目标问题

我目前正在对C语言实现的循环排序函数做全代码验证，用ACSL注解配合Frama-C的AstraVer后端，在Why3 GUI里查看验证结果，现在还差几个目标没完成：

• Safety部分：67/68，还差一个「loop variant decrease」目标未证明
• Behavior部分：32/39，还有多个目标待完成

以下是各部分的验证结果截图：

• Safety部分：
  
• Behavior第一部分：
  
• Behavior第二部分：
  

这是我当前的循环排序代码（带ACSL注解）：

/*@ predicate sorted(int *array, integer first, integer last) =
   @    \forall integer i;
   @        first < i < last ==> array[i - 1] <= array[i];
*/

/*@
  @ requires array != \null; 
  @ requires \valid(array + (0 .. size-1));
  @ requires size >= 0; 
  @ assigns array[0..size-1]; 
  @
  @ ensures \forall integer i; 0 <= i < size ==> array[i] >= \old(array[i]);
  @ ensures sorted(array, 0, size);
  */
void sorting(int *array, int size) {
    int bound, idx, x, i, tmp;

    /*@ loop invariant 0 <= bound <= size - 2; 
      @ loop variant size - bound;    
      @*/
    for (bound = 0; bound <= size - 2; bound++) {
        /* @assert bound < size; */ 
        x = array[bound];
        idx = bound;

        /*@ loop invariant bound + 1 <= i <= size;
          @ loop invariant idx >= bound;                           
          @ loop invariant idx <= size-1;                          
          @ loop assigns i, idx;
          @ loop variant size - i;   
          @*/
        for (i = bound + 1; i < size; i++) {
            /*@ assert i < size; @*/
              
            if (array[i] < x) {
                /*@ assert idx + 1 < size; @*/
                idx++;
            }
        }

        if (idx == bound) {
            continue;
        }

        
        /*@ loop invariant idx >= bound && idx < size; 
          @ loop assigns idx;
          @ loop variant size - idx;
        @ */
        while (x == array[idx]) {
            /*@ assert bound <= idx < size; */ 
            idx += 1;
            /*@ assert idx < size; */
        }

        if (idx != bound) {
            /*@ assert idx < size; */
            tmp = array[idx];
            array[idx] = x;
            x = tmp;
        }
    
    /*@
      @ loop invariant bound <= idx < size;
      @ loop assigns idx, tmp, x, i, array[bound .. size-1];
      @ loop variant idx - bound;
    @ */
    
        while (idx != bound) {
            /*@ assert bound <= idx < size;  */
            idx = bound;

            /*@ loop invariant bound < i <= size;     
              @ loop invariant idx >= bound;
              @ loop invariant idx <= size-1;
              @ loop assigns i, idx; 
              @ loop variant size - i;         
             @*/
            for (i = bound + 1; i < size; i++) {
                if (array[i] < x) {
                    /*@ assert idx + 1 < size; */
                    idx += 1;
                }
            }
         
            /*@ assert idx < size; */
            /*@ 
              @ loop invariant idx >= bound && idx < size;
              @ loop assigns idx;
              @ loop variant size - idx;  
              @ */
            while (x == array[idx]) {
                /*@ assert idx + 1 < size; */
                idx += 1;
                /*@ assert idx < size;  */
            }
            /* @assert idx < size; */
            if (x != array[idx]) {
                /* @assert idx < size; */
                tmp = array[idx];
                /* @assert idx < size; */
                array[idx] = x;
                x = tmp;
            }
        }
    }
}

我还尝试过定义置换相关的公理，代码如下，但验证效果没提升，而且我觉得用公理有点像“作弊”，不太想用这种方式：

/*@ axiomatic Permut {
  @ predicate permut{L1,L2}(int *t1, int *t2, integer n);
  @     axiom permut_refl{L}:
  @         \forall int *t, integer n; permut{L,L}(t,t,n);
  @     axiom permut_sym{L1,L2}:
  @         \forall int *t1, *t2, integer n;
  @             permut{L1,L2}(t1,t2,n) ==> permut{L2,L1}(t2,t1,n);
  @     axiom permut_trans{L1,L2,L3}:
  @         \forall int *t1, *t2, *t3, integer n;
  @             permut{L1,L2}(t1,t2,n) && permut{L2,L3}(t2,t3,n)
  @             ==> permut{L1,L3}(t1,t3,n);
  @     axiom permut_exchange{L1,L2}:
  @         \forall int *t1, *t2, integer i, j, n;
  @         swap{L1, L2}(t1, t2, i, j, n) ==> permut{L1,L2}(t1,t2,n);
  @ }
  @*/

我感觉ACSL引理可能是解决问题的关键，但自己想不出有效的引理来补充。有没有大佬能给点建议，我该加哪些注解或者调整现有注解，才能完成剩余的验证目标？

备注：内容来源于stack exchange，提问作者st_dec