// openjml --esc T_Polygon.java
public interface T_Polygon {

  /** Number of sides to the polygon */
  //@ ensures \result >= 3;
  //@ spec_pure helper
  public int sides();

}   

class Square implements T_Polygon {

  /** Length of one side of the Square */
  public int side;

  //@ public invariant side >= 0;

  //@ requires 0 <= side < 1000;
  //@ ensures this.side == side;
  public Square(int side) {
    this.side = side;
  }

  //@ also
  //@   ensures \result == 4;
  //@ spec_pure helper
  public int sides() {
    return 4;
  }

}