Processed HOL4 output

val final_thm =
   |- HOLFOOT_SPECIFICATION (
   























      create(r; n_const) [w/r: r;  | (0 < #n_const )] {
         local (n = n_const), d;
         r = new() ;
         d = new-block (n) [dta];
         r→size = n;
         r→len = 0;
         r→first = 0;
         r→data = d;
      } [w/r: r;  | ring_buffer(r, #n_const, dta: [])]
      







      clear(; b_const)
        [w/r: ;  | ring_buffer(#b_const, #s, dta: data)] {
         local (b = b_const); b→len = 0
      } [w/r: ;  | ring_buffer(#b_const, #s, dta: [])]













      
      head(r; b_const)
        [w/r: r;  | ring_buffer(#b_const, #s, dta: x::xs)] {
         local (b = b_const), v_f, v_d;
         v_f = b→first; v_d = b→data; r = (v_d + v_f)→dta;
      } [w/r: r;  | (r = #x) ★ ring_buffer(#b_const, #s, dta: x::xs)]
      

















      push(; b_const, x_const)
        [w/r: ;  | ring_buffer(#b_const, #s, dta: xs) ★
            pure(LENGTH xs < s)] {
         local (b = b_const), (x = x_const), v_s, v_f, v_l, v_d;
         v_f = b→first;
         v_l = b→len;
         v_s = b→size;
         v_d = b→data;
         (v_d + ((v_f + v_l) MOD v_s) )→dta = x;
         b→len = (v_l + 1);
      } [w/r: ;  | ring_buffer(#b_const, #s, dta: xs ++ [x_const])]
      

















      pop(r; b_const)
        [w/r: r;  | ring_buffer(#b_const, #s, dta: x::xs)] {
         local (b = b_const), v_f, v_d, v_l, v_s;
         v_f = b→first;
         v_d = b→data;
         v_l = b→len;
         v_s = b→size;
         r = (v_d + v_f)→dta;
         b→len = (v_l − 1);
         b→first = ((v_f + 1) MOD v_s);
      } [w/r: r;  | (r = #x) ★ ring_buffer(#b_const, #s, dta: xs)]
      













      test(b; x_const, y_const, z_const) [w/r: b;  | pure(T)] {
         local (x = x_const), (y = y_const), (z = z_const), h;
         create(b; 2);
         push(; b, x);
         push(; b, y);
         pop(h; b);
         assert [(h = x)];
         push(; b, z);
         pop(h; b);
         assert [(h = y)];
         pop(h; b);
         assert [(h = z)];
      } [w/r: b;  | ring_buffer(b, 2, dta: [])]
      
      
   ):
   thm

/* Holfoot is easily extensible with new predicates. In the
   corresponding proof-script-file "ring_buffer.hol" a new
   predicate "ring_buffer" is defined. A detailed explanation can
   be found there. Here is just a high level one:

   ring_buffer (b, s, d) 

   denotes that a heap location "b" a record
   with the entries "data", "size", "first" and "len" is stored.
   The entries "size", "first", "len" have the obvious meaning.
   The ring-buffer predicate "ring_buffer (b, s, d)" demands that 
   the value "s" is stored in "size" and the size of the data in "len".

   "data" however is in this case not the array itself, but a 
   pointer to an array of the right size "s". Doing the described mapping
   operation and using "first" and "len", the list "d" is a stored
   in this array. This list "d" is the logical content of the buffer. 
*/


/* The function "create" gets a call-by-reference argument "r" and
   a call-by-value one "n". "r" is used as the return value.
   "n" is the size of the created buffer. The pre-condition is "True",
   the procedure allocates a ring buffer and guarantees that there is
   an empty ring-buffer of the right size is there at the end. */
create(r;n) [0 < n] {
  local d;
  r = new();         /* Allocate memory for "r" */ 
  d = new(n) [dta];  /* Allocate memory for the array */

  /* initialise the record in "r" */
  r -> size = n;     
  r -> len = 0;
  r -> first = 0;
  r -> data = d;
} [ring_buffer(r,n,``[]``)]

/* "clear" gets a call-by-value argument "b" that has to
   point to some ring-buffer containing some arbitrary data of
   and arbitrary length. 
   It guarantees that there is in the end an empty ring-buffer
   of the right size at "b". Moreover, the semantics of separation
   logic guarantee, that there is no memory leak. */

clear(b) [ring_buffer(b,#s,data)] {
  b -> len = 0;
} [ring_buffer(b,#s,``[]``)]

/* "head" gets two arguments. A call-by-reference one "r" that is
   used a the return value and a call-by-value one "b".
   The precondition demands that
   "b" points to a ring-buffer of some size "#s".
   Notice that "#" denotes that "s" is a meta variable
   and not a program variable. The buffer logically contains the list
   starting with "x" and containing with a list "xs". Therefore the
   length of the buffer is implicitly given as "LENGTH (xs :: xs)". 

   The post-condition guarantees that there is still the same
   ring-buffer with the same content and that "r" has been updated to now
   contain the value "x". */
head(r;b) [ring_buffer(b, #s, ``x :: xs``)] {
  local v_f, v_d;

  /* read "first" and "data" from memory */
  v_f = b -> first;
  v_d = b -> data;

  /* lookup the right value */
  r = (v_d + v_f) -> dta;
} [r == #x * ring_buffer(b,#s,``x :: xs``)]


/* "push" gets two call-by-value arguments. "b" points to a ring-buffer.
   "x" should be inserted into this buffer.

   The precondition demands that
   "b" to point to a ring-buffer of some size "#s" containing
   logically the list "xs". Moreover, "LENGTH xs < #s" has to hold, i.e. the
   buffer is not full.

   The post-condition guarantees that "x" has been inserted at
   the end of the list and the length of the buffer has been incremented. */
push(b,x) [ring_buffer(b,#s,``xs``) * ``LENGTH xs < #s``] {
  local v_s, v_f, v_l, v_d;

  /* read the record */
  v_f = b -> first;
  v_l = b -> len;
  v_s = b -> size;
  v_d = b -> data;

  /* store x, the operation means 
     a [(first + len) MOD size] <- x */
  (v_d + ``(v_f + v_l) MOD v_s``) -> dta = x;
  
  /* update length */
  b -> len = v_l + 1;
} [ring_buffer(b,#s,``xs ++ [x]``)]


/* "pop" gets two arguments. A call-by-reference one "r" that is
   used a the return value and a call-by-value one "b".
   The precondition demands that
   "b" points to a ring-buffer of some size "#s".
   The buffer contains the list
   starting with "x" and containing with a list "xs". 

   The precondition of "pop" is the same as the precondition
   of "head". However, in contrast to "head", "x" is removed from
   the ring-buffer. The post-condition guarantees that there is the 
   ring-buffer without "x" and 
   that "r" has been updated to now contain the value "x". */
pop(r;b) [ring_buffer(b,#s,``x :: xs``)] {
  local v_f, v_d, v_l, v_s;

  /* read the record */
  v_f = b -> first;
  v_d = b -> data;
  v_l = b -> len;
  v_s = b -> size;

  /* lookup the right value */
  r = (v_d + v_f) -> dta;

  /* decrement length */
  b->len = v_l - 1;

  /* increment first */
  b->first = ``(v_f + 1) MOD v_s``;
} [r == #x * ring_buffer(b,#s,``xs``)]


/* The test code. Since Holfoot looks also for garbage left in
   memory an extra call-by-reference argument "b" is passed. 
   This argument is used to point at the newly created buffer.
   The benefit compared to a local variable is that it can be
   referred to in the post-condition.
*/
test(b; x, y, z) [] {
  local h;
  create(b;2);
  push(b, x);
  push(b, y);
  
  pop (h; b);
  assert [h == x];

  push(b, z);
  pop (h; b);
  assert [h == y];
  pop (h; b);
  assert [h == z];
} [ring_buffer(b, 2, ``[]``)]