class Counter {

  ghost var val: int ;

  predicate Valid()
    reads this ;
  {
  }

  // The constructor
  constructor init()
    ensures val == 0;
    ensures Valid();
    modifies this;
  {
  }

  method Inc()
    modifies this;
    requires Valid();
    ensures Valid();
    ensures val == old(val) + 1;
  {
  }

  method Dec()
    modifies this;
    requires Valid();
    ensures Valid();
    ensures val == old(val) - 1;
  {
  }

  method Clear()
    modifies this;
    requires Valid();
    ensures Valid();
    ensures val == 0;
  {
  }

  method Get() returns (n: int)
    requires Valid();
    ensures Valid();
    ensures n == val;
  {
  }

  method Set(n: int)
    modifies this;
    requires Valid();
    ensures Valid();
    ensures n == val;
  {
  }
}