Prog1Tools
Class GraphicScreenSpecContract

java.lang.Object
  extended by net.sourceforge.c4j.ContractBase<GraphicScreenSpec>
      extended by Prog1Tools.GraphicScreenSpecContract

public class GraphicScreenSpecContract
extends net.sourceforge.c4j.ContractBase<GraphicScreenSpec>

Vertragsklasse der Spezifikation eines grafikfaehigen Farbbildschirms.

Version:
1.1
Author:
hagen.buchwald@kit.edu

Field Summary
 
Fields inherited from class net.sourceforge.c4j.ContractBase
m_target
 
Constructor Summary
GraphicScreenSpecContract(GraphicScreenSpec target)
           
 
Method Summary
 void post_clearScreen()
           
 void post_drawArc(int x, int y, int width, int height, int startAngle, int arcAngle, boolean isFilled)
           
 void post_drawCircle(int x, int y, int radius, boolean isFilled)
           
 void post_drawLine(int x1, int y1, int x2, int y2)
           
 void post_drawOrigin()
           
 void post_drawOval(int x, int y, int width, int height, boolean isFilled)
           
 void post_drawPolygon(int[] xPoints, int[] yPoints, int nPoints, boolean isFilled)
           
 void post_drawPolyline(int[] xPoints, int[] yPoints, int nPoints)
           
 void post_drawRectangle(int x, int y, int width, int height, boolean isFilled)
           
 void post_drawRectangle3D(int x, int y, int width, int height, boolean isFilled, boolean isRaised)
           
 void post_drawRectangleRounded(int x, int y, int width, int height, int arcWidth, int arcHeight, boolean isFilled)
           
 void post_drawText(int x, int y, java.lang.String text)
           
 void post_getColor()
           
 void post_getItem(int index)
           
 void post_getMaxNumberOfItems()
           
 void post_getMaxX()
           
 void post_getMaxY()
           
 void post_getNumberOfItems()
           
 void post_getOrigin()
           
 void post_repaint()
           
 void post_setColor(java.awt.Color color)
           
 void post_setOrigin(int x, int y)
           
 void pre_clearScreen()
           
 void pre_drawArc(int x, int y, int width, int height, int startAngle, int arcAngle, boolean isFilled)
           
 void pre_drawCircle(int x, int y, int radius, boolean isFilled)
           
 void pre_drawLine(int x1, int y1, int x2, int y2)
           
 void pre_drawOrigin()
           
 void pre_drawOval(int x, int y, int width, int height, boolean isFilled)
           
 void pre_drawPolygon(int[] xPoints, int[] yPoints, int nPoints, boolean isFilled)
           
 void pre_drawPolyline(int[] xPoints, int[] yPoints, int nPoints)
           
 void pre_drawRectangle(int x, int y, int width, int height, boolean isFilled)
           
 void pre_drawRectangle3D(int x, int y, int width, int height, boolean isFilled, boolean isRaised)
           
 void pre_drawRectangleRounded(int x, int y, int width, int height, int arcWidth, int arcHeight, boolean isFilled)
           
 void pre_drawText(int x, int y, java.lang.String text)
           
 void pre_getColor()
           
 void pre_getItem(int index)
           
 void pre_getMaxNumberOfItems()
           
 void pre_getMaxX()
           
 void pre_getMaxY()
           
 void pre_getNumberOfItems()
           
 void pre_getOrigin()
           
 void pre_repaint()
           
 void pre_setColor(java.awt.Color color)
           
 void pre_setOrigin(int x, int y)
           
 
Methods inherited from class net.sourceforge.c4j.ContractBase
addLogger, classInvariantCheck, getPreconditionValue, getReturnValue, getTargetField, implies, popPreconditionValuesMap, popReturnValue, postConditionCheck, preConditionCheck, pushPreconditionValuesMap, pushReturnValue, setPreconditionValue, setReturnValue
 
Methods inherited from class java.lang.Object
clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait
 

Constructor Detail

GraphicScreenSpecContract

public GraphicScreenSpecContract(GraphicScreenSpec target)
Method Detail

pre_clearScreen

public void pre_clearScreen()

