org.jmlspecs.jml4.fspv.theory
Class TheoryInvariantExpression

java.lang.Object
  org.jmlspecs.jml4.fspv.theory.TheoryExpression
      org.jmlspecs.jml4.fspv.theory.TheoryBlockExpression
          org.jmlspecs.jml4.fspv.theory.TheoryInvariantExpression

public class TheoryInvariantExpression
extends TheoryBlockExpression

Field Summary

static TheoryInvariantExpression

EMPTY_INVARIANT

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

EMPTY_BLOCK, expressions

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

EMPTY, type, withSideEffects

Constructor Summary

TheoryInvariantExpression(TheoryExpression[] expressions)

Method Summary

java.lang.Object

visit(TheoryVisitor visitor)

Methods inherited from class org.jmlspecs.jml4.fspv.theory.TheoryBlockExpression

expressionAt, size

Methods inherited from class java.lang.Object

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

Field Detail

EMPTY_INVARIANT

public static final TheoryInvariantExpression EMPTY_INVARIANT

Constructor Detail

TheoryInvariantExpression

public TheoryInvariantExpression(TheoryExpression[] expressions)

Method Detail

visit

public java.lang.Object visit(TheoryVisitor visitor)

Overrides:

visit in class TheoryExpression