militarytime.java

Java程序设计(美) David D. Riley著 机械工业出版社 书籍配套 代码

// (Figure 8.11)

/** Class Invariant:
 *		0 <= hour <= 23
 *		and   0 <= minute <= 59
 *		and   0 <= second <= 59  */
public class MilitaryTime  {	
	protected  int  hour, minute, second;

	/** post:	hour == 1  and  minute == 0  and  second == 0  */
	public  MilitaryTime()   {
		hour = 1;
		minute = 0;
		second = 0;
	} 

	/** post:	hour == 12  and  minute == 0  and  second == 0  */
	public  void  setToNoon()   { 
		hour = 12;
		minute = 0;
		second = 0;
	}

	/** post:	(hour@pre < 23  implies  hour == hour@pre + 1)
	 *			and  (hour@pre == 23  implies  hour == 0)  
	 */
	public  void  advance1Hour()   {
		if (hour < 23)
			hour++;
		else  
			hour = 0;
	}

	/** post:	(minute@pre < 59  implies  minute == minute@pre + 1)
	 *			and  (minute@pre == 59  implies  
	 *						(minute == 0  and  hour advanced by 1)) 
	 */
	public  void  advance1Minute()   {
		if (minute < 59)
			minute++;
		else   {
			minute = 0;
			advance1Hour();
		}
	}
 

	/** post:	(second@pre < 59  implies  second == second@pre + 1)
	 * 			and  (second@pre == 59  implies  
	 *						(second == 0  and  minute advanced by 1))  
	 */
	public  void  advance1Second()   {
			if (second < 59)
			second++;
		else   {
			second = 0;
			advance1Minute();
		}
	}
	/** post:	result == hour  */
	public  int  hours()   {
		return hour;
	}
	/** post:	result == minute  */
	public  int  minutes()   {
		return minute;
	}
	/** post:	result == second  */
	public  int  seconds()   {
		return second;
	}
}