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    }