org.jmlspecs.jml4.fspv.theory
Class TheoryHelper

java.lang.Object
  org.jmlspecs.jml4.fspv.theory.TheoryHelper

public class TheoryHelper
extends java.lang.Object

Constructor Summary

TheoryHelper()

Method Summary

void	addLemma(TheoryLemma l)
void	addVariable(TheoryVariable v)
TheoryLemma[]	getLemmas()
TheoryVariable[]	getVariables()
boolean	isBlockStack()
boolean	isLocalVarStack()
boolean	isTopStack()
TheoryVariable	lookupVariable(TheoryVariable variable)
TheoryExpression	popExpression()
TheoryStatement	popStatement()
TheoryBlockStatement	popStatements()
void	push(TheoryExpression e)
void	push(TheoryStatement s)
void	pushBlockStack()
void	pushLocalVarStack(TheoryVariable variable)
void	pushLoopStack()
void	reset()

Methods inherited from class java.lang.Object

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

Constructor Detail

TheoryHelper

public TheoryHelper()

Method Detail

pushBlockStack

public void pushBlockStack()

pushLocalVarStack

public void pushLocalVarStack(TheoryVariable variable)

pushLoopStack

public void pushLoopStack()

push

public void push(TheoryStatement s)

popStatement

public TheoryStatement popStatement()

popStatements

public TheoryBlockStatement popStatements()

push

public void push(TheoryExpression e)

popExpression

public TheoryExpression popExpression()

isTopStack

public boolean isTopStack()

isLocalVarStack

public boolean isLocalVarStack()

isBlockStack

public boolean isBlockStack()

addLemma

public void addLemma(TheoryLemma l)

getLemmas

public TheoryLemma[] getLemmas()

addVariable

public void addVariable(TheoryVariable v)

getVariables

public TheoryVariable[] getVariables()

lookupVariable

public TheoryVariable lookupVariable(TheoryVariable variable)

reset

public void reset()