enrich ring-buffer-inv
 with
   procedures 
      create#  int : ring_buffer;
      clear#   : ring_buffer nonfunctional;
      head#  ring_buffer : elem;
      push#  elem : ring_buffer nonfunctional;
      pop#   : ring_buffer × elem nonfunctional;
      get#  int × array : elem;
      put#  int × elem : array nonfunctional;
      test#  elem × elem × elem :  nondeterministic;
      assert#  bool : ;
   variables 
      bv : bool; 
      a0 : elem; 
declaration 
   get : get# (i, ar; a)
           { 
              if 0 ≤ i ∧ i < n→i(# ar)
              then a := ar[i→n(i)]
              else abort
           };
   put : put# (i, a; ar)
           { 
              if 0 ≤ i ∧ i < n→i(# ar)
              then ar := ar[i→n(i), a]
              else abort
           };
   create : create# (i; buf)
              { 
                 buf := mk(mkarray(i→n(i)), i, 0, 0)
              };
   clear : clear# (;buf)
             { 
                buf := buf .len:= 0
             };
   head : head# (buf; a)
            { 
               get#(buf .first, buf .data; a)
            };
   push : push# (a; buf)
            { 
               let j = (buf .first + buf .len) % buf .size in put#(j, a; buf .data) ; buf := buf .len:= (buf .len + 1)
            };
   pop : pop# (;buf, a)
           { 
              get#(buf .first, buf .data; a) ; buf := buf .first:= ((buf .first + 1) % buf .size) ; buf := buf .len:= (buf .len - 1)
           };
   test
   : test# (a, b, c)
       { 
          let buf = [?], a0 = [?]
          in { 
                create#(2; buf) ; 
                push#(a; buf) ; 
                push#(b; buf) ; 
                pop#(; buf, a0) ; 
                assert#(a0 = a) ; 
                push#(c; buf) ; 
                pop#(; buf, a0) ; 
                assert#(a0 = b) ; 
                pop#(; buf, a0) ; 
                assert#(a0 = c)
             }
       };
   assert : assert# (bv)
              { 
                 if ¬ bv
                 then abort
              };
end enrich