Prog1Tools
Class TurtleSpecContract

java.lang.Object
  extended by net.sourceforge.c4j.ContractBase<TurtleSpec>
      extended by Prog1Tools.TurtleSpecContract

public class TurtleSpecContract
extends net.sourceforge.c4j.ContractBase<TurtleSpec>

Vertragsklasse zum Interface TurtleSpec.

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

Field Summary
 
Fields inherited from class net.sourceforge.c4j.ContractBase
m_target
 
Constructor Summary
TurtleSpecContract(TurtleSpec target)
           
 
Method Summary
 void post_forward(int distance)
           
 void post_getHeading()
           
 void post_getPositionX()
           
 void post_getPositionY()
           
 void post_hideTurtle()
           
 void post_isVisibleTurtle()
           
 void post_setHeading(int heading)
           
 void post_setTurtle(int xPos, int yPos)
           
 void post_showTurtle()
           
 void pre_forward(int distance)
           
 void pre_getHeading()
           
 void pre_getPositionX()
           
 void pre_getPositionY()
           
 void pre_hideTurtle()
           
 void pre_isVisibleTurtle()
           
 void pre_setHeading(int heading)
           
 void pre_setTurtle(int xPos, int yPos)
           
 void pre_showTurtle()
           
 
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

TurtleSpecContract

public TurtleSpecContract(TurtleSpec target)
Method Detail

pre_setTurtle

public void pre_setTurtle(int xPos,
                          int yPos)

post_setTurtle

public void post_setTurtle(int xPos,
                           int yPos)

pre_setHeading

public void pre_setHeading(int heading)

post_setHeading

public void post_setHeading(int heading)

pre_forward

public void pre_forward(int distance)

post_forward

public void post_forward(int distance)

pre_getPositionX

public void pre_getPositionX()

post_getPositionX

public void post_getPositionX()

pre_getPositionY

public void pre_getPositionY()

post_getPositionY

public void post_getPositionY()

pre_getHeading

public void pre_getHeading()

post_getHeading

public void post_getHeading()

pre_showTurtle

public void pre_showTurtle()

post_showTurtle

public void post_showTurtle()

pre_hideTurtle

public void pre_hideTurtle()

post_hideTurtle

public void post_hideTurtle()

pre_isVisibleTurtle

public void pre_isVisibleTurtle()

post_isVisibleTurtle

public void post_isVisibleTurtle()