/** * A container that can hold at most one String. Thus, a String can only be * added if the box is empty. * * @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 contents * @ensures #contents is empty ==> item in contents
* #contents is not empty ==> contents = #contents */ public void insert(String item); /** * Removes 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 |contents| > 0 * @alters contents * @ensures removeAny not in box
* removeAny union box = #box * @return a String from the box */ public String removeAny(); }