org.jSyncManager.SJS.Adapters.SMTPServer.contracts
Class StateContract

java.lang.Object
  net.sourceforge.c4j.ContractBase<AbstractSMTPServer.State>
      org.jSyncManager.SJS.Adapters.SMTPServer.contracts.StateContract

public class StateContract
extends net.sourceforge.c4j.ContractBase<AbstractSMTPServer.State>

This class lists the contracts and invariants for the SMTPCommand abstract class

Version:

1.0

Author:

Matt Campbell

See Also:

AbstractSMTPServer.SmtpCommand

Field Summary

Fields inherited from class net.sourceforge.c4j.ContractBase

m_target

Constructor Summary

StateContract(AbstractSMTPServer.State t)
A general constructor that sets the instance variable
This is of the form required by C4J

Method Summary

void	classInvariant() The invariant for this class.
void	post_clearBits(long mask) These conditions must be true at the conclusion of running clearBits Method
void	post_getState() These conditions must be true at the conclusion of running getState Method
void	pre_areBitsSet(long mask) These conditions must be true before running the areBitsSet method
void	pre_clearBits(long mask) These conditions must be true before running the clearBits method
void	pre_insertBits(long mask) These conditions must be true before running the insertBits method
void	pre_setState(long s) These conditions must be true before running the areBitsSet method

Methods inherited from class net.sourceforge.c4j.ContractBase

addLogger, classInvariantCheck, getPreconditionValue, getReturnValue, getTargetField, 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

StateContract

public StateContract(AbstractSMTPServer.State t)

A general constructor that sets the instance variable
This is of the form required by C4J

Parameters:

t - the reference to the base class

Method Detail

classInvariant

public void classInvariant()

The invariant for this class. Each of these conditions must be satisfied before and after each method call

pre_areBitsSet

public void pre_areBitsSet(long mask)

These conditions must be true before running the areBitsSet method

Parameters:

mask - The parameter to the method

See Also:

AbstractSMTPServer.State.areBitsSet(long)

pre_setState

public void pre_setState(long s)

These conditions must be true before running the areBitsSet method

Parameters:

s - The parameter to the method

See Also:

AbstractSMTPServer.State.setState(long)

post_getState

public void post_getState()

These conditions must be true at the conclusion of running getState Method

See Also:

AbstractSMTPServer.State.setState(long)

pre_insertBits

public void pre_insertBits(long mask)

These conditions must be true before running the insertBits method

Parameters:

mask - The parameter to the method

See Also:

AbstractSMTPServer.State.insertBits(long)

pre_clearBits

public void pre_clearBits(long mask)

These conditions must be true before running the clearBits method

Parameters:

mask - The parameter to the method

See Also:

AbstractSMTPServer.State.clearBits(long)

post_clearBits

public void post_clearBits(long mask)

These conditions must be true at the conclusion of running clearBits Method

Parameters:

mask - The parameter to the method

See Also:

AbstractSMTPServer.State.clearBits(long)