post_clearScreen

public void post_clearScreen()

pre_repaint

public void pre_repaint()

post_repaint

public void post_repaint()

pre_getColor

public void pre_getColor()

post_getColor

public void post_getColor()

pre_setColor

public void pre_setColor(java.awt.Color color)

post_setColor

public void post_setColor(java.awt.Color color)

pre_setOrigin

public void pre_setOrigin(int x,
                          int y)

post_setOrigin

public void post_setOrigin(int x,
                           int y)

pre_getOrigin

public void pre_getOrigin()

post_getOrigin

public void post_getOrigin()

pre_drawOrigin

public void pre_drawOrigin()

post_drawOrigin

public void post_drawOrigin()

pre_drawLine

public void pre_drawLine(int x1,
                         int y1,
                         int x2,
                         int y2)

post_drawLine

public void post_drawLine(int x1,
                          int y1,
                          int x2,
                          int y2)

pre_drawPolyline

public void pre_drawPolyline(int[] xPoints,
                             int[] yPoints,
                             int nPoints)

post_drawPolyline

public void post_drawPolyline(int[] xPoints,
                              int[] yPoints,
                              int nPoints)

pre_drawPolygon

public void pre_drawPolygon(int[] xPoints,
                            int[] yPoints,
                            int nPoints,
                            boolean isFilled)

post_drawPolygon

public void post_drawPolygon(int[] xPoints,
                             int[] yPoints,
                             int nPoints,
                             boolean isFilled)

pre_drawText

public void pre_drawText(int x,
                         int y,
                         java.lang.String text)

post_drawText

public void post_drawText(int x,
                          int y,
                          java.lang.String text)

pre_drawCircle

public void pre_drawCircle(int x,
                           int y,
                           int radius,
                           boolean isFilled)

post_drawCircle

public void post_drawCircle(int x,
                            int y,
                            int radius,
                            boolean isFilled)

pre_drawOval

public void pre_drawOval(int x,
                         int y,
                         int width,
                         int height,
                         boolean isFilled)

post_drawOval

public void post_drawOval(int x,
                          int y,
                          int width,
                          int height,
                          boolean isFilled)

pre_drawRectangle

public void pre_drawRectangle(int x,
                              int y,
                              int width,
                              int height,
                              boolean isFilled)

post_drawRectangle

public void post_drawRectangle(int x,
                               int y,
                               int width,
                               int height,
                               boolean isFilled)

pre_drawRectangle3D

public void pre_drawRectangle3D(int x,
                                int y,
                                int width,
                                int height,
                                boolean isFilled,
                                boolean isRaised)

post_drawRectangle3D

public void post_drawRectangle3D(int x,
                                 int y,
                                 int width,
                                 int height,
                                 boolean isFilled,
                                 boolean isRaised)

pre_drawRectangleRounded

public void pre_drawRectangleRounded(int x,
                                     int y,
                                     int width,
                                     int height,
                                     int arcWidth,
                                     int arcHeight,
                                     boolean isFilled)

post_drawRectangleRounded

public void post_drawRectangleRounded(int x,
                                      int y,
                                      int width,
                                      int height,
                                      int arcWidth,
                                      int arcHeight,
                                      boolean isFilled)

pre_drawArc

public void pre_drawArc(int x,
                        int y,
                        int width,
                        int height,
                        int startAngle,
                        int arcAngle,
                        boolean isFilled)

post_drawArc

public void post_drawArc(int x,
                         int y,
                         int width,
                         int height,
                         int startAngle,
                         int arcAngle,
                         boolean isFilled)

pre_getNumberOfItems

public void pre_getNumberOfItems()

post_getNumberOfItems

public void post_getNumberOfItems()

pre_getMaxX

public void pre_getMaxX()

post_getMaxX

public void post_getMaxX()

pre_getMaxY

public void pre_getMaxY()

post_getMaxY

public void post_getMaxY()

pre_getMaxNumberOfItems

public void pre_getMaxNumberOfItems()

post_getMaxNumberOfItems

public void post_getMaxNumberOfItems()

pre_getItem

public void pre_getItem(int index)

post_getItem

public void post_getItem(int index)