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 }