org.jmlspecs.jml4.fspv.theory
Class TheoryLoopAnnotationsExpression

java.lang.Object
  org.jmlspecs.jml4.fspv.theory.TheoryExpression
      org.jmlspecs.jml4.fspv.theory.TheoryLoopAnnotationsExpression

public class TheoryLoopAnnotationsExpression
extends TheoryExpression

Field Summary

static TheoryLoopAnnotationsExpression	EMPTY_LOOP_ANNOTATIONS
TheoryInvariantExpression	invariant
TheoryVariantExpression	variant

Fields inherited from class org.jmlspecs.jml4.fspv.theory.TheoryExpression

EMPTY, type, withSideEffects

Constructor Summary

TheoryLoopAnnotationsExpression(TheoryInvariantExpression invariant, TheoryVariantExpression variant)

Method Summary

TheoryExpression	invariantAt(int i)
int	invariantSize()
TheoryExpression	variantAt(int i)
int	variantSize()
java.lang.Object	visit(TheoryVisitor visitor)

Methods inherited from class java.lang.Object

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

Field Detail

EMPTY_LOOP_ANNOTATIONS

public static final TheoryLoopAnnotationsExpression EMPTY_LOOP_ANNOTATIONS

invariant

public final TheoryInvariantExpression invariant

variant

public final TheoryVariantExpression variant

Constructor Detail

TheoryLoopAnnotationsExpression

public TheoryLoopAnnotationsExpression(TheoryInvariantExpression invariant,
                                       TheoryVariantExpression variant)

Method Detail

invariantSize

public int invariantSize()

invariantAt

public TheoryExpression invariantAt(int i)

variantSize

public int variantSize()

variantAt

public TheoryExpression variantAt(int i)

visit

public java.lang.Object visit(TheoryVisitor visitor)

Overrides:

visit in class TheoryExpression