Jass - Documentation

Buffer Example

1 Buffer Example

package jass.examples;

public class Buffer implements Cloneable {

  protected int in,out;
  protected Object[] buf;

  public Buffer() {
    buf = new Object[0];
  }

  public Buffer (int anzahl) {
    /** require anzahl > 0; **/
    buf = new Object[anzahl];
    /** ensure buf.length == anzahl; **/
  }

  public boolean empty() {
    return in - out == 0;
    /** ensure changeonly{}; **/
  }

  public boolean full() {
    return in - out == buf.length;
    /** ensure changeonly{}; **/    
  }

  public void add(Object o) {
    /** require [valid_object] o != null; [buffer_not_full] !full(); **/
    buf[in % buf.length] = o;
    in++;
    /** ensure changeonly{in,buf}; Old.in == in - 1; **/
  }

  public Object remove() {
    /** require [buffer_not_empty] !empty(); **/
    Object o = buf[out % buf.length];
    out++;
    return o;
    /** ensure changeonly{out}; [valid_object] Result != null; **/
  } 

  public boolean contains(Object o) {
    /** require o != null; **/
    boolean found = false;
    for (int i = 0; i < buf.length; i++) 
      /** invariant 0 <= i && i <= buf.length; **/
      /** variant buf.length - i **/
      if (buf[i].equals(o)) 
        found = true;
    return found;
    /** ensure changeonly{}; **/    
  }   

  protected Object clone() {
    /* Use the Objects clone method. This is enough cause only in and out 
       are refered with Old expressions. */
    Object b = null;
    try {
      b = super.clone();
    }     
    catch (CloneNotSupportedException e){;}
    return b;
  }

  /** invariant [range] 0 <= in - out && in - out <= buf.length; 
        [valid_content] buf.length == 0 || 
	   (forall i : {out%buf.length .. in%buf.length-1} # buf[i] != null);
   **/
}