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

#define RADIX 256

_(ghost \natural count)
unsigned int lo;
unsigned int hi;

void init()
  _(writes &hi, &lo, &count)
  _(ensures hi < RADIX && lo < RADIX)
  _(ensures count == (hi*RADIX) + lo)
{
  _(ghost count = 0)
  lo = 0;
  hi = 0;
}

void inc()
  // invariants and gluing
  _(requires count == (hi*RADIX) + lo)    
  _(requires hi < RADIX && lo < RADIX)
  // Precondition for inc
  _(requires count < RADIX*RADIX - 1)
  _(writes &hi, &lo, &count)
  // Invariants and gluing in post state
  _(ensures count == (hi*RADIX) + lo)
  _(ensures hi < RADIX && lo < RADIX)    
{
  _(ghost count = count + 1)
  if(lo < RADIX-1)
    lo++;
  else {
    lo = 0;
    hi++;
  }
}	

/* Using wrapped structures 

typedef struct counter {
  _(ghost \natural count)
  unsigned int lo;
  unsigned int hi;
  _(invariant lo < RADIX && hi < RADIX)
  _(invariant hi*RADIX + lo == count)
} counter;

void init(counter *p)
_(writes \span(p))
_(ensures \wrapped(p))
{
  _(ghost p->count = 0)
  p->lo = 0;
  p->hi = 0;
  _(wrap p);
}

void inc(counter *p)
_(requires \wrapped(p))
_(requires p->count < 255*RADIX+255)
_(writes p)
_(ensures \wrapped(p))
{
  _(unwrap p)
  _(ghost p->count = p->count + 1)
  if(p->lo < RADIX-1)
    p->lo++;
  else {
    p->lo = 0;
    p->hi++;
  }
  _(wrap p)
}	

*/