de.uka.ilkd.key.gui

Class DependencyContractCompletion

java.lang.Object

de.uka.ilkd.key.gui.DependencyContractCompletion

All Implemented Interfaces:

InteractiveRuleApplicationCompletion

public class DependencyContractCompletion
extends java.lang.Object
implements InteractiveRuleApplicationCompletion

This class completes the instantiation for a dependency contract applications. The user is queried for the heap with which to instantiate the app.

Nested Class Summary

Nested Classes

Modifier and Type	Class and Description
static class	DependencyContractCompletion.TermStringWrapper

Constructor Summary

Constructors

Constructor and Description
DependencyContractCompletion()

Method Summary

Modifier and Type	Method and Description
boolean	canComplete(IBuiltInRuleApp app) checks if this instance is responsible for the given app
static boolean	checkCanComplete(IBuiltInRuleApp app) Checks if the app is supported.
IBuiltInRuleApp	complete(IBuiltInRuleApp app, Goal goal, boolean forced) method called to complete the given builtin rule application
static void	extractHeaps(java.util.List<LocationVariable> heapContext, java.util.List<PosInOccurrence> steps, DependencyContractCompletion.TermStringWrapper[] heaps, LogicPrinter lp)
static PosInOccurrence	findCorrespondingStep(java.util.List<PosInOccurrence> steps, Term[] resultHeaps)
private static PosInOccurrence	letUserChooseStep(java.util.List<LocationVariable> heapContext, java.util.List<PosInOccurrence> steps, boolean forced, Services services) collects all possible heaps and presents them to the user for selection.

Methods inherited from class java.lang.Object

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

Constructor Detail

DependencyContractCompletion

public DependencyContractCompletion()

Method Detail

complete

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

Description copied from interface: InteractiveRuleApplicationCompletion

method called to complete the given builtin rule application

Specified by:

complete in interface InteractiveRuleApplicationCompletion

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

letUserChooseStep

private static PosInOccurrence letUserChooseStep(java.util.List<LocationVariable> heapContext,
                                                 java.util.List<PosInOccurrence> steps,
                                                 boolean forced,
                                                 Services services)

collects all possible heaps and presents them to the user for selection. If forced is true the user will not be asked if only one alternative is possible

Parameters:

steps -

forced -

services -

Returns:

findCorrespondingStep

public static PosInOccurrence findCorrespondingStep(java.util.List<PosInOccurrence> steps,
                                                    Term[] resultHeaps)

extractHeaps

public static void extractHeaps(java.util.List<LocationVariable> heapContext,
                                java.util.List<PosInOccurrence> steps,
                                DependencyContractCompletion.TermStringWrapper[] heaps,
                                LogicPrinter lp)

canComplete

public boolean canComplete(IBuiltInRuleApp app)

Description copied from interface: InteractiveRuleApplicationCompletion

checks if this instance is responsible for the given app

Specified by:

canComplete in interface InteractiveRuleApplicationCompletion

Parameters:

app - the rule app

Returns:

true iff this instance might be able to complete the app

checkCanComplete

public static boolean checkCanComplete(IBuiltInRuleApp app)

Checks if the app is supported. This functionality is also used by the Eclipse plug-ins like the KeYIDE.