2.1.3.8 Insertion sort array

This version of insertion sort does not move cells of the list but only moves data between cells. Then, it simulates the insertion sort on arrays.

C code 
Spl encoding

#include "intlist.h"

/* acyclic(x) and l[x]==_l and data(x) */
void insertSortArr(intlist x) {
  intlist xi, y;
  int m, n;
  xi = y = NULL;
  xi = x->next;
  while (xi != NULL) {
    y = x;
    while (y != xi && y->data <= xi->data) {
      y = y->next;
    }
    m = xi->data;
    while (y != xi) {
      n = y->data;
      y->data = m;
      m = n;
      y = y->next;
    }
    xi->data = m;
    xi = xi->next;
  }
}


var _data:real, _free:real, _len:real, 
    _new:real, _next:real, _null:real,
    x:real, xi:real, y:real, yi:real,
    _l:int, _k:int, S:int, m:int, n:int;
begin
  assume (x == 0); 
  xi = _null; 
  y = _null; yi = _null;
  xi = x * _next;
  while xi != _null do
    y = x;
    while y != xi and y * _data <= xi * _data do
      yi = y * _next;
      y = _null;
      y = yi;
      yi = _null;
    done;
    m = xi * _data;
    while y != xi do
      n = y * _data;
      y = m / _data; 
      m = n;
      yi = y * _next;
      y = _null;
      y = yi;
      yi = _null;
    done;
    y = _null;
    xi = m / _data;
    yi = xi * _next;
    xi = _null;
    xi = yi;
    yi = _null;
  done;
end

Results

Domain 
Param. 
Log file 
Interesting constraint

LSUM-PRD
Anon=(0,1)
log/intlist-insertSortArr-lsum-prd-01
x(n1) and S(n1)+d(n1)=S and l[n1]=l

LSUM-REL
Anon=(0,1)
log/intlist-insertSortArr-lsum-rel-01
x(n1) and S(n1)+d(n1)=S and l[n1]=l

MSET
TODO
TODO
TODO

UCONS
TODO
TODO
x(n1) and \forall y1\in n1 \implies d(n1) <= d(y1) and
 \forall y1, y2\in n1 \implies d(y1) <= d(y2)