001 /* Copyright 2000, 2001, Compaq Computer Corporation */ 002 003 package javafe.genericfile; 004 005 006 import java.io.IOException; 007 import java.io.InputStream; 008 009 010 /** 011 * A GenericFile is a least-common-denominator representation of a 012 * read-only file (or directory).<p> 013 * 014 * Note: The existence of GenericFile does not imply the actual 015 * existence of an underlying file.<p> 016 * 017 * 018 * Currently, GenericFile's can be created from normal files 019 * (java.io.File) and zipfile entries (java.util.zip.ZipEntry).<p> 020 * 021 * Additional operations on GenericFiles will be added later as needed.<p> 022 */ 023 024 public interface GenericFile { 025 026 /*************************************************** 027 * * 028 * Operations on GenericFiles: * 029 * * 030 **************************************************/ 031 032 /** 033 * Return a name that uniquely identifies us to the user. 034 * 035 * Warning: the result may not be a conventional filename or use 036 * the system separators. 037 */ 038 //@ ensures \result != null; 039 public abstract String getHumanName(); 040 041 042 /** 043 * Return a String that canonically represents the identity of our 044 * underlying file. 045 * 046 * This function must be defined such that if two GenericFiles 047 * return non-null canonical ID's then the IDs are the same 048 * (modulo .equals) => the GenericFiles represent the same 049 * underlying file. Ideally, under normal circumstances, the => 050 * is actually a <=>. 051 * 052 * This function should only return null in exceptional 053 * cases, such as when an I/O error in the underlying storage media 054 * prevents construction of a canonical ID. 055 * 056 * Convention: Canonical IDs start with <X> where X is the 057 * fully-qualified name of the class that mediates I/O to the 058 * underlying file. E.g., java.io.File for a normal disk file. 059 */ 060 public abstract String getCanonicalID(); 061 062 063 /** 064 * Return our local name, the name that distinguishes us 065 * within the directory that contains us. 066 * 067 * E.g., "/a/b/c" has local name "c", "/e/r/" has local name "r", and 068 * "/" has local name "". (assuming "/" is the separator char) 069 */ 070 //@ ensures \result != null; 071 public abstract String getLocalName(); 072 073 074 /** 075 * Do we represent a directory? 076 */ 077 public abstract boolean isDirectory(); 078 079 080 /** 081 * Open the file we represent as an InputStream.<p> 082 * 083 * java.io.IOEXception may be thrown for many reasons, including no 084 * such file and read permission denied.<p> 085 */ 086 //@ modifies objectState; 087 //@ ensures \fresh(\result); 088 //@ ensures \result != null; 089 //@ ensures \result.isOpen; 090 public abstract InputStream getInputStream() throws IOException; 091 092 093 /** 094 * Returns the time that the file represented by us was last 095 * modified.<p> 096 * 097 * The return value is system dependent and should only be used to 098 * compare with other values returned by last modified. It should 099 * not be interpreted as an absolute time.<p> 100 * 101 * If a last-modified time is not available (e.g., underlying file 102 * doesn't exist, no time specified in a zipentry, etc.), then 0L 103 * is returned.<p> 104 */ 105 public abstract long lastModified(); 106 107 108 /** 109 * Attempt to return a GenericFile that describes the file in the 110 * same "directory" as us that has the local name <code>n</code>. <p> 111 * 112 * No attempt is made to verify whether or not that file exists.<p> 113 * 114 * In cases where the notion of "containing directory" makes no 115 * sense (e.g., streams or root directories), null is returned. 116 */ 117 public abstract GenericFile getSibling(/*@ non_null @*/ String n); 118 }