org.jmlspecs.jml4.esc.gc.lang.sugared
Class SugaredPostcondition

java.lang.Object
  org.jmlspecs.jml4.esc.gc.lang.sugared.SugaredStatement
      org.jmlspecs.jml4.esc.gc.lang.sugared.SugaredPostcondition

public class SugaredPostcondition
extends SugaredStatement

Field Summary

int	methodStart
SugaredExpression	pred

Fields inherited from class org.jmlspecs.jml4.esc.gc.lang.sugared.SugaredStatement

sourceStart

Constructor Summary

SugaredPostcondition(SugaredExpression pred, SugaredExpression invariant, int sourceStart, int methodStart)

Method Summary

SimpleStatement	accept(DesugaringVisitor visitor)
SugaredStatement	accept(DesugarLoopVisitor visitor, SugaredStatement rest)
SugaredStatement	accept(SimplifyingVisitor visitor)
java.lang.String	toString()

Methods inherited from class java.lang.Object

equals, getClass, hashCode, notify, notifyAll, wait, wait, wait

Field Detail

pred

public final SugaredExpression pred

methodStart

public final int methodStart

Constructor Detail

SugaredPostcondition

public SugaredPostcondition(SugaredExpression pred,
                            SugaredExpression invariant,
                            int sourceStart,
                            int methodStart)

Method Detail

accept

public SimpleStatement accept(DesugaringVisitor visitor)

Specified by:

accept in class SugaredStatement

accept

public SugaredStatement accept(SimplifyingVisitor visitor)

Specified by:

accept in class SugaredStatement

accept

public SugaredStatement accept(DesugarLoopVisitor visitor,
                               SugaredStatement rest)

Specified by:

accept in class SugaredStatement

toString

public java.lang.String toString()

Specified by:

toString in class SugaredStatement