// ----------------------------------------------------------------------------
// Sorting lists by the Insertion Sort Algorithm
// ----------------------------------------------------------------------------

//****************************************
//CONSTANTS
//****************************************
val M:ℕ;
val N:ℕ;

//****************************************
//VARIABLES
//****************************************
type nat = ℕ[M];
type index = ℕ[N-1];
type array = Array[N,nat];
rectype(N) list = nil | cons(nat,list);

//****************************************
//SUPPORTING FUNCTIONS
//****************************************
//listLength(a:list)
//  returns the length of a list
fun listLengthRec(a:list,out:ℕ[N]):ℕ[N]
  decreases N-out;
  = match a with
  {
    nil -> out;
    cons(elem:nat,rem:list) -> listLengthRec(rem,out+1);
  };
fun listLength(a:list):ℕ[N] = listLengthRec(a,0);

//toArray(a:list):array
//  returns an array representation of a list
//  empty slots get filled with 0.
proc toArray(a:list):array
{
  var out:array := Array[N,nat](0);
  var b:list = a;
  for var i:ℤ[-1,N-1] := N-1; i≥0; i := i-1 do
  {
    match b with
    {
      nil -> ;
      cons(elem:nat,rem2:list) ->
      {
        out[i] = elem;
        b = rem2;
      }
    }
  }
  return out;
}

//toList(a:array,n:ℕ[N]):list
//  returns a list created by the last n elements of a
proc toList(a:array,n:ℕ[N]):list
{
  var out:list = list!nil;
  for var i:ℤ[0,N-1+1] := N-1-(n-1); i≤N-1; i:=i+1 do
  {
    out:=list!cons(a[i],out);
  }
  return out;
}

//****************************************
//SUPPORTING STATEMENTS
//****************************************
//isSorted(a:list)
//  returns if all elements of a are sorted
//  (high in front, low at the back)
pred isSorted(a:list)
  decreases listLength(a);
  <=> match a with
  {
    nil -> true;
    cons(elem:nat,rem:list) ->
    match rem with
    {
      nil -> true;
      cons(elem2:nat,rem2:list) ->
        elem2 ≤ elem ∧ isSorted(rem);
    };
  };

//isSortedArray(a:array,n:index)
//  returns if the last n elements are sorted
pred isSortedArray(a:array,n:ℕ[N]) <=>
  ∀i:index.(N-1-(n-1) ≤ i ∧ i ≤ N-1-1) => a[i] ≤ a[i+1];

//isPermutationOf(a:array,b:array)
//  returns if a is a permutation of b
pred isPermutationOf(a:array,b:array) <=>
  ∃p:Array[N,index].
    (∀i:index,j:index. i ≠ j => p[i] ≠ p[j])
    ∧ (∀i:index. a[i] = b[p[i]]);
//****************************************
//THEOREMS
//****************************************
pred ListsAndArraysAreIsomorph() <=>
  (∀a:list. a=toList(toArray(a),listLength(a)))
  ∧ (∀a:array.a=toArray(toList(a,N)))
  ∧ (∀a:list.isSorted(a)<=>isSortedArray(toArray(a),listLength(a)))
;
//****************************************
//CONDITIONS
//****************************************
//pre-Condition for insertionSort()
//  (*) trivial
pred pre(a:list) <=> true;

//post-Condition for insertionSort()
//  (*) result is sorted
//  (*) result is a permutation of a
pred post(a:list,result:list) <=>
  listLength(a) = listLength(result)
  ∧ isSorted(result)
  ∧ isPermutationOf(toArray(a),toArray(result));

//termination term for insertionSort()
//  each recursion the array-size gets smaller
fun termin(a:list):ℕ[N] = listLength(a);

//pre-Condition for insert()
//  (*) a is sorted
pred preInsert(x:nat,a:list) <=>
  listLength(a)<N
  ∧ isSorted(a);

//post-Condition for insert()
//  (*) result is sorted
//  (*) result is a permutation of a
pred postInsert(x:nat,a:list,result:list) <=>
  listLength(a)+1 = listLength(result)
  ∧ isSorted(result)
  ∧ isPermutationOf(toArray(list!cons(x,a)),toArray(result));

