de.uka.ilkd.key.logic.label

Class FormulaTermLabel

java.lang.Object

de.uka.ilkd.key.logic.label.FormulaTermLabel

All Implemented Interfaces:

TermLabel, Named

public class FormulaTermLabel
extends java.lang.Object
implements TermLabel

Label attached to a predicates for instance in postconditions, loop invariants or precondition checks of applied operation contracts.

Field Summary

Fields

Modifier and Type	Field and Description
static java.lang.String	BEFORE_ID_SEPARATOR Separator between multiple before IDs.
private java.lang.String	beforeIds The optional previous IDs of the label this one is derived from separated by ";".
private int	majorId The unique major ID of this term label in the Sequent.
private int	minorId The per major ID unique minor ID of this term label in the Sequent.
static Name	NAME The unique name of this label.
static java.lang.String	PROOF_COUNTER_NAME The name used in Services.getCounter(String) to keep track of the already used IDs.
static java.lang.String	PROOF_COUNTER_SUB_PREFIX The prefix of the name used in Services.getCounter(String) to keep track of the already used sub IDs.

Constructor Summary

Constructors

Constructor and Description
FormulaTermLabel(int majorId, int minorId) Constructor.
FormulaTermLabel(int majorId, int minorId, java.util.Collection<java.lang.String> beforeIds) Constructor.
FormulaTermLabel(java.lang.String id) Constructor.
FormulaTermLabel(java.lang.String id, java.lang.String beforeIds) Constructor.

Method Summary

Modifier and Type	Method and Description
boolean	equals(java.lang.Object o)
java.lang.String[]	getBeforeIds() Returns the optional previous IDs of the label this one is derived from.
private static java.lang.String[]	getBeforeIds(java.lang.String beforeIds) Returns the optional previous IDs of the label this one is derived from.
java.lang.Object	getChild(int i) Retrieves the i-th parameter object of this term label.
int	getChildCount() Gets the number of parameters of this term label.
java.lang.String	getId() Returns the unique ID of this label in the Sequent.
int	getMajorId() Returns the major part of the unique ID.
static int	getMajorId(java.lang.String id) Returns the major part of the given ID.
int	getMinorId() Returns the minor part of the unique ID.
static int	getMinorId(java.lang.String id) Returns the minor part of the given ID.
static java.util.List<java.lang.String>	getValidBeforeIds(java.lang.String beforeIds) Returns the optional previous IDs if they are all valid.
Name	name() returns the name of this element
static int	newLabelSubID(Services services, FormulaTermLabel label) Creates a new label sub ID.
static int	newLabelSubID(Services services, int labelId) Creates a new label sub ID.
java.lang.String	toString()

Methods inherited from class java.lang.Object

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

Field Detail

NAME

public static final Name NAME

The unique name of this label.

PROOF_COUNTER_NAME

public static final java.lang.String PROOF_COUNTER_NAME

The name used in Services.getCounter(String) to keep track of the already used IDs.

See Also:

Constant Field Values

PROOF_COUNTER_SUB_PREFIX

public static final java.lang.String PROOF_COUNTER_SUB_PREFIX

The prefix of the name used in Services.getCounter(String) to keep track of the already used sub IDs.

See Also:

Constant Field Values

BEFORE_ID_SEPARATOR

public static final java.lang.String BEFORE_ID_SEPARATOR

Separator between multiple before IDs.

See Also:

Constant Field Values

majorId

private final int majorId

The unique major ID of this term label in the Sequent.

minorId

private final int minorId

The per major ID unique minor ID of this term label in the Sequent.

beforeIds

private final java.lang.String beforeIds

The optional previous IDs of the label this one is derived from separated by ";".

Constructor Detail

FormulaTermLabel

public FormulaTermLabel(java.lang.String id)
                 throws TermLabelException

Constructor.

Parameters:

id - The unique ID of this term label in the Sequent.

Throws:

TermLabelException - Occurred Exception in case that the given ID is not valid.

FormulaTermLabel

public FormulaTermLabel(java.lang.String id,
                        java.lang.String beforeIds)
                 throws TermLabelException

Constructor.

Parameters:

id - The unique ID of this term label in the Sequent.

beforeIds - The optional previous IDs of the label this one is derived from separated by ";".

Throws:

TermLabelException - Occurred Exception in case that the given IDs are not valid.

FormulaTermLabel

public FormulaTermLabel(int majorId,
                        int minorId)

Constructor.

Parameters:

majorId - The major part of the unique ID.

minorId - The minor part of the unique ID.

FormulaTermLabel

public FormulaTermLabel(int majorId,
                        int minorId,
                        java.util.Collection<java.lang.String> beforeIds)

Constructor.

Parameters:

majorId - The major part of the unique ID.

minorId - The minor part of the unique ID.

beforeIds - The optional previous ID of the label this one is derived from.

Method Detail

equals

public boolean equals(java.lang.Object o)

Overrides:

equals in class java.lang.Object

toString

public java.lang.String toString()

Overrides:

toString in class java.lang.Object

getChild

public java.lang.Object 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)

getId

public java.lang.String getId()

Returns the unique ID of this label in the Sequent.

Returns:

The unique ID of this label in the Sequent.

getMajorId

public int getMajorId()

Returns the major part of the unique ID.

Returns:

The major part of the unique ID.

getMajorId

public static int getMajorId(java.lang.String id)
                      throws TermLabelException

Returns the major part of the given ID.

Parameters:

id - The ID to extract its major part.

Returns:

The major part of the given ID.

Throws:

TermLabelException - Occurred Exception in case that the given ID is not valid.

getMinorId

public int getMinorId()

Returns the minor part of the unique ID.

Returns:

The minor part of the unique ID.

getMinorId

public static int getMinorId(java.lang.String id)
                      throws TermLabelException

Returns the minor part of the given ID.

Parameters:

id - The ID to extract its minor part.

Returns:

The minor part of the given ID.

Throws:

TermLabelException - Occurred Exception in case that the given ID is not valid.

getBeforeIds

public java.lang.String[] getBeforeIds()

Returns the optional previous IDs of the label this one is derived from.

Returns:

The optional previous IDs of the label this one is derived from.

getBeforeIds

private static java.lang.String[] getBeforeIds(java.lang.String beforeIds)

Returns the optional previous IDs of the label this one is derived from.

Parameters:

beforeIds - The String with the before IDs.

Returns:

The optional previous IDs of the label this one is derived from.

getValidBeforeIds

public static java.util.List<java.lang.String> getValidBeforeIds(java.lang.String beforeIds)
                                                          throws TermLabelException

Returns the optional previous IDs if they are all valid.

Parameters:

beforeIds - The String with the before IDs to analyze.

Returns:

The valid before IDs.

Throws:

TermLabelException - Occurred Exception in case that the given IDs are not valid.

name

public Name name()

returns the name of this element

Specified by:

name in interface Named

Returns:

the name of the element

newLabelSubID

public static int newLabelSubID(Services services,
                                FormulaTermLabel label)

Creates a new label sub ID.

Parameters:

services - The Services to use.

label - The parent FormulaTermLabel which provides the major ID.

Returns:

The new label sub ID.

newLabelSubID

public static int newLabelSubID(Services services,
                                int labelId)

Creates a new label sub ID.

Parameters:

services - The Services to use.

labelId - The parent FormulaTermLabel which provides the major ID.

Returns:

The new label sub ID.