    001    /* Copyright 2000, 2001, Compaq Computer Corporation */
    002
    003    package escjava.prover;
    004
    005
    006    import java.io.*;
    007
    008
    009    /**
    010     ** A <code>SPair</code> is a pair of a <code>SExp</code> and a
    011     ** <code>SList</code>; together with the <code>SNil</code> class, it is
    012     ** used to implement lists of <code>SExp</code>s. <p>
    013     **
    014     ** Considered as <code>SList</code>s, <code>SPair</code>s always
    015     ** represent non-empty lists.<p>
    016     **/
    017
    018    /*package*/ class SPair extends SList {
    019
    020        /***************************************************
    021         *                                                 *
    022         * Instance variables:                             *
    023         *                                                 *
    024         ***************************************************/
    025
    026        /**
    027         ** The head of our list; this field should not be modified by
    028         ** clients and should be non-null.
    029         **/
    030        //@ invariant head != null;
    031        public SExp head;
    032
    033        /**
    034         ** The tail of our list; this field should not be modified by
    035         ** clients and should be non-null.
    036         **/
    037        //@ invariant tail != null;
    038        public SList tail;
    039
    040
    041        /***************************************************
    042         *                                                 *
    043         * Creation:                                       *
    044         *                                                 *
    045         ***************************************************/
    046
    047        /**
    048         ** Return a new list with given head and tail. <p>
    049         **
    050         ** Both must be non-null.<p>
    051         **/
    052        //@ requires head != null && tail != null;
    053        public SPair(SExp head, SList tail) {
    054            this.head = head;
    055            this.tail = tail;
    056        }
    057
    058
    059        /***************************************************
    060         *                                                 *
    061         * List Accessors:                                 *
    062         *                                                 *
    063         ***************************************************/
    064
    065        /**
    066         ** Are we an empty list?
    067         **/
    068        public /*@ pure @*/ boolean isEmpty() {
    069            return false;
    070        }
    071
    072        /**
    073         ** If we represent a non-empty list, return it as a
    074         ** <code>SPair</code>; otherwise, throw <code>SExpTypeError</code>.
    075         **/
    076        /*package*/ /*@ non_null @*/ SPair getPair() {
    077            return this;
    078        }
    079
    080        /**
    081         ** Return our length
    082         **/
    083        public int length() {
    084            return 1+tail.length();
    085        }
    086
    087        /**
    088         ** Return true if the heads are equal and the tails are equal.
    089         **/
    090        public boolean equals(Object o) {
    091            if (!(o instanceof SPair)) return false;
    092            SPair a = (SPair)o;
    093            return this.head.equals(a.head) && this.tail.equals(a.tail);
    094        }
    095
    096    }