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

// Demonstrating refinement checking for C implementations

unsigned count;
unsigned lo, hi;

void init()
  _(writes &count, &lo, &hi)
  _(ensures (hi * 256) + lo == count) // Gluing
  _(ensures hi <= 255 && lo <= 255) // State invariant
{
  count = 0;
  lo = 0;
  hi = 0;
}

void inc()
  // Precondition for inc
  _(requires (hi < 255 || lo < 255))
  // State invariant and Gluing relation
  _(requires hi <= 255 && lo <= 255)
  _(requires (hi * 256) + lo == count)
  _(writes &count, &lo, &hi)
  // State invariant and Gluing relation in post state
  _(ensures hi <= 255 && lo <= 255)
  _(ensures (hi * 256) + lo == count)
{
  count = count + 1;
  if (lo < 255)
    lo = lo + 1;
  else {
    lo = 0;
    hi = hi + 1;
  }
}