de.uka.ilkd.key.logic.label

Class BlockContractValidityTermLabel

java.lang.Object

de.uka.ilkd.key.logic.label.BlockContractValidityTermLabel

All Implemented Interfaces:

TermLabel, Named

public class BlockContractValidityTermLabel
extends java.lang.Object
implements TermLabel

Label attached to the modality of the validity branch of a block contract.

Field Summary

Fields

Modifier and Type	Field and Description
private ProgramVariable	exceptionVariable The name of the exception variable to distinguish normal from exceptional termination.
static Name	NAME The unique name of this label.

Constructor Summary

Constructors

Constructor and Description
BlockContractValidityTermLabel(ProgramVariable exceptionVariable) Constructor.

Method Summary

Modifier and Type	Method and Description
ProgramVariable	getChild(int i) Retrieves the i-th parameter object of this term label.
int	getChildCount() Gets the number of parameters of this term label.
ProgramVariable	getExceptionVariable() retrieves the original exception variable as found in the local variable declaration statement
Name	name() returns the name of this element
java.lang.String	toString()

Methods inherited from class java.lang.Object

clone, equals, finalize, getClass, hashCode, notify, notifyAll, wait, wait, wait

Field Detail

NAME

public static final Name NAME

The unique name of this label.

exceptionVariable

private final ProgramVariable exceptionVariable

The name of the exception variable to distinguish normal from exceptional termination.

Constructor Detail

BlockContractValidityTermLabel

public BlockContractValidityTermLabel(ProgramVariable exceptionVariable)

Constructor.

Parameters:

exceptionVariable - the exception variable to distinguish normal from exceptional termination.

Method Detail

toString

public java.lang.String toString()

Overrides:

toString in class java.lang.Object

getExceptionVariable

public ProgramVariable getExceptionVariable()

retrieves the original exception variable as found in the local variable declaration statement

Returns:

the original exception variable

getChild

public ProgramVariable getChild(int i)

Retrieves the i-th parameter object of this term label.

A term label may have structure, i.e. can be parameterized.

Specified by:

getChild in interface TermLabel

Parameters:

i - the number of the parameter to retrieve ( 0 <= i < getChildCount())

Returns:

the selected parameter

getChildCount

public int getChildCount()

Gets the number of parameters of this term label.

Specified by:

getChildCount in interface TermLabel

Returns:

the number of parameters (a non-negative number)

name

public Name name()

returns the name of this element

Specified by:

name in interface Named

Returns:

the name of the element