001package myhw3.data;
002
003/**
004 * <p>Public view of an inventory record.</p>
005 *
006 * <p>Records are mutable, but cannot be changed outside the package.</p>
007 *
008 * <p>This interface should not be implemented outside the package.</p>
009 *
010 * <p><code>equals</code> and <code>hashCode</code> delegate to the
011 * underlying Video object.</p>
012 * @see Data
013 */
014public interface Record {
015        /**
016         * Returns the video.
017         * <p><b>Invariant:</b> <code>video() != null</code>.</p>
018         */
019        public Video video();
020        /**
021         * Returns the number of copies of the video that are in the inventory.
022         * <p><b>Invariant:</b> <code>numOwned() > 0</code>.</p>
023         */
024        public int numOwned();
025        /**
026         * Returns the number of copies of the video that are currently checked out.
027         * <p><b>Invariant:</b> <code>numOut() <= numOwned()</code>.</p>
028         */
029        public int numOut();
030        /**
031         * Returns the total number of times this video has ever been checked out.
032         * <p><b>Invariant:</b> <code>numRentals() >= numOut()</code>.</p>
033         */
034        public int numRentals();
035        /**
036         * Delegates to video.
037         * Returns false if thatObject is not a Record created by this package.
038         */
039        public boolean equals(Object thatObject);
040        /**
041         * Delegates to video.
042         */
043        public int hashCode();
044        /**
045         *  Return a string representation of the object in the following format:
046         * <code>"video [numOwned,numOut,numRentals]"</code>.
047         */
048        public String toString();
049}