//termination term for insert()
//  each recursion the array-size gets smaller
fun terminInsert(x:nat,a:list):ℕ[N] = listLength(a);

//****************************************
//VERIFICATION CONDITIONS
//****************************************
//Verification Condition 1 for insert()
//   given the precondition,
//   (*) all preconditions of the subfunctions hold.
theorem VC_pre_insert(x:nat,a:list)
  requires preInsert(x,a);
  <=> match a with
  {
    nil -> true;
    cons(elem:nat,rem:list) -> elem > x => preInsert(x,rem);
  };

//Verification Condition 2 for insert()
//  given the precondition,
//  (*) the postcondition holds given that all subfunctions can
//      be defined by there postconditions.
theorem VC_post_insert(x:nat,a:list)
  requires preInsert(x,a);
  <=> match a with
  {
    nil -> postInsert(x,a,list!cons(x,a));
    cons(elem:nat,rem:list) ->
      if elem ≤ x then
        postInsert(x,a,list!cons(x,a))
      else
        ∀b:list.postInsert(x,rem,b)
        => postInsert(x,a,list!cons(elem,b));
  };

//Verification Condition 3 for insert()
//  given the precondition,
//  (*) the termination term always positive or zero
//  (*) each recursion reduces the termination term
theorem VC_term_insert(x:nat,a:list)
  requires preInsert(x,a);
  <=> terminInsert(x,a)≥0
  ∧ match a with
  {
    nil -> true;
    cons(elem:nat,rem:list) -> elem > x => terminInsert(x,rem)<terminInsert(x,a);
  };

//Verification Condition 1 for insertionSort()
//   given the precondition,
//   (*) all preconditions of the subfunctions hold.
theorem VC_pre(a:list)
  requires pre(a);
  <=> match a with
  {
    nil -> true;
    cons(elem:nat,rem:list) ->
      match rem with
      {
        nil -> true;
        cons(elem2:nat,rem2:list) ->
        pre(rem)
        ∧(∀b:list.post(rem,b)
        =>preInsert(elem,b));
      };
  };

//Verification Condition 2 for insertionSort()
//  given the precondition,
//  (*) the postcondition holds given that all subfunctions can
//      be defined by there postconditions.
theorem VC_post(a:list)
  requires pre(a);
  <=> match a with
  {
    nil -> post(a,list!nil);
    cons(elem:nat,rem:list) ->
      match rem with
      {
        nil -> post(a,list!cons(elem,rem));
        cons(elem2:nat,rem2:list) ->
        (∀b:list.post(rem,b)=>∀c:list.postInsert(elem,b,c)=>post(a,c));
      };
  };

//Verification Condition 3 for insertionSort()
//  given the precondition,
//  (*) the termination term always positive or zero
//  (*) each recursion reduces the termination term
theorem VC_termination(a:list)
  requires pre(a);
  <=> termin(a)≥0
  ∧ match a with
  {
    nil -> true;
    cons(elem:nat,rem:list) ->
      match rem with
      {
        nil -> true;
        cons(elem2:nat,rem2:list) -> termin(rem)<termin(a);
      };
  };

//****************************************
//  IMPLEMENTATION
//****************************************
//insert(x:nat,a:list):list
//  takes a element and inserts it into
//  a sorted list, so that the resulting
//  list is again sorted.
fun insert(x:nat,a:list):list
  requires preInsert(x,a);
  ensures postInsert(x,a,result);
  decreases listLength(a);
  = match a with
  {
    nil -> list!cons(x,a);
    cons(elem:nat,rem:list) ->
      if elem ≤ x then
        list!cons(x,a)
      else
        list!cons(elem,insert(x,rem));
  };

//insertionSort(a:list):list
//  sorts a list
fun insertionSort(a:list):list
  requires pre(a);
  ensures post(a,result);
  decreases termin(a);
  = match a with
  {
    nil -> list!nil;
    cons(elem:nat,rem:list) ->
      match rem with
      {
        nil -> list!cons(elem,rem);
        cons(elem2:nat,rem2:list) -> insert(elem,insertionSort(rem));
      };
  };