de.uka.ilkd.key.gui

Interface InteractiveRuleApplicationCompletion

All Known Implementing Classes:

BlockContractExternalCompletion, BlockContractInternalCompletion, DependencyContractCompletion, FunctionalOperationContractCompletion, LoopApplyHeadCompletion, LoopContractExternalCompletion, LoopContractInternalCompletion, LoopInvariantRuleCompletion, MergeRuleCompletion

public interface InteractiveRuleApplicationCompletion

Instances of class implementing this interface are able to complete rule applications. At the moment they are only responsible for built-in rule apps, but they should be generalized to treat taclets as well.

Method Summary

Modifier and Type	Method and Description
boolean	canComplete(IBuiltInRuleApp app) checks if this instance is responsible for the given app
IBuiltInRuleApp	complete(IBuiltInRuleApp app, Goal goal, boolean forced) method called to complete the given builtin rule application

Method Detail

complete

IBuiltInRuleApp complete(IBuiltInRuleApp app,
                         Goal goal,
                         boolean forced)

method called to complete the given builtin rule application

Parameters:

app - the app to complete

goal - the goal where the app will be applied

forced - a boolean indicating if the user shall be bothered if the instantiation is unique or can be chosen in a reasonable way as if unique

Returns:

the completed app or null if completion was not possible

canComplete

boolean canComplete(IBuiltInRuleApp app)

checks if this instance is responsible for the given app

Parameters:

app - the rule app

Returns:

true iff this instance might be able to complete the app