de.uka.ilkd.key.rule

Class AbstractContractRuleApp

java.lang.Object

de.uka.ilkd.key.rule.AbstractBuiltInRuleApp

de.uka.ilkd.key.rule.AbstractContractRuleApp

All Implemented Interfaces:

IBuiltInRuleApp, RuleApp

Direct Known Subclasses:

ContractRuleApp, UseDependencyContractApp

public abstract class AbstractContractRuleApp
extends AbstractBuiltInRuleApp

Field Summary

Fields

Modifier and Type	Field and Description
protected Contract	instantiation

Fields inherited from class de.uka.ilkd.key.rule.AbstractBuiltInRuleApp

builtInRule, ifInsts, pio

Constructor Summary

Constructors

Modifier	Constructor and Description
protected	AbstractContractRuleApp(BuiltInRule rule, PosInOccurrence pio)
protected	AbstractContractRuleApp(BuiltInRule rule, PosInOccurrence pio, Contract contract)
protected	AbstractContractRuleApp(BuiltInRule rule, PosInOccurrence pio, ImmutableList<PosInOccurrence> ifInsts, Contract contract)

Method Summary

Modifier and Type	Method and Description
AbstractContractRuleApp	check(Services services)
boolean	complete() returns true if all variables are instantiated
Contract	getInstantiation()
abstract IObserverFunction	getObserverFunction(Services services)
abstract AbstractContractRuleApp	setContract(Contract contract)
abstract AbstractContractRuleApp	tryToInstantiate(Goal goal) Tries to complete the rule application from the available information.

Methods inherited from class de.uka.ilkd.key.rule.AbstractBuiltInRuleApp

execute, forceInstantiate, getHeapContext, ifInsts, isSufficientlyComplete, posInOccurrence, replacePos, rule, setIfInsts, setMutable, toString

Methods inherited from class java.lang.Object

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

Field Detail

instantiation

protected final Contract instantiation

Constructor Detail

AbstractContractRuleApp

protected AbstractContractRuleApp(BuiltInRule rule,
                                  PosInOccurrence pio)

AbstractContractRuleApp

protected AbstractContractRuleApp(BuiltInRule rule,
                                  PosInOccurrence pio,
                                  Contract contract)

AbstractContractRuleApp

protected AbstractContractRuleApp(BuiltInRule rule,
                                  PosInOccurrence pio,
                                  ImmutableList<PosInOccurrence> ifInsts,
                                  Contract contract)

Method Detail

getInstantiation

public Contract getInstantiation()

check

public AbstractContractRuleApp check(Services services)

tryToInstantiate

public abstract AbstractContractRuleApp tryToInstantiate(Goal goal)

Description copied from interface: IBuiltInRuleApp

Tries to complete the rule application from the available information. Attention: Do neither add GUI code to the rules nor use this method directly Instead ask the implementation of the UserInterfaceControl to complete a built-in rule. Returns a complete app only if there is exactly one contract. If you want a complete app for combined contracts, use forceInstantiate instead. For an example implementation see e.g. UseOperationContractRule or UseDependencyContractRule.

Specified by:

tryToInstantiate in interface IBuiltInRuleApp

Specified by:

tryToInstantiate in class AbstractBuiltInRuleApp

setContract

public abstract AbstractContractRuleApp setContract(Contract contract)

complete

public boolean complete()

Description copied from class: AbstractBuiltInRuleApp

returns true if all variables are instantiated

Specified by:

complete in interface RuleApp

Overrides:

complete in class AbstractBuiltInRuleApp

Returns:

true if all variables are instantiated

getObserverFunction

public abstract IObserverFunction getObserverFunction(Services services)