Package | Description |
---|---|
de.uka.ilkd.key.gui |
This package contains classes forming the graphical user interface of KeY.
|
de.uka.ilkd.key.rule |
This package contains classes for implementing rules.
|
de.uka.ilkd.key.rule.merge | |
de.uka.ilkd.key.symbolic_execution.rule |
Modifier and Type | Method and Description |
---|---|
LoopSpecification |
InvariantConfigurator.getLoopInvariant(LoopSpecification loopInv,
Services services,
boolean requiresVariant,
java.util.List<LocationVariable> heapContext)
Creates a Dialog.
|
Modifier and Type | Method and Description |
---|---|
ImmutableList<Goal> |
BlockContractExternalRule.apply(Goal goal,
Services services,
RuleApp ruleApp) |
ImmutableList<Goal> |
Rule.apply(Goal goal,
Services services,
RuleApp ruleApp)
the rule is applied on the given goal using the
information of rule application.
|
ImmutableList<Goal> |
WhileInvariantRule.apply(Goal goal,
Services services,
RuleApp ruleApp) |
ImmutableList<Goal> |
BlockContractInternalRule.apply(Goal goal,
Services services,
RuleApp ruleApp) |
ImmutableList<Goal> |
LoopContractExternalRule.apply(Goal goal,
Services services,
RuleApp ruleApp) |
ImmutableList<Goal> |
LoopContractInternalRule.apply(Goal goal,
Services services,
RuleApp ruleApp) |
ImmutableList<Goal> |
LoopApplyHeadRule.apply(Goal goal,
Services services,
RuleApp application) |
ImmutableList<Goal> |
LoopScopeInvariantRule.apply(Goal goal,
Services services,
RuleApp ruleApp) |
AbstractLoopInvariantRule.LoopInvariantInformation |
AbstractLoopInvariantRule.doPreparations(Goal goal,
Services services,
RuleApp ruleApp)
Constructs the data needed for the currently implemented loop invariants;
also prepares the new set of goals, that is splitting the current goal is
no longer required after calling this method.
|
protected static AbstractLoopInvariantRule.Instantiation |
AbstractLoopInvariantRule.instantiate(LoopInvariantBuiltInRuleApp app,
Services services)
Constructs the
AbstractLoopInvariantRule.Instantiation object containing the relevant
parameters for this LoopScopeInvariantRule application. |
Modifier and Type | Method and Description |
---|---|
ImmutableList<Goal> |
MergeRule.apply(Goal goal,
Services services,
RuleApp ruleApp) |
ImmutableList<Goal> |
CloseAfterMerge.apply(Goal goal,
Services services,
RuleApp ruleApp) |
Modifier and Type | Method and Description |
---|---|
ImmutableList<Goal> |
ModalitySideProofRule.apply(Goal goal,
Services services,
RuleApp ruleApp)
the rule is applied on the given goal using the
information of rule application.
|
ImmutableList<Goal> |
QuerySideProofRule.apply(Goal goal,
Services services,
RuleApp ruleApp)
the rule is applied on the given goal using the
information of rule application.
|
Copyright © 2003-2019 The KeY-Project.