org.jmlspecs.jml4.fspv.theory
Class TheoryBlockStatement

java.lang.Object
  org.jmlspecs.jml4.fspv.theory.TheoryStatement
      org.jmlspecs.jml4.fspv.theory.TheoryBlockStatement

Direct Known Subclasses:

TheoryLocalDeclarationBlockStatement

public class TheoryBlockStatement
extends TheoryStatement

Field Summary

static TheoryBlockStatement	EMPTY_BLOCK
TheoryStatement[]	statements

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

EMPTY

Constructor Summary

TheoryBlockStatement(TheoryStatement[] statements)

Method Summary

static TheoryBlockStatement	Merge(TheoryBlockStatement prestateAssignments, TheoryBlockStatement block)
int	size()
TheoryStatement	statementAt(int i)
java.lang.String	toString()
java.lang.Object	visit(TheoryVisitor visitor)

Methods inherited from class java.lang.Object

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

Field Detail

EMPTY_BLOCK

public static final TheoryBlockStatement EMPTY_BLOCK

statements

public TheoryStatement[] statements

Constructor Detail

TheoryBlockStatement

public TheoryBlockStatement(TheoryStatement[] statements)

Method Detail

toString

public java.lang.String toString()

Overrides:

toString in class java.lang.Object

size

public int size()

statementAt

public TheoryStatement statementAt(int i)

Merge

public static TheoryBlockStatement Merge(TheoryBlockStatement prestateAssignments,
                                         TheoryBlockStatement block)

visit

public java.lang.Object visit(TheoryVisitor visitor)

Overrides:

visit in class TheoryStatement