/**
 * A Pencil has a (positive) length and color.  A pencil can change its color.
 * It can also decrease its length as a result of being sharpened.
 * 
 * @mathmodel c : Colors, where c is the color of the pencil <br />
 *            s : int, where s is the length of the pencil
 * @initially Pencil(Colors color, int length) <br />
 *     ensures c = color and
 *             length > 0 ==> s = length
 * @constraint s > 0
 */
public interface Pencil {

	/**
	 * Returns a human-readable representation of the pencil.
	 * Both the color and the length are included.
	 * 
	 * @return String describing c and s 
	 */
	public String toString();
	
	/**
	 * Sets the pencil color.
	 * 
	 * @param newColor is any valid color
	 * @alters c
	 * @ensures c = newColor
	 */
	public void setColor(Colors newColor);
	
	/**
	 * Sharpens the pencil by grinding it down.  Sharpening can never
	 * increase the length of the pencil.  The requested length is
	 * removed, if possible.
	 * 
	 * @param remove amount by which pencil will be shortened
	 * @requires remove >= 0
	 * @alters s
	 * @ensures remove < #s ==> s + remove = #s and <br />
	 *          s <= #s
	 */
	public void sharpen(int remove);
}