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    }