    001    /* Copyright 2000, 2001, Compaq Computer Corporation */
    002
    003    package escjava.prover;
    004
    005    import java.io.*;
    006
    007    /**
    008     * The single <code>SNil</code> instance represents the empty list of
    009     * <code>SExp</code>s.
    010     */
    011
    012    final class SNil extends SList
    013    {
    014        /**
    015         * The single instance of this class, or <code>null</code> if it
    016         * has not yet been allocated.
    017         */
    018        //@ spec_public
    019        private static SNil single = null;
    020
    021        /**
    022         * Instance creation is private so we can ensure that at most one
    023         * instance of this class is ever created.
    024         */
    025        //@ private normal_behavior
    026        //@   requires single == null;
    027        //@   modifies single;
    028        //@   ensures single != null;
    029        private SNil() {
    030            javafe.util.Assert.notFalse(single == null);
    031            single = this;
    032        }
    033
    034        /**
    035         * @return the single SNil instance.
    036         */
    037        //@ public normal_behavior
    038        //@   modifies single;
    039        //@   ensures \result != null;
    040        //@ also
    041        //@ private normal_behavior
    042        //@   requires single == null;
    043        //@   modifies single;
    044        //@   ensures single != null;
    045        //@ also
    046        //@ private normal_behavior
    047        //@   requires single != null;
    048        //@   modifies \nothing;
    049        //@   ensures \result == single;
    050        public static /*@ non_null @*/ SNil getNil() {
    051            if (single != null) {
    052                return single;
    053            } else {
    054                single = new SNil();
    055                return single;
    056            }
    057        }
    058
    059        /**
    060         * @return true if the parameter is also the single instance of
    061         * SNil.
    062         */
    063        //@ also
    064        //@ private normal_behavior
    065        //@   ensures \result <==> (o == this);
    066        public /*@ pure @*/ boolean equals(Object o) {
    067            return o == this;
    068        }
    069
    070        /**
    071         * @return a flag indicating if we are we an empty list, which is
    072         * always <code>true</code> since we are the nil instance.
    073         */
    074        //@ also
    075        //@ public normal_behavior
    076        //@   ensures \result;
    077        public /*@ pure @*/ boolean isEmpty() {
    078            return true;
    079        }
    080
    081        /**
    082         * @return our length, which is zero since we are the nil
    083         * instance.
    084         */
    085        //@ also
    086        //@ public normal_behavior
    087        //@   ensures \result == 0;
    088        public /*@ pure @*/ int length() { return 0; }
    089    }