package genericity;

/**
 * @mathmodel contents : set of Strings
 * @initially contents is empty
 * @constraint |contents| <= 1
 */
public interface BoxOfStrings {

	/**
	 * Reports the size of the box. Since the number of elements in the box is
	 * at most 1, the method returns either 0 or 1.
	 * 
	 * @ensures size = |contents|
	 * @return the number of Strings in the box
	 */
	public int size();

	/**
	 * Tests whether or not the box contains the particular String.
	 * 
	 * @param target
	 *            a String to be found in the box
	 * @ensures contains <==> target in contents
	 * @return true if and only if the box contains the target
	 */
	public boolean contains(String target);

	/**
	 * Adds a String to the box. This method is only effective if the box is
	 * empty. Otherwise, the box remains unchanged.
	 * 
	 * @param item
	 *            a String to be added to the box
	 * @alters this
	 * @ensures #contents is empty ==> item in contents <br />
	 *          #contents is not empty ==> contents = #contents
	 */
	public void insert(String item);

	/**
	 * Remove an arbitrary String from the box. Since the box can contain at
	 * most one String, there is no ambiguity about which String is
	 * removed.
	 * 
	 * @requires |box| > 0
	 * @alters box
	 * @ensures removeAny not in box <br />
	 *          removeAny union box = #box
	 * @return a String from the box
	 */
	public String removeAny();

}