/** A bad imlementation of stacks.  What's wrong with it? */       //   1
public class BadStack {                                            //   2
                                                                   //   3
    public static final int MAX_SIZE = 100;                        //   4
    Object[] elems;                                                //   5
    public int pushed;                                             //   6
                                                                   //   7
    //@ public invariant 0 <= pushed && pushed < MAX_SIZE;         //   8
                                                                   //   9
    /** Initialize this to be an empty BadStack. */                //  10
    public BadStack() {                                            //  11
        elems = new Object[MAX_SIZE];                              //  12
        pushed = 0;                                                //  13
    }                                                              //  14
                                                                   //  15
    /** Push the given element on this stack. */                   //  16
    //@ requires pushed < MAX_SIZE;                                //  17
    public void push(Object x) {                                   //  18
        if (pushed < MAX_SIZE) {                                   //  19
            elems[pushed] = x;                                     //  20
            pushed += 1;                                           //  21
        } else {                                                   //  22
            throw new IllegalStateException("Too many elements!"); //  23
        }                                                          //  24
    }                                                              //  25
                                                                   //  26
    /** Pop this stack. */                                         //  27
    //@ requires pushed > 0;                                       //  28
    public void pop() {                                            //  29
        if (pushed > 0) {                                          //  30
            elems[pushed] = null;                                  //  31
            pushed -= 1;                                           //  32
        } else {                                                   //  33
            throw new IllegalStateException("Empty Stack!");       //  34
        }                                                          //  35
    }                                                              //  36
                                                                   //  37
    /** Return the top element of this stack. */                   //  38
    //@ requires pushed > 0;                                       //  39
    public Object top() {                                          //  40
        if (pushed > 0) {                                          //  41
            return elems[pushed-1];                                //  42
        } else {                                                   //  43
            throw new IllegalStateException("Empty Stack!");       //  44
        }                                                          //  45
    }                                                              //  46
                                                                   //  47
    /** Is this stack empty? */                                    //  48
    boolean isEmpty() {                                            //  49
        return pushed == 0;                                        //  50
    }                                                              //  51
                                                                   //  52
    /** Is this stack not empty? */                                //  53
    boolean isNotEmpty() {                                         //  54
        return !isEmpty();                                         //  55
    }                                                              //  56
                                                                   //  57
    /** What is the size of this stack? */                         //  58
    int size() {                                                   //  59
        return pushed;                                             //  60
    }                                                              //  61
                                                                   //  62
    /** How many more elements can be pushed on this stack? */     //  63
    int spaceRemaining() {                                         //  64
        return MAX_SIZE - pushed;                                  //  65
    }                                                              //  66
                                                                   //  67
    /** Return the maximum size of this stack? */                  //  68
    int maximumSize() {                                            //  69
        return MAX_SIZE;                                           //  70
    }                                                              //  71
                                                                   //  72
    /** Is this stack full? */                                     //  73
    boolean isFull() {                                             //  74
        return pushed == MAX_SIZE - 1;                             //  75
    }                                                              //  76
                                                                   //  77
    /** Is this stack not full? */                                 //  78
    boolean isNotFull() {                                          //  79
        return !isFull();                                          //  80
    }                                                              //  81
                                                                   //  82
    private int x = 0;                                             //  83
    private int y = 0;                                             //  84
                                                                   //  85
    /** Return the x coordinate of this stack. */                  //  86
    public int getX() {                                            //  87
        return x;                                                  //  88
    }                                                              //  89
                                                                   //  90
    /** Return the y coordinate of this stack. */                  //  91
    public int getY() {                                            //  92
        return y;                                                  //  93
    }                                                              //  94
                                                                   //  95
    /** Set the x coordinate of this stack. */                     //  96
    public void setX(int xv) {                                     //  97
        x = xv;                                                    //  98
    }                                                              //  99
                                                                   // 100
    /** Return the y coordinate of this stack. */                  // 101
    public void setY(int yv) {                                     // 102
        y = yv;                                                    // 103
    }                                                              // 104
                                                                   // 105
}                                                                  // 106