    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    }