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 }