de.uka.ilkd.key.rule

Class ContractRuleApp

java.lang.Object

de.uka.ilkd.key.rule.AbstractBuiltInRuleApp

de.uka.ilkd.key.rule.AbstractContractRuleApp

de.uka.ilkd.key.rule.ContractRuleApp

All Implemented Interfaces:

IBuiltInRuleApp, RuleApp

public class ContractRuleApp
extends AbstractContractRuleApp

Represents an application of a contract rule. Currently, this is only used for applications read in from a proof file; fresh applications are represented as regular BuiltInRuleApps. (yes, I know that this is ugly - BW)

Field Summary

Fields

Modifier and Type	Field and Description
private java.util.List<LocationVariable>	heapContext

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

instantiation

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

builtInRule, ifInsts, pio

Constructor Summary

Constructors

Modifier	Constructor and Description
(package private)	ContractRuleApp(BuiltInRule rule, PosInOccurrence pio)
private	ContractRuleApp(BuiltInRule rule, PosInOccurrence pio, Contract instantiation)

Method Summary

Modifier and Type	Method and Description
ContractRuleApp	forceInstantiate(Goal goal)
java.util.List<LocationVariable>	getHeapContext()
IObserverFunction	getObserverFunction(Services services)
boolean	isSufficientlyComplete() returns true if tryToInstantiate may be able to complete the app
Term	programTerm()
ContractRuleApp	replacePos(PosInOccurrence newPos)
UseOperationContractRule	rule() returns the rule of this rule application
ContractRuleApp	setContract(Contract contract)
ContractRuleApp	setIfInsts(ImmutableList<PosInOccurrence> ifInsts)
ContractRuleApp	tryToInstantiate(Goal goal) Tries to complete the rule application from the available information.

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

check, complete, getInstantiation

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

execute, ifInsts, posInOccurrence, setMutable, toString

Methods inherited from class java.lang.Object

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

Field Detail

heapContext

private java.util.List<LocationVariable> heapContext

Constructor Detail

ContractRuleApp

ContractRuleApp(BuiltInRule rule,
                PosInOccurrence pio)

ContractRuleApp

private ContractRuleApp(BuiltInRule rule,
                        PosInOccurrence pio,
                        Contract instantiation)

Method Detail

replacePos

public ContractRuleApp replacePos(PosInOccurrence newPos)

Specified by:

replacePos in interface IBuiltInRuleApp

Specified by:

replacePos in class AbstractBuiltInRuleApp

setContract

public ContractRuleApp setContract(Contract contract)

Specified by:

setContract in class AbstractContractRuleApp

rule

public UseOperationContractRule rule()

Description copied from class: AbstractBuiltInRuleApp

returns the rule of this rule application

Specified by:

rule in interface IBuiltInRuleApp

Specified by:

rule in interface RuleApp

Overrides:

rule in class AbstractBuiltInRuleApp

isSufficientlyComplete

public boolean isSufficientlyComplete()

Description copied from interface: IBuiltInRuleApp

returns true if tryToInstantiate may be able to complete the app

Specified by:

isSufficientlyComplete in interface IBuiltInRuleApp

Overrides:

isSufficientlyComplete in class AbstractBuiltInRuleApp

Returns:

tryToInstantiate

public ContractRuleApp 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 AbstractContractRuleApp

forceInstantiate

public ContractRuleApp forceInstantiate(Goal goal)

Specified by:

forceInstantiate in interface IBuiltInRuleApp

Overrides:

forceInstantiate in class AbstractBuiltInRuleApp

setIfInsts

public ContractRuleApp setIfInsts(ImmutableList<PosInOccurrence> ifInsts)

Specified by:

setIfInsts in interface IBuiltInRuleApp

Specified by:

setIfInsts in class AbstractBuiltInRuleApp

getHeapContext

public java.util.List<LocationVariable> getHeapContext()

Specified by:

getHeapContext in interface IBuiltInRuleApp

Overrides:

getHeapContext in class AbstractBuiltInRuleApp

programTerm

public Term programTerm()

getObserverFunction

public IObserverFunction getObserverFunction(Services services)

Specified by:

getObserverFunction in class AbstractContractRuleApp