Prog1Tools
Class TextScreenCellSpecContract

java.lang.Object
  extended by net.sourceforge.c4j.ContractBase<TextScreenCellSpec>
      extended by Prog1Tools.TextScreenCellSpecContract

public class TextScreenCellSpecContract
extends net.sourceforge.c4j.ContractBase<TextScreenCellSpec>

Vertragsklasse der Spezifikation einer Bildschirmzelle eines TextScreens.

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

Field Summary
 
Fields inherited from class net.sourceforge.c4j.ContractBase
m_target
 
Constructor Summary
TextScreenCellSpecContract(TextScreenCellSpec target)
           
 
Method Summary
 void classInvariant()
           
 void post_getBackgroundColor()
           
 void post_getChar()
           
 void post_getColumn()
           
 void post_getForegroundColor()
           
 void post_getRow()
           
 void post_setBackgroundColor(java.awt.Color color)
           
 void post_setChar(char character)
           
 void post_setForegroundColor(java.awt.Color color)
           
 void pre_getBackgroundColor()
           
 void pre_getChar()
           
 void pre_getColumn()
           
 void pre_getForegroundColor()
           
 void pre_getRow()
           
 void pre_setBackgroundColor(java.awt.Color color)
           
 void pre_setChar(char character)
           
 void pre_setForegroundColor(java.awt.Color color)
           
 
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

TextScreenCellSpecContract

public TextScreenCellSpecContract(TextScreenCellSpec target)
Method Detail

classInvariant

public void classInvariant()

pre_getRow

public void pre_getRow()

post_getRow

public void post_getRow()

pre_getColumn

public void pre_getColumn()

post_getColumn

public void post_getColumn()

pre_getChar

public void pre_getChar()

post_getChar

public void post_getChar()

pre_setChar

public void pre_setChar(char character)

post_setChar

public void post_setChar(char character)

pre_setForegroundColor

public void pre_setForegroundColor(java.awt.Color color)

post_setForegroundColor

public void post_setForegroundColor(java.awt.Color color)

pre_setBackgroundColor

public void pre_setBackgroundColor(java.awt.Color color)

post_setBackgroundColor

public void post_setBackgroundColor(java.awt.Color color)

pre_getForegroundColor

public void pre_getForegroundColor()

post_getForegroundColor

public void post_getForegroundColor()

pre_getBackgroundColor

public void pre_getBackgroundColor()

post_getBackgroundColor

public void post_getBackgroundColor()