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

java.lang.Object
  net.sourceforge.c4j.ContractBase<Message>
      org.jSyncManager.SJS.Adapters.SMTPServer.contracts.MessageContract

public class MessageContract
extends net.sourceforge.c4j.ContractBase<Message>

Contract for the Message Class

Version:

v1.0

Author:

Ahmad

Field Summary

Fields inherited from class net.sourceforge.c4j.ContractBase

m_target

Constructor Summary

MessageContract(Message t)
Constructor, get a reference for the Message object

Method Summary

void	classInvariant() Invariant checks.
void	post_Message(Address from, java.util.List<Address> to, java.lang.String body) Post-Message (third) constructor condition..
void	post_Message(java.util.Date sent, java.util.Date received, Address from, java.util.List<Address> to, java.lang.String body) Post-Message (second) constructor condition.
void	post_setFrom(Address from) Post-condition for setFrom.
void	post_setFrom(java.lang.String from) Post-condition for setFrom.
void	post_setReceived(java.util.Date received) Post-condition for setReceived.
void	post_setSent(java.util.Date sent) Post-condition for setSent.
void	post_setTo(java.util.List<Address> to) Post-condition for setTo method.
void	post_toString() Post-condition for toString method.
void	pre_addTo(Address address) Pre-condition for addTo method.
void	pre_appendData(java.lang.String data) Pre-condition for appendData method.
void	pre_getToIter() Pre-condition for getToIter method.
void	pre_Message() Pre-Message constructor condition.
void	pre_Message(Address from, java.util.List<Address> to, java.lang.String body) Pre-Message (third) constructor condition.
void	pre_Message(java.util.Date sent, java.util.Date received, Address from, java.util.List<Address> to, java.lang.String body) Pre-Message (second) constructor condition.
void	pre_setFrom(Address from) Pre-condition for setFrom.
void	pre_setFrom(java.lang.String from) Pre-condition for setFrom.
void	pre_setReceived(java.util.Date received) Pre-condition for setReceived.
void	pre_setSent(java.util.Date sent) Pre-condition for setSent.
void	pre_setTo(java.util.List<Address> to) Pre-condition for setTo.
void	pre_toString() Pre-condition for toString 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

MessageContract

public MessageContract(Message t)

Constructor, get a reference for the Message object

Parameters:

t - the object.

Method Detail

classInvariant

public void classInvariant()

Invariant checks.

pre_Message

public void pre_Message()

Pre-Message constructor condition.

pre_Message

public void pre_Message(java.util.Date sent,
                        java.util.Date received,
                        Address from,
                        java.util.List<Address> to,
                        java.lang.String body)

Pre-Message (second) constructor condition.

Parameters:

sent - See Message class.

received - See Message class.

from - See Message class.

to - See Message class.

body - See Message class.

post_Message

public void post_Message(java.util.Date sent,
                         java.util.Date received,
                         Address from,
                         java.util.List<Address> to,
                         java.lang.String body)

Post-Message (second) constructor condition.

Parameters:

sent - See Message class.

received - See Message class.

from - See Message class.

to - See Message class.

body - See Message class.

pre_Message

public void pre_Message(Address from,
                        java.util.List<Address> to,
                        java.lang.String body)

Pre-Message (third) constructor condition.

Parameters:

from - See Message class.

to - See Message class.

body - See Message class.

post_Message

public void post_Message(Address from,
                         java.util.List<Address> to,
                         java.lang.String body)

Post-Message (third) constructor condition..

Parameters:

from - See Message class.

to - See Message class.

body - See Message class.

pre_setFrom

public void pre_setFrom(Address from)

Pre-condition for setFrom.

Parameters:

from - See Message class.

post_setFrom

public void post_setFrom(Address from)

Post-condition for setFrom.

Parameters:

from - See Message class.

pre_setFrom

public void pre_setFrom(java.lang.String from)

Pre-condition for setFrom.

Parameters:

from - See Message class.

post_setFrom

public void post_setFrom(java.lang.String from)

Post-condition for setFrom.

Parameters:

from - See Message class.

pre_setReceived

public void pre_setReceived(java.util.Date received)

Pre-condition for setReceived.

Parameters:

received - See Message class.

post_setReceived

public void post_setReceived(java.util.Date received)

Post-condition for setReceived.

Parameters:

received - See Message class.

pre_setSent

public void pre_setSent(java.util.Date sent)

Pre-condition for setSent.

Parameters:

sent - See Message class.

post_setSent

public void post_setSent(java.util.Date sent)

Post-condition for setSent.

Parameters:

sent - See Message class.

pre_setTo

public void pre_setTo(java.util.List<Address> to)

Pre-condition for setTo.

Parameters:

to - See Message class.

post_setTo

public void post_setTo(java.util.List<Address> to)

Post-condition for setTo method.

Parameters:

to - See Message class.

pre_getToIter

public void pre_getToIter()

Pre-condition for getToIter method.

pre_addTo

public void pre_addTo(Address address)

Pre-condition for addTo method.

Parameters:

address - See Message class.

pre_appendData

public void pre_appendData(java.lang.String data)

Pre-condition for appendData method.

Parameters:

data - See Message class.

pre_toString

public void pre_toString()

Pre-condition for toString method.

post_toString

public void post_toString()

Post-condition for toString method.