borderedoval.java

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

import java.awt.*;
/**		Class Invariant
 *			getwidth() == getHeight()  
 *			and  innerOval.getWidth() == getWidth() - 4
 *			and  innerOval.getHeight() == getHeight() - 4
 *			and  innerOval.getX() == innerOval.getY() == 2
 *			and  innerOval is added to this 
 */
public class BorderedOval extends Oval {
	private Oval  innerOval;

	/**		pre:	d > 4
	 *		post:	getX() == x  and  getY() == y  
	 *				and  getWidth() == d  and  getHeight() == d  
	 *				and  getBackground() == borderColor() == Color.black 
	 */ 
	public BorderedOval( int x, int y, int d)   {
		super(x, y, d, d);
		innerOval = new Oval(2, 2, d-4, d-4);
		add( innerOval );
	}
	
	/**	post:	getBackground() == c */
	public  void  setBorderColor( Color c )   {
		setBackground( c );
	}
	
	/**	post:	innerOval.getBackground() == c */
	public  void  setInnerColor( Color c )   {
		innerOval.setBackground( c );
	}
	
	/**	post:	result == innerOval.getBackground()  */
	public  Color  getInnerColor() {
		return innerOval.getBackground();
	}
	
	/**	post:	result == getBackground()  */
	public  Color  getBorderColor() {
		return getBackground();
	}
	
	/**	post:	getWidth() == d  and  getHeight() == d  */
	public void  setSize( int d )   {
		setSize(d, d);
	}
		
	/**	pre:	w > 4  and  h > 4
	 *	post:	getWidth() == w  and  getHeight() == h 
	 */
	public void  setSize( int w, int h )   {
		super.setSize( w, h );
		innerOval.setSize( w-4, h-4 );
	}
}