de.uka.ilkd.key.rule

Class AbstractAuxiliaryContractRule

java.lang.Object

de.uka.ilkd.key.rule.AbstractAuxiliaryContractRule

All Implemented Interfaces:

BuiltInRule, Rule

Direct Known Subclasses:

AbstractBlockContractRule, AbstractLoopContractRule

public abstract class AbstractAuxiliaryContractRule
extends java.lang.Object
implements BuiltInRule

Rule for the application of AuxiliaryContracts.

Author:

wacker, lanzinger

See Also:

AbstractAuxiliaryContractBuiltInRuleApp

Nested Class Summary

Nested Classes

Modifier and Type	Class and Description
static class	AbstractAuxiliaryContractRule.Instantiation This encapsulates all information from the rule application that is needed to apply the rule.
protected static class	AbstractAuxiliaryContractRule.Instantiator A builder for AbstractAuxiliaryContractRule.Instantiations.

Field Summary

Fields

Modifier and Type	Field and Description
static java.lang.String	FULL_PRECONDITION_TERM_HINT
static java.lang.String	NEW_POSTCONDITION_TERM_HINT

Constructor Summary

Constructors

Constructor and Description
AbstractAuxiliaryContractRule()

Method Summary

Modifier and Type	Method and Description
protected static Term	createLocalAnonUpdate(ImmutableSet<ProgramVariable> localOuts, Services services)
protected static ProgramVariable	createLocalVariable(java.lang.String nameBase, KeYJavaType type, Services services)
java.lang.String	displayName() returns the display name of the rule
abstract Term	getLastFocusTerm()
abstract AbstractAuxiliaryContractRule.Instantiation	getLastInstantiation()
boolean	isApplicableOnSubTerms()
protected static boolean	occursNotAtTopLevelInSuccedent(PosInOccurrence occurrence)
protected static void	register(ProgramVariable pv, Services services) Adds pv to the sevices' program variable namespace.
protected abstract void	setLastFocusTerm(Term formula)
protected abstract void	setLastInstantiation(AbstractAuxiliaryContractRule.Instantiation inst)
java.lang.String	toString()

Methods inherited from class java.lang.Object

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

Methods inherited from interface de.uka.ilkd.key.rule.BuiltInRule

createApp, isApplicable

Methods inherited from interface de.uka.ilkd.key.rule.Rule

apply, name

Field Detail

FULL_PRECONDITION_TERM_HINT

public static final java.lang.String FULL_PRECONDITION_TERM_HINT

See Also:

Constant Field Values

NEW_POSTCONDITION_TERM_HINT

public static final java.lang.String NEW_POSTCONDITION_TERM_HINT

See Also:

Constant Field Values

Constructor Detail

AbstractAuxiliaryContractRule

public AbstractAuxiliaryContractRule()

Method Detail

occursNotAtTopLevelInSuccedent

protected static boolean occursNotAtTopLevelInSuccedent(PosInOccurrence occurrence)

Parameters:

occurrence - an occurrence.

Returns:

true iff the occurrence is not at the top level in the succedent.

register

protected static void register(ProgramVariable pv,
                               Services services)

Adds pv to the sevices' program variable namespace.

Parameters:

pv - a variable.

services - services.

getLastInstantiation

public abstract AbstractAuxiliaryContractRule.Instantiation getLastInstantiation()

Returns:

the instantiation from the last time this rule was applied.

getLastFocusTerm

public abstract Term getLastFocusTerm()

Returns:

the term on which the rule was last applied.

setLastInstantiation

protected abstract void setLastInstantiation(AbstractAuxiliaryContractRule.Instantiation inst)

Parameters:

inst - the last instantiation.

See Also:

getLastInstantiation()

setLastFocusTerm

protected abstract void setLastFocusTerm(Term formula)

Parameters:

formula - the last focus term.

See Also:

getLastFocusTerm()

displayName

public java.lang.String displayName()

Description copied from interface: Rule

returns the display name of the rule

Specified by:

displayName in interface Rule

toString

public java.lang.String toString()

Overrides:

toString in class java.lang.Object

isApplicableOnSubTerms

public boolean isApplicableOnSubTerms()

Specified by:

isApplicableOnSubTerms in interface BuiltInRule

createLocalAnonUpdate

protected static Term createLocalAnonUpdate(ImmutableSet<ProgramVariable> localOuts,
                                            Services services)

Parameters:

localOuts - a set of variables.

services - services.

Returns:

an anonymizing update for the specified variables.

createLocalVariable

protected static ProgramVariable createLocalVariable(java.lang.String nameBase,
                                                     KeYJavaType type,
                                                     Services services)

Parameters:

nameBase - a base name.

type - a type.

services - services.

Returns:

a new local variable with the specified base name of the specified type.