Processed HOL4 output

val final_thm =
   |- HOLFOOT_SPECIFICATION (
   











      swap(; a_const, i_const, j_const)
        [w/r: ;  | data_array(#a_const, #m, dta:data) ★
            (#i_const < #m ) ★ (#j_const < #m )] {
         local (a = a_const), (i = i_const), (j = j_const), ti, tj;
         ti = (a + i)→dta;
         tj = (a + j)→dta;
         (a + j)→dta = ti;
         (a + i)→dta = tj;
      } [w/r: ;  |
            data_array(#a_const, #m,
               dta:SWAP_ELEMENTS j_const i_const data)]
      



















      two_way_sort(; a_const, m_const)
        [w/r: ;  | data_array(#a_const, #m_const, dta:data) ★
            (#m_const > 0) ★ pure(EVERY IS_BOOL_TO_NUM data)] {
         local (a = a_const), (m = m_const), i, j, temp;
         i = 0;
         j = (m − 1);
         /* Loop Invariant:
            [w/r: i, j, temp; a, m | data_array(a, m, dta:_rdata) ★
                (j < m) ★
                pure(PERM !data _rdata ∧ EVERY IS_BOOL_TO_NUM !data ∧
                     (∀n. n < i ⇒ (EL n _rdata = 0)) ∧
                     ∀n. j < n ∧ n < m ⇒ (EL n _rdata = 1))] */
         while (i ≤ j) {
            temp = (a + i)→dta;
            if (temp = 0) {
               i = (i + 1)
            } else {
               temp = (a + j)→dta;
               if (temp = 1) {
                  j = (j − 1)
               } else {
                  swap(; a, i, j); i = (i + 1); j = (j − 1);
               };
            };
         };
      } [w/r: ;  | data_array(#a_const, #m_const, dta:_rdata) ★
            pure(SORTED $<= _rdata ∧ PERM data _rdata)]
      
      
   ):
   thm

/* swap gets 3 call by value arguments: "a", "i", and "j".
   The precondition states that there is an array in memory starting
   at location "a", with size of constant "m". Moreover, the content
   "data" of the array is specified explicitly. 
   The indices "i" and "j" are smaller than "m" and therefore the array accesses are
   within the bound. */

swap (a,i,j) [data_array(a,#m,data) * i < #m * j < #m]{
  local ti, tj;

  /* Holfoot supports only very simple operations. There is no special
     expressions or commands for arrays. Arrays are accessed using explicit
     pointer arithmetic. For example, "(a+i) -> dta" means adding "i" to
     the value of "a" and looking up the value stored in memory at this position
     indexed by the tag "dta". More traditionally, it is written as "a[i]". 

     Moreover, memory lookups can not be used in expressions directly. They have
     to be stored in a local variable first. Therefore, the code becomes: */

  ti = (a + i) -> dta;    /* ti <- a[i] */
  tj = (a + j) -> dta;    /* tj <- a[j] */
  (a + j) -> dta = ti;    /* a[j] <- ti */
  (a + i) -> dta = tj;    /* a[i] <- tj */

  /* The post-condition states that there is still an array of the original size
     at location m. However, the data content changed. It now contains the
     original list with the elements at positions "i" and "j" swapped. The 
     quotation mark denote a HOL4-term. SWAP_ELEMENTS is a HOL4 function. */
} [data_array(a,#m,``SWAP_ELEMENTS j i data``)]


/* Holfoot does not support typing. All values are natural numbers. Therefore,
   Boolean values are mapped to numbers (True => 1, False => 0). 

   The function "two_way_sort" gets two call-by-value arguments "a" and "m".
   "a" is the location of an array containing some data "data". Because the
   size is not stored in the array directly, the argument "m" is used to
   pass the size of the array. The condition "m > 0" therefore demands that the
   array is not empty. Moreover the pure condition
   ``EVERY IS_BOOL_TO_NUM data`` demands that only Boolean values 
   (i.e. only 0 and 1) are stored in the array. */
 
two_way_sort (a, m) [data_array (a, m, data) * m > 0 *
                     ``EVERY IS_BOOL_TO_NUM data``] {
  local i, j, temp;
  i = 0;
  j = m - 1;
  while (i <= j)
    /* The loop invariant says that there is always an
       array of the right size at "a". This array contains some
       existentially quantified data "_rdata". (Following Smallfoot,
       the underscore is used to denote existential quantification).
       Moreover, the upper index "j" is always smaller than 
       the size of the array. There is a pure side-condition as well.
       It demands that "_rdata" is a permutation of "data" and that
       "data" contains only Boolean values. Moreover all
       array entries below "i" are 0, all above "j" are 1. 

       Notice that the termination of the loop is not proven. */        
    [data_array (a, m, _rdata) * j < m * 
     ``(PERM data _rdata) /\
       EVERY IS_BOOL_TO_NUM data /\
       (!n. n < i ==> (EL n _rdata = 0)) /\
       (!n. (j < n /\ n < m) ==> (EL n _rdata = 1))``] {

    temp = (a + i) -> dta;
    if (temp == 0) {
      i = i+1;
    } else {
      temp = (a + j) -> dta;
      if (temp == 1) {
        j = j-1;
      } else {
        swap(a, i, j);
        i = i+1;
        j = j-1;
      }
    }
  }
  /* The post-condition guarantees that there is still the array
     with size "m" at "a". However, it now contains some existentially
     quantified data "_rdata" such that "_rdata" is a permutation of
     the original data "data" and it is sorted according to the "<=" relation.

     Holfoot uses fault avoiding semantics. Therefore, it is implicitly
     guaranteed that all memory accesses were within the boundaries of the array.
     Moreover it is guaranteed that there is no memory leak, i.e. that no junk 
     is left on the heap. */ 
} [data_array (a, m, _rdata) * 
   ``(SORTED $<= _rdata) /\ (PERM data _rdata)``]