de.uka.ilkd.key.logic.label

Interface TermLabel

All Superinterfaces:

Named

All Known Implementing Classes:

BlockContractValidityTermLabel, FormulaTermLabel, ParameterlessTermLabel, SymbolicExecutionTermLabel, TermLabelSV

public interface TermLabel
extends Named

The interface for term labels. Term labels are annotations that can be attached to Terms and carry additional information. They must not be soundness relevant. But they may be used in strategies to compute the order in which rules are applied.

Terms with or without term labels are still unmodifiable. It is recommended to implement TermLabels including their parameters also unmodifiable. For new TermLabels without parameters class ParameterlessTermLabel can be used.

A term label can have parameters accessible via getChild(int) and getChildCount(). Such parameters can be any Object. But keep in mind that it is required to parse Strings into Terms, e.g. if it is used in a Taclet definition or if a cut rule is applied. For convenience parameters are always printed as Strings and have to be parsed individually into the required Object instances via a TermLabelFactory.

Which TermLabels are available is defined by the Profile or more precise by its TermLabelManager available via Profile.getTermLabelManager(). The TermLabelManager provides also the functionality to parse and maintain them during prove.

The TermLabelManager is responsible during prove to maintain term labels. This means that labels of new Terms created during rule application are computed via TermLabelManager#instantiateLabels( de.uka.ilkd.key.logic.label.TermLabelState, de.uka.ilkd.key.java.Services, de.uka.ilkd.key.logic.PosInOccurrence, Term, de.uka.ilkd.key.rule.Rule, de.uka.ilkd.key.proof.Goal, Object, Term, de.uka.ilkd.key.logic.op.Operator, de.uka.ilkd.key.collection.ImmutableArray, de.uka.ilkd.key.collection.ImmutableArray, de.uka.ilkd.key.logic.JavaBlock) and of existing Terms are refactored (added or removed) via TermLabelManager#refactorGoal( de.uka.ilkd.key.logic.label.TermLabelState, de.uka.ilkd.key.java.Services, de.uka.ilkd.key.logic.PosInOccurrence, Term, de.uka.ilkd.key.rule.Rule, de.uka.ilkd.key.proof.Goal, Term).

Antecedent and succedent of a Sequent are sets. The equality check if a SequentFormula is already contained ignores TermLabels. To ensure that TermLabels are not lost, TermLabelManager.mergeLabels(de.uka.ilkd.key.java.Services, de.uka.ilkd.key.logic.SequentChangeInfo) merges the labels of the existing SequentFormula with those of the rejected SequentFormula. How this is done in detail is implemented by a TermLabelMerger. If no TermLabelMerger is available, the TermLabel of the rejected SequentFormula are lost.

To implement a new TermLabel follow the following steps:

1. Provide TermLabel implementation.
   • Without parameters: Add a constant with the Name and one with the instance to ParameterlessTermLabel.
   • With parameters: Implement new class realizing the interface TermLabel.
2. Provide a TermLabelFactory which will be used during the parse process.
   • Without parameters: Reuse class SingletonLabelFactory with the instance added as constant to ParameterlessTermLabel.
   • With parameters: Implement new class realizing the interface TermLabelFactory.
3. Define how the TermLabel is maintained during prove. This may have to be done for different rules in different ways. Orienteer yourself for each rule on the examples provided in the following. They are ordered with the less to the most performance impact during prove. Try to treat as many rules as possible with the same solution, but choose always the solution with the less performance impact!
   • a(b<<l>>) ~~> c(b<<l>>): b is a constant which is never rewritten by rules. The label stays on the Term and will be dropped when the Term is dropped. Nothing to be done.
   • a ~~> b<<l>>: The taclet rewrites a into b<<l>>. TermLabels defined by taclets are automatically considered during rule application. Nothing to be done.
   • a<<l>> ~~> b<<l>> The application Term a contains the label before. Use an application TermLabelPolicy to ensure that it is maintained.
   • Update[...]<<l>> ~~> Update[...new...]<<l>> The application Term Update contains a Modality. Use a modality TermLabelPolicy to ensure that it is maintained.
   • 2 + 3 ~~> 5<>a>>: A new label has to be added which is not provided by the rule. Implement a TermLabelUpdate which adds, sorts or removes TermLabel before a new Term is created.
   • 2<<a>> + 3<<b>> ~~> 5<<a>>: A direct child of the application Term a contains the label before. Use a direct ChildTermLabelPolicy to ensure that it is added also to the new term.
   • 2 + (3<<a>> - 1<<b>>) ~~> 4<<a>>: A child or grandchild of the application Term a contains the label before. Use a direct ChildTermLabelPolicy to ensure that it is added also to the new term.
   • 2<<a>> + 3<<b>> ~~> 2<<a>> - 3: Implement a TermLabelRefactoring which works on TermLabelRefactoring.RefactoringScope.APPLICATION_DIRECT_CHILDREN to freely add or remove TermLabels on direct children of the application Term.
   • 2 + (3<<a>> - 1<<b>>) ~~> 2 * (3<<a>> - 1): Implement a TermLabelRefactoring which works on TermLabelRefactoring.RefactoringScope.APPLICATION_CHILDREN_AND_GRANDCHILDREN_SUBTREE to freely add or remove TermLabels on children and grandchildren of the application Term.
   • Change labels on the whole Sequent: Implement a TermLabelRefactoring which works on TermLabelRefactoring.RefactoringScope.SEQUENT to freely add or remove TermLabels on any Term of the Sequent.
   • Implement a TermLabelMerger to ensure that TermLabels are maintained in case of rejected SequentFormulas.
4. Make sure that the Profile supports the new TermLabel. All implementations from the previous have to be bundled in a TermLabelManager.TermLabelConfiguration instance. This instance has to be created and returned in AbstractProfile.computeTermLabelConfiguration().
5. During rule application, especially for BuiltInRule, the functionality of TermLabelManager to maintain TermLabels is only called for newly created Terms labeled up to now. If your TermLabelPolicy, TermLabelUpdate or TermLabelRefactoring is not called on the right Term, it is your task to call TermLabelManager#instantiateLabels( de.uka.ilkd.key.logic.label.TermLabelState, de.uka.ilkd.key.java.Services, de.uka.ilkd.key.logic.PosInOccurrence, de.uka.ilkd.key.rule.Rule, de.uka.ilkd.key.proof.Goal, Object, Term, de.uka.ilkd.key.logic.op.Operator, de.uka.ilkd.key.collection.ImmutableArray, de.uka.ilkd.key.collection.ImmutableArray, de.uka.ilkd.key.logic.JavaBlock) and TermLabelManager#refactorLabels( de.uka.ilkd.key.logic.label.TermLabelState, de.uka.ilkd.key.java.Services, de.uka.ilkd.key.logic.PosInOccurrence, de.uka.ilkd.key.rule.Rule, de.uka.ilkd.key.proof.Goal, Term) on the right place in the rule implementation.

Author:

Martin Hentschel

See Also:

TermLabelManager

Method Summary

Modifier and Type	Method and Description
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.

Methods inherited from interface de.uka.ilkd.key.logic.Named

name

Method Detail

getChild

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.

Parameters:

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

Returns:

the selected parameter

Throws:

java.lang.IndexOutOfBoundsException - if the given parameter number i is negative or greater-or-equal the number of parameters returned by getChildCount()

getChildCount

int getChildCount()

Gets the number of parameters of this term label.

Returns:

the number of parameters (a non-negative number)