timewithmillisec.java

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

// (Figure 8.12)

public class TimeWithMillisec extends MilitaryTime {	
	protected  int  millisec;

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

/** post:	(millisec@pre < 999  implies  millisec == millisec@pre + 1)
	 *			and  (millisec@pre == 59  implies  
	 *						(millisec == 0  and second advanced by 1)) 
	 */
	public  void  advance1Millisec()   {
		if (millisec < 59)
			millisec ++;
		else   {
			millisec = 0;
			advance1Second();
		}
	}
}