interface Array[type T]
{
  requires
  {
    def count() : uint;
    def _subscript(uint n) : T& {
      pre(n < count());
      inner;
    }
  }
}

interface Stack[type T]
{
  inherits
  {
    Array[T];
  }
  requires
  {
    def push(T x) {
      uint old = count();
      inner;
      post(count() == old + 1);
    }
    def pop() {
      uint old = count();
      pre(!is_empty());
      inner;
      post(count() == old - 1);
    }
    def top() : T& {
      pre(!is_empty());
      inner;
    }
  }
  extension
  {
    def is_empty() : bool {
      return count() == 0;
    }
    def clear() {
      while (!is_empty()) {
        pop();
      };
    }
    def dup() {
      push(top());
    }
    def reverse() {
      if (count() < 1) return;
      int max = count() - 1;
      uint n = count() / 2;
      for_each (i, range(0,n-1)) {     
        swap_elements(i, max - i);
      };
    }
    def swap_elements(uint i, uint j) {
      T tmp = _subscript(i);
      _subscript(i) = _subscript(j);
      _subscript(j) = tmp;
    }
  }
}

The principal reason for allowing required function redefintions is so that preconditions and postconditions can be verified (using the pre / post macros). The innert keyword is equivalent to writing: result = super->method_name(method_args) if the function is non-void or simply super->method_name(method_args) otherwise.

I hope this makes more sense than the older syntax and explanations. Any feedback would be appreciated as usual.

Acknowledgements