de.uka.ilkd.key.rule.label

Class RemoveInCheckBranchesTermLabelRefactoring

java.lang.Object

de.uka.ilkd.key.rule.label.RemoveInCheckBranchesTermLabelRefactoring

All Implemented Interfaces:

RuleSpecificTask, TermLabelRefactoring

public class RemoveInCheckBranchesTermLabelRefactoring
extends java.lang.Object
implements TermLabelRefactoring

This TermLabelRefactoring removes the supported TermLabel in check branches. These are:

• AbstractAuxiliaryContractRule: Pre
• UseOperationContractRule: Pre
• UseOperationContractRule: Null reference
• WhileInvariantRule: Invariant Initially Valid

Author:

Martin Hentschel

Nested Class Summary

Nested classes/interfaces inherited from interface de.uka.ilkd.key.rule.label.TermLabelRefactoring

TermLabelRefactoring.RefactoringScope

Field Summary

Fields

Modifier and Type	Field and Description
private Name	termLabelNameToRemove The Name of the supported TermLabel.

Constructor Summary

Constructors

Constructor and Description
RemoveInCheckBranchesTermLabelRefactoring(Name termLabelNameToRemove) Constructor.

Method Summary

Modifier and Type	Method and Description
TermLabelRefactoring.RefactoringScope	defineRefactoringScope(TermLabelState state, Services services, PosInOccurrence applicationPosInOccurrence, Term applicationTerm, Rule rule, Goal goal, java.lang.Object hint, Term tacletTerm) Defines if a refactoring is required and if so in which TermLabelRefactoring.RefactoringScope.
ImmutableList<Name>	getSupportedRuleNames() Returns the supported rule Names or null or an empty list if all rules are supported.
void	refactoreLabels(TermLabelState state, Services services, PosInOccurrence applicationPosInOccurrence, Term applicationTerm, Rule rule, Goal goal, java.lang.Object hint, Term tacletTerm, Term term, java.util.List<TermLabel> labels) This method is used to refactor the labels of the given Term.

Methods inherited from class java.lang.Object

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

Field Detail

termLabelNameToRemove

private final Name termLabelNameToRemove

The Name of the supported TermLabel.

Constructor Detail

RemoveInCheckBranchesTermLabelRefactoring

public RemoveInCheckBranchesTermLabelRefactoring(Name termLabelNameToRemove)

Constructor.

Parameters:

termLabelNameToRemove - The Name of the supported TermLabel.

Method Detail

getSupportedRuleNames

public ImmutableList<Name> getSupportedRuleNames()

Returns the supported rule Names or null or an empty list if all rules are supported.

Specified by:

getSupportedRuleNames in interface RuleSpecificTask

Returns:

The list of supported rule Names or null/empty list if all rules are supported.

defineRefactoringScope

public TermLabelRefactoring.RefactoringScope defineRefactoringScope(TermLabelState state,
                                                                    Services services,
                                                                    PosInOccurrence applicationPosInOccurrence,
                                                                    Term applicationTerm,
                                                                    Rule rule,
                                                                    Goal goal,
                                                                    java.lang.Object hint,
                                                                    Term tacletTerm)

Defines if a refactoring is required and if so in which TermLabelRefactoring.RefactoringScope.

Specified by:

defineRefactoringScope in interface TermLabelRefactoring

Parameters:

state - The TermLabelState of the current rule application.

services - The Services used by the Proof on which a Rule is applied right now.

applicationPosInOccurrence - The PosInOccurrence in the previous Sequent which defines the Term that is rewritten.

applicationTerm - The Term defined by the PosInOccurrence in the previous Sequent.

rule - The Rule which is applied.

goal - The optional Goal on which the Term to create will be used.

hint - An optional hint passed from the active rule to describe the term which should be created.

tacletTerm - The optional taclet Term.

Returns:

The required TermLabelRefactoring.RefactoringScope.

refactoreLabels

public void refactoreLabels(TermLabelState state,
                            Services services,
                            PosInOccurrence applicationPosInOccurrence,
                            Term applicationTerm,
                            Rule rule,
                            Goal goal,
                            java.lang.Object hint,
                            Term tacletTerm,
                            Term term,
                            java.util.List<TermLabel> labels)

This method is used to refactor the labels of the given Term.

Specified by:

refactoreLabels in interface TermLabelRefactoring

Parameters:

state - The TermLabelState of the current rule application.

services - The Services used by the Proof on which a Rule is applied right now.

applicationPosInOccurrence - The PosInOccurrence in the previous Sequent which defines the Term that is rewritten.

applicationTerm - The Term defined by the PosInOccurrence in the previous Sequent.

rule - The Rule which is applied.

goal - The optional Goal on which the Term to create will be used.

hint - An optional hint passed from the active rule to describe the term which should be created.

tacletTerm - The optional taclet Term.

term - The Term which is now refactored.

labels - The new labels the Term will have after the refactoring.