#include<vcc.h>
#include<limits.h>

#define MAXLEN 10

typedef struct queue {
  // Abstract queue
  _(ghost int qmap[\natural])
  _(ghost \natural abeg, aend, alen)
  _(invariant abeg <= aend)
  _(invariant alen == aend - abeg)
  _(invariant alen <= MAXLEN)
  // Concrete queue
  int A[MAXLEN];         
  unsigned int beg;     
  unsigned int end;       
  unsigned int len;
  _(invariant 0 <= beg && beg < MAXLEN)
  _(invariant 0 <= end && end < MAXLEN)
  _(invariant 0 <= len && len <= MAXLEN)
  _(invariant (beg < end) ==> (len == end - beg))
  _(invariant (beg == end) ==> ((len == 0) || (len == MAXLEN)))
  _(invariant (beg > end) ==> (len == (MAXLEN - beg) + end))
  // Gluing invariant
  _(invariant (beg < end) ==> \forall \natural k; (0 <= k && k < len) ==> A[beg+k] == qmap[abeg+k])
  _(invariant (beg >= end && len > 0) ==> \forall \natural k; (beg <= k && k < MAXLEN ==> A[k] == qmap[abeg+(k-beg)])) 
  _(invariant (beg >= end && len > 0) ==> \forall \natural k; (0 <= k && k < end ==> A[k] == qmap[abeg+(MAXLEN-beg)+k])) 
  _(invariant len == alen)
} queue;
                          
void init(queue *p) 
_(writes \span(p))
_(ensures \wrapped(p))
{
  _(ghost p->qmap = \lambda \natural i; 0)
  _(ghost p->abeg = 0)
  _(ghost p->aend = 0)
  _(ghost p->alen = 0)
  
  p->beg = 0;           
  p->end = 0;
  p->len = 0;     
  _(wrap p)        
}                         


void enq(queue *p, int newval)
_(requires \wrapped(p))
_(requires p->len < MAXLEN)
_(writes p)
_(ensures p->alen == \old(p->alen)+1)
_(ensures \forall unsigned k; k < \old(p->alen) ==> p->qmap[(p->abeg)+k] == \old(p->qmap[(p->abeg)+k]))
_(ensures p->qmap[p->aend -1] == newval)
_(ensures \wrapped(p))
{
  _(unwrap p)
  // Abstract enq
  _(ghost p->qmap = \lambda \natural i; (i == p->aend) ? newval: p->qmap[i])
  _(ghost p->aend = p->aend + 1)
  _(ghost p->alen = p->alen + 1);
  // Concrete enq
  p->A[p->end] = newval;          
  if (p->end < MAXLEN-1)     
    (p->end)++;                
  else                       
    p->end = 0;              
  p->len++;
  _(wrap p)
	return;                  
}    

int deq(queue *p)
_(requires \wrapped(p))
_(requires p->alen > 0)
_(writes p)
_(ensures (\result == \old(p->qmap[p->abeg])))
_(ensures \wrapped(p))
{
  int res;
  _(unwrap p)
  // Abstract deq
  _(ghost p->abeg = p->abeg + 1)
  _(ghost p->alen = p->alen - 1);
  // Concrete deq
  res = (p->A)[p->beg];
  if (p->beg < MAXLEN-1)     
    p->beg++;                
  else                       
    p->beg = 0;              
  p->len--;
  _(wrap p)
  return res;                  
}