package Examples;

import java.util.*;

/**
 * A simple class implementing a sorted list. Internally it also maintains
 * a pointer to the greatest element in the list (if it is not
 * empty).
 * 
 * <p>There are some faults in the method {@link #insert insert}.
 */
public class SimpleSortedList {

    private LinkedList<Comparable> s;
    private Comparable max;

    /**
     * This constructs an empty list.
     */
    public SimpleSortedList() {
        s = new LinkedList<Comparable>();
    }

    /**
     * This class invariant only specifies that the max-pointer points
     * to some element in the list, if it is not empty. 
     */
    private boolean classinv() {
        return s.isEmpty() || s.contains(max);
    }

    /**
     * This inserts a new element into the list.
     */
    public void insert(Comparable x) {
        int i = 0;
        for (Comparable y : s) {
            if (y.compareTo(x) > 0) {
                break;
            }
            i++;
        }
        s.add(i, x);

        // deliberate error:
        if (max == null || x.compareTo(max) < 0) {
            max = x;
        }
    }

    /**
     * Return and remove the greatest element from the list, if it is
     * not empty.
     */
    public Comparable get() {
        Comparable x = max;
        s.remove(max);
        if (s.isEmpty()) {
            max = null;
        } else {
            max = s.getLast();
        }
        return x;
    }

    /**
     * A specification for {@link #get get}.
     */
    public Comparable get_spec() {

        assert !s.isEmpty() : "PRE";
        Comparable ret = get();
        assert s.isEmpty() || ret.compareTo(s.getLast()) >= 0 : "POST";
        return ret;
    }

    static public void main(String[] args) {
        // Calling T2 from here; see how it finds the mistake:
        Sequenic.T2.Main.main(SimpleSortedList.class.getName());
    }
}