001package myhw2.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         *  Return a string representation of the object in the following format:
037         * <code>"video [numOwned,numOut,numRentals]"</code>.
038         */
039        public String toString();
040}