org.jmlspecs.jml4.fspv.theory
Class TheoryLemma

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

public class TheoryLemma
extends java.lang.Object

Field Summary

TheoryBlockStatement	block
static java.lang.String	LEMMA_SUFFIX_SEPARATOR
java.lang.String	name
TheoryExpression	post
TheoryExpression	pre
TheoryVariable[]	variables

Constructor Summary

TheoryLemma(TheoryVariable[] variables, java.lang.String name, TheoryExpression pre, TheoryBlockStatement block, TheoryExpression post)

Method Summary

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

LEMMA_SUFFIX_SEPARATOR

public static final java.lang.String LEMMA_SUFFIX_SEPARATOR

See Also:

Constant Field Values

name

public final java.lang.String name

variables

public final TheoryVariable[] variables

pre

public final TheoryExpression pre

block

public final TheoryBlockStatement block

post

public final TheoryExpression post

Constructor Detail

TheoryLemma

public TheoryLemma(TheoryVariable[] variables,
                   java.lang.String name,
                   TheoryExpression pre,
                   TheoryBlockStatement block,
                   TheoryExpression post)

Method Detail

toString

public java.lang.String toString()

Overrides:

toString in class java.lang.Object

visit

public java.lang.Object visit(TheoryVisitor visitor)