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    }