Package | Description |
---|---|
de.uka.ilkd.key.axiom_abstraction.predicateabstraction | |
de.uka.ilkd.key.control | |
de.uka.ilkd.key.gui |
This package contains classes forming the graphical user interface of KeY.
|
de.uka.ilkd.key.gui.lemmatagenerator | |
de.uka.ilkd.key.informationflow.rule | |
de.uka.ilkd.key.logic |
provides a representation for the term and sequent
structure.
|
de.uka.ilkd.key.logic.op |
contains the operators of
Term s. |
de.uka.ilkd.key.logic.sort |
This package contains different kinds and implementations subtyping interface Sort.
|
de.uka.ilkd.key.nparser.builder | |
de.uka.ilkd.key.pp |
This package contains pretty-printing functionality used by the GUI and for
saving proofs.
|
de.uka.ilkd.key.proof |
This package contains the core data structures of proofs, nodes, goals, as well
as machinery to deal with these data structures.
|
de.uka.ilkd.key.proof.init |
This package contains classes handling prover initialisation.
|
de.uka.ilkd.key.proof.io |
Classes related to loading and saving proof files.
|
de.uka.ilkd.key.proof.mgt |
This package contains classes for proof environments and proof management.
|
de.uka.ilkd.key.rule |
This package contains classes for implementing rules.
|
de.uka.ilkd.key.rule.executor.javadl | |
de.uka.ilkd.key.rule.merge | |
de.uka.ilkd.key.rule.metaconstruct |
contains classes representing the meta constructs of
Taclet s. |
de.uka.ilkd.key.rule.tacletbuilder | |
de.uka.ilkd.key.settings | |
de.uka.ilkd.key.speclang |
This package contains the specification language frontends of KeY.
|
de.uka.ilkd.key.speclang.jml | |
de.uka.ilkd.key.speclang.jml.translation | |
de.uka.ilkd.key.strategy |
This package contains classes implementing the proof search strategies of KeY.
|
de.uka.ilkd.key.strategy.quantifierHeuristics | |
de.uka.ilkd.key.symbolic_execution | |
de.uka.ilkd.key.symbolic_execution.profile | |
de.uka.ilkd.key.taclettranslation.assumptions | |
de.uka.ilkd.key.taclettranslation.lemma | |
de.uka.ilkd.key.ui | |
de.uka.ilkd.key.util |
This package is a grab bag of miscellaneous useful code fragments.
|
de.uka.ilkd.key.util.mergerule | |
org.key_project.util.collection |
Modifier and Type | Method and Description |
---|---|
ImmutableSet<AbstractionPredicate> |
AbstractPredicateAbstractionDomainElement.getPredicates() |
Modifier and Type | Method and Description |
---|---|
void |
AbstractPredicateAbstractionDomainElement.setPredicates(ImmutableSet<AbstractionPredicate> predicates) |
Constructor and Description |
---|
AbstractPredicateAbstractionDomainElement(ImmutableSet<AbstractionPredicate> predicates)
Constructs a new
AbstractPredicateAbstractionDomainElement from a
given list of abstraction predicates. |
ConjunctivePredicateAbstractionDomainElement(ImmutableSet<AbstractionPredicate> predicates)
Constructs a new
ConjunctivePredicateAbstractionDomainElement
from a given list of abstraction predicates. |
DisjunctivePredicateAbstractionDomainElement(ImmutableSet<AbstractionPredicate> predicates)
Constructs a new
DisjunctivePredicateAbstractionDomainElement
from a given list of abstraction predicates. |
SimplePredicateAbstractionDomainElement(ImmutableSet<AbstractionPredicate> predicates)
Constructs a new
SimplePredicateAbstractionDomainElement from a
given list of abstraction predicates. |
Modifier and Type | Method and Description |
---|---|
protected ImmutableSet<TacletApp> |
AbstractProofControl.getAppsForName(Goal goal,
java.lang.String name,
PosInOccurrence pos)
collects all Taclet applications at the given position of the specified
taclet
|
protected ImmutableSet<TacletApp> |
AbstractProofControl.getAppsForName(Goal goal,
java.lang.String name,
PosInOccurrence pos,
TacletFilter filter)
collects all taclet applications for the given position and taclet
(identified by its name) matching the filter condition
|
ImmutableSet<IBuiltInRuleApp> |
AbstractProofControl.getBuiltInRuleApp(Goal focusedGoal,
BuiltInRule rule,
PosInOccurrence pos)
collects all built-in rule applications for the given rule that are
applicable at position 'pos' and the current user constraint
|
protected ImmutableSet<IBuiltInRuleApp> |
AbstractProofControl.getBuiltInRuleAppsForName(Goal focusedGoal,
java.lang.String name,
PosInOccurrence pos)
collects all applications of a rule given by its name at a give position
in the sequent
|
Modifier and Type | Method and Description |
---|---|
void |
DefaultUserInterfaceControl.reportWarnings(ImmutableSet<PositionedString> warnings)
Report the occurred warnings.
|
boolean |
AbstractProofControl.selectedTaclet(ImmutableSet<TacletApp> applics,
Goal goal) |
Modifier and Type | Method and Description |
---|---|
void |
WindowUserInterfaceControl.reportWarnings(ImmutableSet<PositionedString> warnings) |
void |
ContractSelectionPanel.setContracts(ImmutableSet<Contract> contracts,
java.lang.String title) |
static void |
IssueDialog.showWarningsIfNecessary(java.awt.Window parent,
ImmutableSet<PositionedString> warnings)
Shows the dialog of a set of (non-critical) parser warnings.
|
Modifier and Type | Method and Description |
---|---|
ImmutableSet<Taclet> |
LemmataHandler.filter(java.util.List<TacletSoundnessPOLoader.TacletInfo> taclets) |
ImmutableSet<Taclet> |
LemmaSelectionDialog.filter(java.util.List<TacletSoundnessPOLoader.TacletInfo> taclets) |
ImmutableSet<Taclet> |
LemmaSelectionDialog.showModal(java.util.List<TacletSoundnessPOLoader.TacletInfo> taclets) |
Modifier and Type | Field and Description |
---|---|
protected ImmutableSet<QuantifiableVariable> |
ClashFreeSubst.svars |
Modifier and Type | Method and Description |
---|---|
ImmutableSet<QuantifiableVariable> |
TermImpl.freeVars() |
ImmutableSet<QuantifiableVariable> |
Term.freeVars()
The set of free quantifiable variables occurring in this term.
|
ImmutableSet<QuantifiableVariable> |
BoundVarsVisitor.getBoundVariables()
returns all the bound variables that have been stored
|
ImmutableSet<Term> |
TermBuilder.unionToSet(Term s) |
ImmutableSet<QuantifiableVariable> |
ClashFreeSubst.VariableCollectVisitor.vars()
the set of all occurring variables.
|
Modifier and Type | Method and Description |
---|---|
protected QuantifiableVariable |
ClashFreeSubst.newVarFor(QuantifiableVariable var,
ImmutableSet<QuantifiableVariable> usedVars)
returns a new variable that has a name derived from that of
var , that is different from any of the names of
variables in usedVars . |
boolean |
BoundVariableTools.resolveCollisions(ImmutableArray<QuantifiableVariable> oldVars,
QuantifiableVariable[] newVars,
ImmutableSet<QuantifiableVariable> criticalVars)
Replace all variables of
oldVars that also turn up in
criticalPairs with new variables (currently just with the
same name). |
boolean |
BoundVariableTools.resolveCollisions(Term originalTerm,
ImmutableSet<QuantifiableVariable> criticalVars,
ImmutableArray<QuantifiableVariable>[] newBoundVars,
Term[] newSubs,
TermServices services)
Ensure that none of the variables
criticalVars is bound by
the top-level operator of t (by bound renaming). |
<T extends E> |
Namespace.set(ImmutableSet<T> names) |
protected java.lang.Iterable<ProgramElementName> |
VariableNamer.wrapGlobals(ImmutableSet<ProgramVariable> globals)
creates a Globals object for use with other internal methods
|
Modifier and Type | Method and Description |
---|---|
ImmutableSet<Modality> |
ModalOperatorSV.getModalities()
returns an unmodifiable set of operators this schemavariable can match
|
Modifier and Type | Method and Description |
---|---|
static ModalOperatorSV |
SchemaVariableFactory.createModalOperatorSV(Name name,
Sort sort,
ImmutableSet<Modality> modalities)
creates a SchemaVariable representing an operator
|
Modifier and Type | Method and Description |
---|---|
ImmutableSet<Sort> |
NullSort.extendsSorts() |
ImmutableSet<Sort> |
AbstractSort.extendsSorts() |
ImmutableSet<Sort> |
Sort.extendsSorts() |
ImmutableSet<Sort> |
NullSort.extendsSorts(Services services) |
ImmutableSet<Sort> |
AbstractSort.extendsSorts(Services services) |
ImmutableSet<Sort> |
Sort.extendsSorts(Services services) |
ImmutableSet<Sort> |
GenericSort.getOneOf() |
Constructor and Description |
---|
AbstractSort(Name name,
ImmutableSet<Sort> ext,
boolean isAbstract) |
GenericSort(Name name,
ImmutableSet<Sort> ext,
ImmutableSet<Sort> oneOf)
creates a generic sort
|
GenericSort(Name name,
ImmutableSet<Sort> ext,
ImmutableSet<Sort> oneOf)
creates a generic sort
|
ProxySort(Name name,
ImmutableSet<Sort> ext) |
SortImpl(Name name,
ImmutableSet<Sort> ext) |
SortImpl(Name name,
ImmutableSet<Sort> ext,
boolean isAbstract) |
Modifier and Type | Method and Description |
---|---|
protected ImmutableSet<Modality> |
ExpressionBuilder.opSVHelper(java.lang.String opName,
ImmutableSet<Modality> modalities) |
ImmutableSet<SchemaVariable> |
TacletPBuilder.visitAddprogvar(KeYParser.AddprogvarContext ctx) |
Modifier and Type | Method and Description |
---|---|
protected ImmutableSet<Modality> |
ExpressionBuilder.opSVHelper(java.lang.String opName,
ImmutableSet<Modality> modalities) |
Modifier and Type | Method and Description |
---|---|
protected void |
LogicPrinter.printAddProgVars(ImmutableSet<SchemaVariable> apv) |
void |
LogicPrinter.printTerm(ImmutableSet<Term> terms)
Pretty-prints a set of terms.
|
Modifier and Type | Method and Description |
---|---|
ImmutableSet<java.net.URI> |
NodeInfo.getRelevantFiles()
Returns a set containing URIs of all files relevant to this node.
|
ImmutableSet<IProgramVariable> |
ProgVarReplacer.replace(ImmutableSet<IProgramVariable> vars)
replaces in a set
|
ImmutableSet<Term> |
OpReplacer.replace(ImmutableSet<Term> terms)
Replaces in a set of terms.
|
static ImmutableSet<NoPosTacletApp> |
TacletIndex.toNoPosTacletApp(java.lang.Iterable<Taclet> rule) |
Modifier and Type | Method and Description |
---|---|
void |
NodeInfo.addRelevantFiles(ImmutableSet<java.net.URI> relevantFiles)
Add some files to the set returned by
NodeInfo.getRelevantFiles() . |
ImmutableSet<IProgramVariable> |
ProgVarReplacer.replace(ImmutableSet<IProgramVariable> vars)
replaces in a set
|
ImmutableSet<Term> |
OpReplacer.replace(ImmutableSet<Term> terms)
Replaces in a set of terms.
|
Modifier and Type | Field and Description |
---|---|
protected ImmutableSet<NoPosTacletApp> |
AbstractPO.taclets |
Modifier and Type | Method and Description |
---|---|
protected ImmutableSet<GoalChooserBuilder> |
AbstractProfile.computeSupportedGoalChooserBuilder() |
ImmutableSet<Choice> |
InitConfig.getActivatedChoices()
Returns the choices which are currently active.
|
ImmutableSet<NoPosTacletApp> |
AbstractOperationPO.getInitialTaclets() |
protected ImmutableSet<StrategyFactory> |
JavaProfile.getStrategyFactories() |
protected ImmutableSet<StrategyFactory> |
AbstractProfile.getStrategyFactories() |
ImmutableSet<PositionedString> |
ProblemInitializer.getWarnings()
Returns the found warnings.
|
ImmutableSet<PositionedString> |
KeYUserProblemFile.read() |
protected ImmutableSet<ClassAxiom> |
WellDefinednessPO.selectClassAxioms(KeYJavaType kjt) |
protected ImmutableSet<ClassAxiom> |
AbstractPO.selectClassAxioms(KeYJavaType selfKJT) |
ImmutableSet<java.lang.String> |
Profile.supportedGoalChoosers()
returns the names of possible goalchoosers to be used by the
automatic prover environment
|
ImmutableSet<java.lang.String> |
AbstractProfile.supportedGoalChoosers()
returns the names of the supported goal chooser
builders
|
ImmutableSet<StrategyFactory> |
Profile.supportedStrategies()
returns the strategy factories for the supported strategies
|
ImmutableSet<StrategyFactory> |
AbstractProfile.supportedStrategies() |
Modifier and Type | Method and Description |
---|---|
void |
InitConfig.setActivatedChoices(ImmutableSet<Choice> activatedChoices)
sets the set of activated choices of this initial configuration.
|
Modifier and Type | Method and Description |
---|---|
ImmutableSet<PositionedString> |
LDTInput.read()
reads all LDTs, i.e., all associated .key files with respect to
the given modification strategy.
|
ImmutableSet<PositionedString> |
KeYFile.read() |
ImmutableSet<PositionedString> |
EnvInput.read()
Reads the input using the given modification strategy, i.e.,
parts of the input do not modify the initial configuration while
others do.
|
Modifier and Type | Method and Description |
---|---|
void |
ProblemLoaderControl.reportWarnings(ImmutableSet<PositionedString> warnings)
Report the occurred warnings.
|
Modifier and Type | Method and Description |
---|---|
ImmutableSet<Contract> |
SpecificationRepository.getAllContracts()
Returns all registered contracts.
|
ImmutableSet<Proof> |
SpecificationRepository.getAllProofs()
Returns all proofs registered with this specification repository.
|
ImmutableSet<WellDefinednessCheck> |
SpecificationRepository.getAllWdChecks()
Returns all registered well-definedness checks.
|
ImmutableSet<BlockContract> |
SpecificationRepository.getBlockContracts(StatementBlock block)
Returns all block contracts for the specified block.
|
ImmutableSet<BlockContract> |
SpecificationRepository.getBlockContracts(StatementBlock block,
Modality modality)
Returns block contracts for according block statement
and modality.
|
ImmutableSet<ClassAxiom> |
SpecificationRepository.getClassAxioms(KeYJavaType selfKjt)
Returns all class axioms visible in the passed class, including the
axioms induced by invariant declarations.
|
ImmutableSet<ClassInvariant> |
SpecificationRepository.getClassInvariants(KeYJavaType kjt)
Returns all known class invariants for the passed type.
|
ImmutableSet<Contract> |
SpecificationRepository.getContracts(KeYJavaType kjt,
IObserverFunction target)
Returns all registered (atomic) contracts for the passed target.
|
ImmutableSet<IObserverFunction> |
SpecificationRepository.getContractTargets(KeYJavaType kjt)
Returns all functions for which contracts are registered in the passed
type.
|
ImmutableSet<Contract> |
SpecificationRepository.getInheritedContracts(Contract contract)
Returns a set encompassing the passed contract and all its versions
inherited to overriding methods.
|
ImmutableSet<Contract> |
SpecificationRepository.getInheritedContracts(ImmutableSet<Contract> contractSet)
Returns a set encompassing the passed contracts and all its versions
inherited to overriding methods.
|
ImmutableSet<LoopContract> |
SpecificationRepository.getLoopContracts(LoopStatement loop)
Returns all loop contracts for the specified loop.
|
ImmutableSet<LoopContract> |
SpecificationRepository.getLoopContracts(LoopStatement loop,
Modality modality)
Returns loop contracts for according loop statement
and modality.
|
ImmutableSet<LoopContract> |
SpecificationRepository.getLoopContracts(StatementBlock block)
Returns all loop contracts for the specified block.
|
ImmutableSet<LoopContract> |
SpecificationRepository.getLoopContracts(StatementBlock block,
Modality modality) |
ImmutableSet<MergeContract> |
SpecificationRepository.getMergeContracts(MergePointStatement mps) |
ImmutableSet<FunctionalOperationContract> |
SpecificationRepository.getOperationContracts(KeYJavaType kjt,
IProgramMethod pm)
Returns all registered (atomic) operation contracts for the passed
operation.
|
ImmutableSet<FunctionalOperationContract> |
SpecificationRepository.getOperationContracts(KeYJavaType kjt,
IProgramMethod pm,
Modality modality)
Returns all registered (atomic) operation contracts for the passed
operation which refer to the passed modality.
|
ImmutableSet<Pair<KeYJavaType,IObserverFunction>> |
SpecificationRepository.getOverridingTargets(KeYJavaType kjt,
IObserverFunction target) |
ImmutableSet<Proof> |
SpecificationRepository.getProofs(Contract atomicContract)
Returns all proofs registered for the passed atomic contract, or for
combined contracts including the passed atomic contract
|
ImmutableSet<Proof> |
SpecificationRepository.getProofs(KeYJavaType kjt,
IObserverFunction target)
Returns all proofs registered for the passed target and its overriding
targets.
|
ImmutableSet<Proof> |
SpecificationRepository.getProofs(ProofOblInput po)
Returns all proofs registered for the passed PO (or stronger POs).
|
ImmutableSet<Contract> |
ProofCorrectnessMgt.getUsedContracts() |
ImmutableSet<Contract> |
SpecificationRepository.splitContract(Contract contract)
Splits the passed contract into its atomic components.
|
Modifier and Type | Method and Description |
---|---|
Pair<IObserverFunction,ImmutableSet<Taclet>> |
SpecificationRepository.limitObs(IObserverFunction obs) |
Modifier and Type | Method and Description |
---|---|
void |
SpecificationRepository.addClassAxioms(ImmutableSet<ClassAxiom> toAdd)
Registers the passed class axioms.
|
void |
SpecificationRepository.addClassInvariants(ImmutableSet<ClassInvariant> toAdd)
Registers the passed class invariants.
|
void |
SpecificationRepository.addContracts(ImmutableSet<Contract> toAdd)
Registers the passed contracts.
|
void |
SpecificationRepository.addInitiallyClauses(ImmutableSet<InitiallyClause> toAdd)
Registers the passed initially clauses.
|
void |
SpecificationRepository.addSpecs(ImmutableSet<SpecificationElement> specs) |
FunctionalOperationContract |
SpecificationRepository.combineOperationContracts(ImmutableSet<FunctionalOperationContract> toCombine)
Creates a combined contract out of the passed atomic contracts.
|
ImmutableSet<Contract> |
SpecificationRepository.getInheritedContracts(ImmutableSet<Contract> contractSet)
Returns a set encompassing the passed contracts and all its versions
inherited to overriding methods.
|
Modifier and Type | Field and Description |
---|---|
protected ImmutableSet<Choice> |
Taclet.choices
the set of taclet options for this taclet
|
ImmutableSet<Choice> |
RuleKey.choices |
protected ImmutableSet<LoopContract> |
LoopApplyHeadBuiltInRuleApp.contracts
The loop contracts on which the rule is applied.
|
protected ImmutableSet<TacletAnnotation> |
Taclet.tacletAnnotations |
Modifier and Type | Method and Description |
---|---|
protected static ImmutableSet<QuantifiableVariable> |
TacletApp.boundAtOccurrenceSet(TacletPrefix prefix,
SVInstantiations instantiations)
collects all bound variables above the occurrence of the schemavariable
whose prefix is given
|
protected static ImmutableSet<QuantifiableVariable> |
TacletApp.boundAtOccurrenceSet(TacletPrefix prefix,
SVInstantiations instantiations,
PosInOccurrence pos)
collects all bound variables above the occurrence of the schemavariable
whose prefix is given
|
protected ImmutableSet<SchemaVariable> |
TacletApp.calculateNonInstantiatedSV()
calculate needed SchemaVariables that have not been instantiated yet.
|
protected static ImmutableSet<QuantifiableVariable> |
TacletApp.collectBoundVarsAbove(PosInOccurrence pos)
collects all bound vars that are bound above the subterm described by the
given term position information
|
protected ImmutableSet<QuantifiableVariable> |
NoPosTacletApp.contextVars(SchemaVariable sv) |
protected ImmutableSet<QuantifiableVariable> |
PosTacletApp.contextVars(SchemaVariable sv) |
protected abstract ImmutableSet<QuantifiableVariable> |
TacletApp.contextVars(SchemaVariable sv) |
protected static ImmutableSet<BlockContract> |
AbstractBlockContractRule.filterAppliedContracts(ImmutableSet<BlockContract> collectedContracts,
Goal goal) |
protected static ImmutableSet<LoopContract> |
AbstractLoopContractRule.filterAppliedContracts(ImmutableSet<LoopContract> collectedContracts,
Goal goal) |
static ImmutableSet<BlockContract> |
AbstractBlockContractRule.getApplicableContracts(AbstractAuxiliaryContractRule.Instantiation instantiation,
Goal goal,
Services services) |
static ImmutableSet<LoopContract> |
AbstractLoopContractRule.getApplicableContracts(AbstractAuxiliaryContractRule.Instantiation instantiation,
Goal goal,
Services services) |
static ImmutableSet<Contract> |
UseDependencyContractRule.getApplicableContracts(Services services,
KeYJavaType kjt,
IObserverFunction target)
Returns the dependency contracts which are applicable for the passed
target.
|
static ImmutableSet<BlockContract> |
AbstractBlockContractRule.getApplicableContracts(SpecificationRepository specifications,
JavaStatement statement,
Modality modality,
Goal goal) |
static ImmutableSet<LoopContract> |
AbstractLoopContractRule.getApplicableContracts(SpecificationRepository specifications,
JavaStatement statement,
Modality modality,
Goal goal) |
static ImmutableSet<FunctionalOperationContract> |
UseOperationContractRule.getApplicableContracts(UseOperationContractRule.Instantiation inst,
Services services)
Returns the operation contracts which are applicable for the passed instantiation.
|
ImmutableSet<QuantifiableVariable> |
Taclet.getBoundVariables()
computes and returns all variables that occur bound in the taclet
including the taclets defined in addrules sections.
|
protected abstract ImmutableSet<QuantifiableVariable> |
Taclet.getBoundVariablesHelper()
collects bound variables in taclet entities others than goal templates
|
protected ImmutableSet<QuantifiableVariable> |
FindTaclet.getBoundVariablesHelper()
returns the variables that occur bound in the find part
|
protected ImmutableSet<QuantifiableVariable> |
NoFindTaclet.getBoundVariablesHelper()
the empty set as a no find taclet has no other entities where
variables cann occur bound than in the goal templates
|
ImmutableSet<Choice> |
Taclet.getChoices() |
abstract ImmutableSet<SchemaVariable> |
Taclet.getIfFindVariables() |
ImmutableSet<SchemaVariable> |
FindTaclet.getIfFindVariables() |
ImmutableSet<SchemaVariable> |
NoFindTaclet.getIfFindVariables() |
protected ImmutableSet<SchemaVariable> |
Taclet.getIfVariables()
returns the set of schemavariables of the taclet's if-part
|
ImmutableSet<Choice> |
Taclet.getTacletOptions() |
ImmutableSet<SchemaVariable> |
TacletPrefix.prefix()
returns the prefix
|
ImmutableSet<SchemaVariable> |
TacletApp.uninstantiatedVars()
returns the variables that have not yet been instantiated and need to be
instantiated to apply the Taclet.
|
Modifier and Type | Method and Description |
---|---|
Term |
AuxiliaryContractBuilders.ConditionsAndClausesBuilder.buildReachableCondition(ImmutableSet<ProgramVariable> variables) |
Term |
AuxiliaryContractBuilders.ConditionsAndClausesBuilder.buildReachableInCondition(ImmutableSet<ProgramVariable> localInVariables) |
Term |
AuxiliaryContractBuilders.ConditionsAndClausesBuilder.buildReachableOutCondition(ImmutableSet<ProgramVariable> localOutVariables) |
protected static AbstractLoopInvariantRule.AdditionalHeapTerms |
AbstractLoopInvariantRule.createAdditionalHeapTerms(Services services,
AbstractLoopInvariantRule.Instantiation inst,
java.util.List<LocationVariable> heapContext,
ImmutableSet<ProgramVariable> localOuts,
java.util.Map<LocationVariable,java.util.Map<Term,Term>> heapToBeforeLoop,
java.util.Map<LocationVariable,Term> atPres)
Prepare anon update, wellformed formula, frame condition and reachable
state formula.
|
protected static Term |
AbstractLoopInvariantRule.createBeforeLoopUpdate(Services services,
java.util.List<LocationVariable> heapContext,
ImmutableSet<ProgramVariable> localOuts,
java.util.Map<LocationVariable,java.util.Map<Term,Term>> heapToBeforeLoop)
Creates the "...Before_LOOP" update needed for the variant.
|
protected static Term |
AbstractAuxiliaryContractRule.createLocalAnonUpdate(ImmutableSet<ProgramVariable> localOuts,
Services services) |
protected static Term |
AbstractLoopInvariantRule.createLocalAnonUpdate(ImmutableSet<ProgramVariable> localOuts,
Services services)
Creates an update for the anonymization of all
ProgramVariable s
in localOuts. |
protected static ImmutableSet<BlockContract> |
AbstractBlockContractRule.filterAppliedContracts(ImmutableSet<BlockContract> collectedContracts,
Goal goal) |
protected static ImmutableSet<LoopContract> |
AbstractLoopContractRule.filterAppliedContracts(ImmutableSet<LoopContract> collectedContracts,
Goal goal) |
void |
Taclet.setTacletOptions(ImmutableSet<Choice> tacletOptions) |
protected AbstractBlockContractRule.InfFlowValidityData |
AbstractBlockContractRule.setUpInfFlowValidityGoal(Goal infFlowGoal,
BlockContract contract,
java.util.Map<LocationVariable,Function> anonymisationHeaps,
Services services,
AuxiliaryContract.Variables variables,
ProgramVariable exceptionParameter,
java.util.List<LocationVariable> heaps,
ImmutableSet<ProgramVariable> localInVariables,
ImmutableSet<ProgramVariable> localOutVariables,
BlockContractInternalBuiltInRuleApp application,
AbstractAuxiliaryContractRule.Instantiation instantiation) |
protected AbstractBlockContractRule.InfFlowValidityData |
AbstractBlockContractRule.setUpInfFlowValidityGoal(Goal infFlowGoal,
BlockContract contract,
java.util.Map<LocationVariable,Function> anonymisationHeaps,
Services services,
AuxiliaryContract.Variables variables,
ProgramVariable exceptionParameter,
java.util.List<LocationVariable> heaps,
ImmutableSet<ProgramVariable> localInVariables,
ImmutableSet<ProgramVariable> localOutVariables,
BlockContractInternalBuiltInRuleApp application,
AbstractAuxiliaryContractRule.Instantiation instantiation) |
Term |
AuxiliaryContractBuilders.GoalsConfigurator.setUpWdGoal(Goal goal,
BlockContract contract,
Term update,
Term anonUpdate,
LocationVariable heap,
Function anonHeap,
ImmutableSet<ProgramVariable> localIns) |
Constructor and Description |
---|
AntecTaclet(Name name,
TacletApplPart applPart,
ImmutableList<TacletGoalTemplate> goalTemplates,
ImmutableList<RuleSet> heuristics,
TacletAttributes attrs,
Term find,
boolean ignoreTopLevelUpdates,
ImmutableMap<SchemaVariable,TacletPrefix> prefixMap,
ImmutableSet<Choice> choices,
ImmutableSet<TacletAnnotation> tacletAnnotations)
creates a Schematic Theory Specific Rule (Taclet) with the given
parameters.
|
AntecTaclet(Name name,
TacletApplPart applPart,
ImmutableList<TacletGoalTemplate> goalTemplates,
ImmutableList<RuleSet> heuristics,
TacletAttributes attrs,
Term find,
boolean ignoreTopLevelUpdates,
ImmutableMap<SchemaVariable,TacletPrefix> prefixMap,
ImmutableSet<Choice> choices,
ImmutableSet<TacletAnnotation> tacletAnnotations)
creates a Schematic Theory Specific Rule (Taclet) with the given
parameters.
|
FindTaclet(Name name,
TacletApplPart applPart,
ImmutableList<TacletGoalTemplate> goalTemplates,
ImmutableList<RuleSet> ruleSets,
TacletAttributes attrs,
Term find,
ImmutableMap<SchemaVariable,TacletPrefix> prefixMap,
ImmutableSet<Choice> choices,
boolean surviveSymbExec,
ImmutableSet<TacletAnnotation> tacletAnnotations)
creates a FindTaclet
|
FindTaclet(Name name,
TacletApplPart applPart,
ImmutableList<TacletGoalTemplate> goalTemplates,
ImmutableList<RuleSet> ruleSets,
TacletAttributes attrs,
Term find,
ImmutableMap<SchemaVariable,TacletPrefix> prefixMap,
ImmutableSet<Choice> choices,
boolean surviveSymbExec,
ImmutableSet<TacletAnnotation> tacletAnnotations)
creates a FindTaclet
|
FindTaclet(Name name,
TacletApplPart applPart,
ImmutableList<TacletGoalTemplate> goalTemplates,
ImmutableList<RuleSet> ruleSets,
TacletAttributes attrs,
Term find,
ImmutableMap<SchemaVariable,TacletPrefix> prefixMap,
ImmutableSet<Choice> choices,
ImmutableSet<TacletAnnotation> tacletAnnotations)
creates a FindTaclet
|
FindTaclet(Name name,
TacletApplPart applPart,
ImmutableList<TacletGoalTemplate> goalTemplates,
ImmutableList<RuleSet> ruleSets,
TacletAttributes attrs,
Term find,
ImmutableMap<SchemaVariable,TacletPrefix> prefixMap,
ImmutableSet<Choice> choices,
ImmutableSet<TacletAnnotation> tacletAnnotations)
creates a FindTaclet
|
LoopApplyHeadBuiltInRuleApp(BuiltInRule rule,
PosInOccurrence pio,
ImmutableSet<LoopContract> contracts) |
NoFindTaclet(Name name,
TacletApplPart applPart,
ImmutableList<TacletGoalTemplate> goalTemplates,
ImmutableList<RuleSet> ruleSets,
TacletAttributes attrs,
ImmutableMap<SchemaVariable,TacletPrefix> prefixMap,
ImmutableSet<Choice> choices,
ImmutableSet<TacletAnnotation> tacletAnnotations)
creates a Schematic Theory Specific Rule (Taclet) with the given
parameters.
|
NoFindTaclet(Name name,
TacletApplPart applPart,
ImmutableList<TacletGoalTemplate> goalTemplates,
ImmutableList<RuleSet> ruleSets,
TacletAttributes attrs,
ImmutableMap<SchemaVariable,TacletPrefix> prefixMap,
ImmutableSet<Choice> choices,
ImmutableSet<TacletAnnotation> tacletAnnotations)
creates a Schematic Theory Specific Rule (Taclet) with the given
parameters.
|
RewriteTaclet(Name name,
TacletApplPart applPart,
ImmutableList<TacletGoalTemplate> goalTemplates,
ImmutableList<RuleSet> ruleSets,
TacletAttributes attrs,
Term find,
ImmutableMap<SchemaVariable,TacletPrefix> prefixMap,
int p_applicationRestriction,
ImmutableSet<Choice> choices,
boolean surviveSymbExec,
ImmutableSet<TacletAnnotation> tacletAnnotations) |
RewriteTaclet(Name name,
TacletApplPart applPart,
ImmutableList<TacletGoalTemplate> goalTemplates,
ImmutableList<RuleSet> ruleSets,
TacletAttributes attrs,
Term find,
ImmutableMap<SchemaVariable,TacletPrefix> prefixMap,
int p_applicationRestriction,
ImmutableSet<Choice> choices,
boolean surviveSymbExec,
ImmutableSet<TacletAnnotation> tacletAnnotations) |
RewriteTaclet(Name name,
TacletApplPart applPart,
ImmutableList<TacletGoalTemplate> goalTemplates,
ImmutableList<RuleSet> ruleSets,
TacletAttributes attrs,
Term find,
ImmutableMap<SchemaVariable,TacletPrefix> prefixMap,
int p_applicationRestriction,
ImmutableSet<Choice> choices,
ImmutableSet<TacletAnnotation> tacletAnnotations)
creates a Schematic Theory Specific Rule (Taclet) with the given
parameters that represents a rewrite rule.
|
RewriteTaclet(Name name,
TacletApplPart applPart,
ImmutableList<TacletGoalTemplate> goalTemplates,
ImmutableList<RuleSet> ruleSets,
TacletAttributes attrs,
Term find,
ImmutableMap<SchemaVariable,TacletPrefix> prefixMap,
int p_applicationRestriction,
ImmutableSet<Choice> choices,
ImmutableSet<TacletAnnotation> tacletAnnotations)
creates a Schematic Theory Specific Rule (Taclet) with the given
parameters that represents a rewrite rule.
|
SuccTaclet(Name name,
TacletApplPart applPart,
ImmutableList<TacletGoalTemplate> goalTemplates,
ImmutableList<RuleSet> heuristics,
TacletAttributes attrs,
Term find,
boolean ignoreTopLevelUpdates,
ImmutableMap<SchemaVariable,TacletPrefix> prefixMap,
ImmutableSet<Choice> choices,
ImmutableSet<TacletAnnotation> tacletAnnotations)
creates a Schematic Theory Specific Rule (Taclet) with the given
parameters that works on the succedent.
|
SuccTaclet(Name name,
TacletApplPart applPart,
ImmutableList<TacletGoalTemplate> goalTemplates,
ImmutableList<RuleSet> heuristics,
TacletAttributes attrs,
Term find,
boolean ignoreTopLevelUpdates,
ImmutableMap<SchemaVariable,TacletPrefix> prefixMap,
ImmutableSet<Choice> choices,
ImmutableSet<TacletAnnotation> tacletAnnotations)
creates a Schematic Theory Specific Rule (Taclet) with the given
parameters that works on the succedent.
|
Taclet(Name name,
TacletApplPart applPart,
ImmutableList<TacletGoalTemplate> goalTemplates,
ImmutableList<RuleSet> ruleSets,
TacletAttributes attrs,
ImmutableMap<SchemaVariable,TacletPrefix> prefixMap,
ImmutableSet<Choice> choices,
boolean surviveSmbExec,
ImmutableSet<TacletAnnotation> tacletAnnotations)
creates a Taclet (originally known as Schematic Theory Specific Rules)
|
Taclet(Name name,
TacletApplPart applPart,
ImmutableList<TacletGoalTemplate> goalTemplates,
ImmutableList<RuleSet> ruleSets,
TacletAttributes attrs,
ImmutableMap<SchemaVariable,TacletPrefix> prefixMap,
ImmutableSet<Choice> choices,
boolean surviveSmbExec,
ImmutableSet<TacletAnnotation> tacletAnnotations)
creates a Taclet (originally known as Schematic Theory Specific Rules)
|
Taclet(Name name,
TacletApplPart applPart,
ImmutableList<TacletGoalTemplate> goalTemplates,
ImmutableList<RuleSet> ruleSets,
TacletAttributes attrs,
ImmutableMap<SchemaVariable,TacletPrefix> prefixMap,
ImmutableSet<Choice> choices,
ImmutableSet<TacletAnnotation> tacletAnnotations)
creates a Schematic Theory Specific Rule (Taclet) with the given
parameters.
|
Taclet(Name name,
TacletApplPart applPart,
ImmutableList<TacletGoalTemplate> goalTemplates,
ImmutableList<RuleSet> ruleSets,
TacletAttributes attrs,
ImmutableMap<SchemaVariable,TacletPrefix> prefixMap,
ImmutableSet<Choice> choices,
ImmutableSet<TacletAnnotation> tacletAnnotations)
creates a Schematic Theory Specific Rule (Taclet) with the given
parameters.
|
TacletPrefix(ImmutableSet<SchemaVariable> prefix,
boolean context)
creates the prefix
|
Modifier and Type | Method and Description |
---|---|
protected void |
TacletExecutor.applyAddProgVars(ImmutableSet<SchemaVariable> pvs,
SequentChangeInfo currentSequent,
Goal goal,
PosInOccurrence posOfFind,
Services services,
MatchConditions matchCond) |
Modifier and Type | Method and Description |
---|---|
ImmutableSet<Term> |
MergeProcedure.ValuesMergeResult.getNewConstraints() |
Constructor and Description |
---|
ValuesMergeResult(ImmutableSet<Term> newConstraints,
Term mergeVal,
java.util.LinkedHashSet<Name> newNames,
java.util.LinkedHashSet<Term> sideConditions) |
Modifier and Type | Method and Description |
---|---|
void |
IntroAtPreDefsOp.updateBlockAndLoopContracts(ImmutableSet<? extends JavaStatement> statements,
java.util.Map<LocationVariable,LocationVariable> atPreVars,
java.util.Map<LocationVariable,LocationVariable> atPreHeapVars,
Services services)
Replace the placeholder variables
(see
AuxiliaryContract.getPlaceholderVariables() )
of all block contracts for blocks in blocks by
atPreVars and atPreHeapVars |
void |
IntroAtPreDefsOp.updateBlockAndLoopContracts(ImmutableSet<StatementBlock> blocks,
ImmutableSet<LoopStatement> loops,
java.util.Map<LocationVariable,LocationVariable> atPreVars,
java.util.Map<LocationVariable,LocationVariable> atPreHeapVars,
Services services)
Replace the placeholder variables
(see
AuxiliaryContract.getPlaceholderVariables() )
of all block contracts for blocks in blocks by
atPreVars and atPreHeapVars |
void |
IntroAtPreDefsOp.updateBlockAndLoopContracts(ImmutableSet<StatementBlock> blocks,
ImmutableSet<LoopStatement> loops,
java.util.Map<LocationVariable,LocationVariable> atPreVars,
java.util.Map<LocationVariable,LocationVariable> atPreHeapVars,
Services services)
Replace the placeholder variables
(see
AuxiliaryContract.getPlaceholderVariables() )
of all block contracts for blocks in blocks by
atPreVars and atPreHeapVars |
Modifier and Type | Field and Description |
---|---|
protected ImmutableSet<Choice> |
TacletBuilder.choices |
protected ImmutableSet<TacletAnnotation> |
TacletBuilder.tacletAnnotations |
Modifier and Type | Field and Description |
---|---|
protected java.util.HashMap<TacletGoalTemplate,ImmutableSet<Choice>> |
TacletBuilder.goal2Choices |
Modifier and Type | Method and Description |
---|---|
ImmutableSet<SchemaVariable> |
TacletGoalTemplate.addedProgVars()
returns the set of schemavaroable whose instantiations will be
added to the sequent namespace
|
ImmutableSet<Taclet> |
TacletGenerator.generateContractAxiomTaclets(Name name,
Term originalPre,
Term originalPost,
Term originalMby,
KeYJavaType kjt,
IObserverFunction target,
java.util.List<? extends ProgramVariable> heaps,
ProgramVariable originalSelfVar,
ProgramVariable originalResultVar,
java.util.Map<LocationVariable,ProgramVariable> atPreVars,
ImmutableList<ProgramVariable> originalParamVars,
ImmutableSet<Pair<Sort,IObserverFunction>> toLimit,
boolean satisfiabilityGuard,
TermServices services) |
ImmutableSet<Taclet> |
TacletGenerator.generateFunctionalRepresentsTaclets(Name name,
Term originalPreTerm,
Term originalRepresentsTerm,
KeYJavaType kjt,
IObserverFunction target,
java.util.List<? extends ProgramVariable> heaps,
ProgramVariable self,
ImmutableList<ProgramVariable> paramVars,
java.util.Map<LocationVariable,ProgramVariable> atPreVars,
ImmutableSet<Pair<Sort,IObserverFunction>> toLimit,
boolean satisfiability,
Services services) |
ImmutableSet<Taclet> |
TacletGenerator.generatePartialInvTaclet(Name name,
java.util.List<SchemaVariable> heapSVs,
SchemaVariable selfSV,
SchemaVariable eqSV,
Term term,
KeYJavaType kjt,
ImmutableSet<Pair<Sort,IObserverFunction>> toLimit,
boolean isStatic,
boolean eqVersion,
Services services) |
ImmutableSet<QuantifiableVariable> |
AntecSuccTacletGoalTemplate.getBoundVariables()
rertieves and returns all variables that are bound in the
goal template
|
ImmutableSet<QuantifiableVariable> |
RewriteTacletGoalTemplate.getBoundVariables()
rertieves and returns all variables that are bound in the
goal template
|
ImmutableSet<QuantifiableVariable> |
TacletGoalTemplate.getBoundVariables()
retrieves and returns all variables that are bound in the
goal template
|
ImmutableSet<Choice> |
TacletBuilder.getChoices() |
Modifier and Type | Method and Description |
---|---|
java.util.HashMap<TacletGoalTemplate,ImmutableSet<Choice>> |
TacletBuilder.getGoal2Choices() |
Modifier and Type | Method and Description |
---|---|
void |
TacletBuilder.addGoal2ChoicesMapping(TacletGoalTemplate gt,
ImmutableSet<Choice> soc)
adds a mapping from GoalTemplate
gt to SetOfsoc |
ImmutableSet<Taclet> |
TacletGenerator.generateContractAxiomTaclets(Name name,
Term originalPre,
Term originalPost,
Term originalMby,
KeYJavaType kjt,
IObserverFunction target,
java.util.List<? extends ProgramVariable> heaps,
ProgramVariable originalSelfVar,
ProgramVariable originalResultVar,
java.util.Map<LocationVariable,ProgramVariable> atPreVars,
ImmutableList<ProgramVariable> originalParamVars,
ImmutableSet<Pair<Sort,IObserverFunction>> toLimit,
boolean satisfiabilityGuard,
TermServices services) |
ImmutableSet<Taclet> |
TacletGenerator.generateFunctionalRepresentsTaclets(Name name,
Term originalPreTerm,
Term originalRepresentsTerm,
KeYJavaType kjt,
IObserverFunction target,
java.util.List<? extends ProgramVariable> heaps,
ProgramVariable self,
ImmutableList<ProgramVariable> paramVars,
java.util.Map<LocationVariable,ProgramVariable> atPreVars,
ImmutableSet<Pair<Sort,IObserverFunction>> toLimit,
boolean satisfiability,
Services services) |
ImmutableSet<Taclet> |
TacletGenerator.generatePartialInvTaclet(Name name,
java.util.List<SchemaVariable> heapSVs,
SchemaVariable selfSV,
SchemaVariable eqSV,
Term term,
KeYJavaType kjt,
ImmutableSet<Pair<Sort,IObserverFunction>> toLimit,
boolean isStatic,
boolean eqVersion,
Services services) |
T |
TacletBuilder.getTacletWithoutInactiveGoalTemplates(ImmutableSet<Choice> active) |
void |
TacletBuilder.setAnnotations(ImmutableSet<TacletAnnotation> tacletAnnotations) |
void |
TacletBuilder.setChoices(ImmutableSet<Choice> choices) |
Constructor and Description |
---|
AntecSuccTacletGoalTemplate(Sequent addedSeq,
ImmutableList<Taclet> addedRules,
Sequent replacewith,
ImmutableSet<SchemaVariable> pvs)
creates new Goaldescription
|
RewriteTacletGoalTemplate(Sequent addedSeq,
ImmutableList<Taclet> addedRules,
Term replacewith,
ImmutableSet<SchemaVariable> pvs)
creates new Goaldescription
|
TacletGoalTemplate(Sequent addedSeq,
ImmutableList<Taclet> addedRules,
ImmutableSet<SchemaVariable> addedProgVars)
creates new Goaldescription
|
Modifier and Type | Method and Description |
---|---|
ImmutableSet<Choice> |
ChoiceSettings.getDefaultChoicesAsSet()
returns the current selected choices as set
|
Modifier and Type | Method and Description |
---|---|
ImmutableSet<T> |
AbstractAuxiliaryContractImpl.Creator.create() |
static ImmutableSet<RewriteTaclet> |
ClassWellDefinedness.createInvTaclet(Services services)
Creates a well-definedness taclet for an invariant reference.
|
ImmutableSet<BlockContract> |
SpecExtractor.extractBlockContracts(IProgramMethod method,
LabeledStatement labeled)
Returns the block contracts for the passed labeled statement if it labels
a block.
|
ImmutableSet<BlockContract> |
SpecExtractor.extractBlockContracts(IProgramMethod method,
StatementBlock block)
Returns the block contracts for the passed block.
|
ImmutableSet<SpecificationElement> |
SpecExtractor.extractClassSpecs(KeYJavaType kjt)
Returns the class invariants for the passed type.
|
ImmutableSet<LoopContract> |
SpecExtractor.extractLoopContracts(IProgramMethod method,
LabeledStatement labeled)
Returns the loop contracts for the passed labeled statement if it labels
a block.
|
ImmutableSet<LoopContract> |
SpecExtractor.extractLoopContracts(IProgramMethod method,
LoopStatement loop)
Returns the loop contracts for the passed loop.
|
ImmutableSet<LoopContract> |
SpecExtractor.extractLoopContracts(IProgramMethod method,
StatementBlock block)
Returns the loop contracts for the passed block.
|
ImmutableSet<MergeContract> |
SpecExtractor.extractMergeContracts(IProgramMethod method,
MergePointStatement mps,
ImmutableList<ProgramVariable> methodParams)
Returns the
MergeContract s for the given
MergePointStatement . |
ImmutableSet<SpecificationElement> |
SpecExtractor.extractMethodSpecs(IProgramMethod pm)
Returns the operation contracts for the passed operation.
|
ImmutableSet<SpecificationElement> |
SpecExtractor.extractMethodSpecs(IProgramMethod pm,
boolean addInvariant) |
ImmutableSet<FunctionalAuxiliaryContract<?>> |
AbstractAuxiliaryContractImpl.getFunctionalContracts() |
ImmutableSet<FunctionalAuxiliaryContract<?>> |
AuxiliaryContract.getFunctionalContracts() |
abstract ImmutableSet<Taclet> |
ClassAxiom.getTaclets(ImmutableSet<Pair<Sort,IObserverFunction>> toLimit,
Services services)
The axiom as one or many taclets, where the non-defining occurrences of
the passed observers are replaced by their "limited" counterparts.
|
ImmutableSet<Taclet> |
ClassAxiomImpl.getTaclets(ImmutableSet<Pair<Sort,IObserverFunction>> toLimit,
Services services) |
ImmutableSet<Taclet> |
QueryAxiom.getTaclets(ImmutableSet<Pair<Sort,IObserverFunction>> toLimit,
Services services) |
ImmutableSet<Taclet> |
PartialInvAxiom.getTaclets(ImmutableSet<Pair<Sort,IObserverFunction>> toLimit,
Services services) |
ImmutableSet<Taclet> |
ContractAxiom.getTaclets(ImmutableSet<Pair<Sort,IObserverFunction>> toLimit,
Services services) |
ImmutableSet<Taclet> |
RepresentsAxiom.getTaclets(ImmutableSet<Pair<Sort,IObserverFunction>> toLimit,
Services services) |
ImmutableSet<Taclet> |
ModelMethodExecution.getTaclets(ImmutableSet<Pair<Sort,IObserverFunction>> toLimit,
Services services) |
abstract ImmutableSet<Pair<Sort,IObserverFunction>> |
ClassAxiom.getUsedObservers(Services services)
Returns the pairs (kjt, obs) for which there is an occurrence of
o.obs in the axiom, where kjt is the type of o (excluding the
defining occurrence of the axiom target).
|
ImmutableSet<Pair<Sort,IObserverFunction>> |
ClassAxiomImpl.getUsedObservers(Services services) |
ImmutableSet<Pair<Sort,IObserverFunction>> |
QueryAxiom.getUsedObservers(Services services) |
ImmutableSet<Pair<Sort,IObserverFunction>> |
PartialInvAxiom.getUsedObservers(Services services) |
ImmutableSet<Pair<Sort,IObserverFunction>> |
ContractAxiom.getUsedObservers(Services services) |
ImmutableSet<Pair<Sort,IObserverFunction>> |
RepresentsAxiom.getUsedObservers(Services services) |
ImmutableSet<Pair<Sort,IObserverFunction>> |
ModelMethodExecution.getUsedObservers(Services services) |
ImmutableSet<PositionedString> |
SLEnvInput.read() |
Modifier and Type | Method and Description |
---|---|
static BlockContract |
BlockContractImpl.combine(ImmutableSet<BlockContract> contracts,
Services services) |
static LoopContract |
LoopContractImpl.combine(ImmutableSet<LoopContract> contracts,
Services services) |
SequentFormula |
StatementWellDefinedness.generateSequent(ProgramVariable self,
LocationVariable heap,
Term anonHeap,
ImmutableSet<ProgramVariable> ps,
Term leadingUpdate,
Term localAnonUpdate,
Services services)
This is where the proof sequent is built, however with a smaller set of variables,
due to the nature of the jml statement.
|
SequentFormula |
StatementWellDefinedness.generateSequent(ProgramVariable self,
ProgramVariable exception,
ProgramVariable result,
LocationVariable heap,
ProgramVariable heapAtPre,
Term anonHeap,
ImmutableSet<ProgramVariable> ps,
Term leadingUpdate,
Term localAnonUpdate,
Services services)
This is where the proof sequent is built.
|
abstract ImmutableSet<Taclet> |
ClassAxiom.getTaclets(ImmutableSet<Pair<Sort,IObserverFunction>> toLimit,
Services services)
The axiom as one or many taclets, where the non-defining occurrences of
the passed observers are replaced by their "limited" counterparts.
|
ImmutableSet<Taclet> |
ClassAxiomImpl.getTaclets(ImmutableSet<Pair<Sort,IObserverFunction>> toLimit,
Services services) |
ImmutableSet<Taclet> |
QueryAxiom.getTaclets(ImmutableSet<Pair<Sort,IObserverFunction>> toLimit,
Services services) |
ImmutableSet<Taclet> |
PartialInvAxiom.getTaclets(ImmutableSet<Pair<Sort,IObserverFunction>> toLimit,
Services services) |
ImmutableSet<Taclet> |
ContractAxiom.getTaclets(ImmutableSet<Pair<Sort,IObserverFunction>> toLimit,
Services services) |
ImmutableSet<Taclet> |
RepresentsAxiom.getTaclets(ImmutableSet<Pair<Sort,IObserverFunction>> toLimit,
Services services) |
ImmutableSet<Taclet> |
ModelMethodExecution.getTaclets(ImmutableSet<Pair<Sort,IObserverFunction>> toLimit,
Services services) |
Constructor and Description |
---|
AbstractAuxiliaryContractImpl(java.lang.String baseName,
StatementBlock block,
java.util.List<Label> labels,
IProgramMethod method,
Modality modality,
java.util.Map<LocationVariable,Term> preconditions,
java.util.Map<LocationVariable,Term> freePreconditions,
Term measuredBy,
java.util.Map<LocationVariable,Term> postconditions,
java.util.Map<LocationVariable,Term> freePostconditions,
java.util.Map<LocationVariable,Term> modifiesClauses,
ImmutableList<InfFlowSpec> infFlowSpecs,
AuxiliaryContract.Variables variables,
boolean transactionApplicable,
java.util.Map<LocationVariable,java.lang.Boolean> hasMod,
ImmutableSet<FunctionalAuxiliaryContract<?>> functionalContracts) |
BlockContractImpl(java.lang.String baseName,
StatementBlock block,
java.util.List<Label> labels,
IProgramMethod method,
Modality modality,
java.util.Map<LocationVariable,Term> preconditions,
java.util.Map<LocationVariable,Term> freePreconditions,
Term measuredBy,
java.util.Map<LocationVariable,Term> postconditions,
java.util.Map<LocationVariable,Term> freePostconditions,
java.util.Map<LocationVariable,Term> modifiesClauses,
ImmutableList<InfFlowSpec> infFlowSpecs,
AuxiliaryContract.Variables variables,
boolean transactionApplicable,
java.util.Map<LocationVariable,java.lang.Boolean> hasMod,
ImmutableSet<FunctionalAuxiliaryContract<?>> functionalContracts) |
BlockWellDefinedness(BlockContract block,
AuxiliaryContract.Variables variables,
ImmutableSet<ProgramVariable> params,
Services services)
Creates a contract to check well-definedness of a block contract
|
LoopContractImpl(java.lang.String baseName,
LoopStatement loop,
java.util.List<Label> labels,
IProgramMethod method,
Modality modality,
java.util.Map<LocationVariable,Term> preconditions,
java.util.Map<LocationVariable,Term> freePreconditions,
Term measuredBy,
java.util.Map<LocationVariable,Term> postconditions,
java.util.Map<LocationVariable,Term> freePostconditions,
java.util.Map<LocationVariable,Term> modifiesClauses,
ImmutableList<InfFlowSpec> infFlowSpecs,
AuxiliaryContract.Variables variables,
boolean transactionApplicable,
java.util.Map<LocationVariable,java.lang.Boolean> hasMod,
Term decreases,
ImmutableSet<FunctionalAuxiliaryContract<?>> functionalContracts,
Services services)
Construct a loop contract for a loop.
|
LoopContractImpl(java.lang.String baseName,
StatementBlock block,
java.util.List<Label> labels,
IProgramMethod method,
Modality modality,
java.util.Map<LocationVariable,Term> preconditions,
java.util.Map<LocationVariable,Term> freePreconditions,
Term measuredBy,
java.util.Map<LocationVariable,Term> postconditions,
java.util.Map<LocationVariable,Term> freePostconditions,
java.util.Map<LocationVariable,Term> modifiesClauses,
ImmutableList<InfFlowSpec> infFlowSpecs,
AuxiliaryContract.Variables variables,
boolean transactionApplicable,
java.util.Map<LocationVariable,java.lang.Boolean> hasMod,
Term decreases,
ImmutableSet<FunctionalAuxiliaryContract<?>> functionalContracts,
Services services)
Construct a loop contract for a block that starts with a loop.
|
LoopWellDefinedness(LoopSpecification inv,
ImmutableSet<ProgramVariable> params,
Services services) |
Modifier and Type | Method and Description |
---|---|
static ImmutableSet<LabeledParserRuleContext> |
JMLSpecExtractor.createNonNullPositionedString(java.lang.String varName,
KeYJavaType kjt,
boolean isImplicitVar,
java.lang.String fileName,
Position pos,
Services services)
creates a JML specification expressing that the given variable/field is
not null and in case of a reference array type that also its elements are
non-null In case of implicit fields or primitive typed fields/variables
the empty set is returned
|
ImmutableSet<BlockContract> |
JMLSpecExtractor.extractBlockContracts(IProgramMethod method,
LabeledStatement labeled) |
ImmutableSet<BlockContract> |
JMLSpecExtractor.extractBlockContracts(IProgramMethod method,
StatementBlock block) |
ImmutableSet<SpecificationElement> |
JMLSpecExtractor.extractClassSpecs(KeYJavaType kjt) |
ImmutableSet<LoopContract> |
JMLSpecExtractor.extractLoopContracts(IProgramMethod method,
LabeledStatement labeled) |
ImmutableSet<LoopContract> |
JMLSpecExtractor.extractLoopContracts(IProgramMethod method,
LoopStatement loop) |
ImmutableSet<LoopContract> |
JMLSpecExtractor.extractLoopContracts(IProgramMethod method,
StatementBlock block) |
ImmutableSet<MergeContract> |
JMLSpecExtractor.extractMergeContracts(IProgramMethod method,
MergePointStatement mps,
ImmutableList<ProgramVariable> methodParams) |
ImmutableSet<SpecificationElement> |
JMLSpecExtractor.extractMethodSpecs(IProgramMethod pm) |
ImmutableSet<SpecificationElement> |
JMLSpecExtractor.extractMethodSpecs(IProgramMethod pm,
boolean addInvariant)
Extracts method specifications (i.e., contracts) from Java+JML input.
|
Modifier and Type | Method and Description |
---|---|
ImmutableSet<Contract> |
JMLSpecFactory.createFunctionalOperationContracts(java.lang.String name,
IProgramMethod pm,
ProgramVariableCollection progVars,
JMLSpecFactory.ContractClauses clauses,
java.util.Map<LocationVariable,Term> posts,
java.util.Map<LocationVariable,Term> axioms)
Generate functional operation contracts.
|
ImmutableSet<BlockContract> |
JMLSpecFactory.createJMLBlockContracts(IProgramMethod method,
java.util.List<Label> labels,
StatementBlock block,
TextualJMLSpecCase specificationCase)
Creates a set of block contracts for a block from a textual specification case.
|
ImmutableSet<LoopContract> |
JMLSpecFactory.createJMLLoopContracts(IProgramMethod method,
java.util.List<Label> labels,
LoopStatement loop,
TextualJMLSpecCase specificationCase)
Creates a set of loop contracts for a loop from a textual specification case.
|
ImmutableSet<LoopContract> |
JMLSpecFactory.createJMLLoopContracts(IProgramMethod method,
java.util.List<Label> labels,
StatementBlock block,
TextualJMLSpecCase specificationCase)
Creates a set of loop contracts for a block from a textual specification case.
|
ImmutableSet<MergeContract> |
JMLSpecFactory.createJMLMergeContracts(IProgramMethod method,
MergePointStatement mps,
TextualJMLMergePointDecl mergePointDecl,
ImmutableList<ProgramVariable> methodParams) |
ImmutableSet<Contract> |
JMLSpecFactory.createJMLOperationContracts(IProgramMethod pm,
TextualJMLSpecCase textualSpecCase)
Creates operation contracts out of the passed JML specification.
|
Modifier and Type | Method and Description |
---|---|
protected Sequent |
IsInRangeProvable.toSequent(ImmutableSet<Term> axioms,
Term toProve)
creates the sequent
axioms ==> toProve |
Modifier and Type | Method and Description |
---|---|
ImmutableSet<Trigger> |
TriggersSet.getAllTriggers() |
ImmutableSet<Substitution> |
Trigger.getSubstitutionsFromTerms(ImmutableSet<Term> targetTerm,
Services services) |
ImmutableSet<QuantifiableVariable> |
TriggersSet.getUniQuantifiedVariables() |
static ImmutableSet<Metavariable> |
EqualityConstraint.metaVars(Term t)
Deprecated.
|
Modifier and Type | Method and Description |
---|---|
static long |
PredictCostProver.computerInstanceCost(Substitution sub,
Term matrix,
ImmutableSet<Term> assertList,
Services services) |
ImmutableSet<Substitution> |
Trigger.getSubstitutionsFromTerms(ImmutableSet<Term> targetTerm,
Services services) |
boolean |
Substitution.isTotalOn(ImmutableSet<QuantifiableVariable> vars) |
Modifier and Type | Method and Description |
---|---|
protected ImmutableSet<Term> |
SymbolicLayoutExtractor.extractAppliedCutsSet(Node goalnode,
Node root)
Extracts the applied cut rules in the given
Node . |
Modifier and Type | Method and Description |
---|---|
protected java.util.List<ImmutableSet<Term>> |
SymbolicLayoutExtractor.extractAppliedCutsFromGoals(Proof proof)
Extracts the possible memory layouts from the given side proof.
|
Modifier and Type | Method and Description |
---|---|
protected ImmutableList<ISymbolicEquivalenceClass> |
SymbolicLayoutExtractor.lazyComputeEquivalenceClasses(ImmutableSet<Term> appliedCuts)
Computes the equivalence classes from the given applied cut rules
lazily when
SymbolicLayoutExtractor.getEquivalenceClasses(int) is called the first time. |
protected ISymbolicLayout |
SymbolicLayoutExtractor.lazyComputeLayout(ImmutableSet<Term> layout,
java.util.Set<AbstractUpdateExtractor.ExtractLocationParameter> locations,
ImmutableList<ISymbolicEquivalenceClass> equivalentClasses,
java.lang.String stateName,
boolean currentLayout)
Computes a memory layout lazily when it is first time requested via
#getLayout(Map, int, Term, Set, String, boolean) . |
Modifier and Type | Method and Description |
---|---|
protected ImmutableSet<GoalChooserBuilder> |
SymbolicExecutionJavaProfile.computeSupportedGoalChooserBuilder() |
protected ImmutableSet<StrategyFactory> |
SimplifyTermProfile.getStrategyFactories() |
protected ImmutableSet<StrategyFactory> |
SymbolicExecutionJavaProfile.getStrategyFactories() |
Modifier and Type | Method and Description |
---|---|
ImmutableList<TacletFormula> |
TacletSetTranslation.getTranslation(ImmutableSet<Sort> sorts)
Builds the translation of the taclets given by calling the method
setTacletSet() . |
ImmutableList<TacletFormula> |
DefaultTacletSetTranslation.getTranslation(ImmutableSet<Sort> sorts) |
TacletFormula |
AssumptionGenerator.translate(Taclet t,
ImmutableSet<Sort> sorts,
int maxGeneric) |
Modifier and Type | Method and Description |
---|---|
ImmutableSet<Taclet> |
TacletSoundnessPOLoader.TacletFilter.filter(java.util.List<TacletSoundnessPOLoader.TacletInfo> taclets) |
ImmutableSet<Taclet> |
TacletSoundnessPOLoader.getResultingTaclets() |
ImmutableSet<Taclet> |
TacletSoundnessPOLoader.getResultingTacletsForOriginalProof() |
abstract ImmutableSet<Taclet> |
TacletLoader.getTacletsAlreadyInUse()
get the taclet base which is considered fix (?)
|
ImmutableSet<Taclet> |
TacletLoader.TacletFromFileLoader.getTacletsAlreadyInUse() |
ImmutableSet<Taclet> |
TacletLoader.KeYsTacletsLoader.getTacletsAlreadyInUse() |
abstract ImmutableSet<Taclet> |
TacletLoader.loadAxioms()
get the set of axioms from the axiom files if applicable.
|
ImmutableSet<Taclet> |
TacletLoader.TacletFromFileLoader.loadAxioms() |
ImmutableSet<Taclet> |
TacletLoader.KeYsTacletsLoader.loadAxioms() |
ImmutableSet<PositionedString> |
EmptyEnvInput.read() |
Modifier and Type | Method and Description |
---|---|
ProofAggregate |
ProofObligationCreator.create(ImmutableSet<Taclet> taclets,
InitConfig[] initConfigs,
ImmutableSet<Taclet> axioms,
java.util.Collection<TacletSoundnessPOLoader.LoaderListener> listeners)
Creates for each taclet in
taclets a proof obligation
containing the corresponding FOL formula of the taclet. |
ProofAggregate |
ProofObligationCreator.create(ImmutableSet<Taclet> taclets,
InitConfig[] initConfigs,
ImmutableSet<Taclet> axioms,
java.util.Collection<TacletSoundnessPOLoader.LoaderListener> listeners)
Creates for each taclet in
taclets a proof obligation
containing the corresponding FOL formula of the taclet. |
void |
TacletSoundnessPOLoader.LoaderListener.stopped(ProofAggregate p,
ImmutableSet<Taclet> taclets,
boolean addAsAxioms) |
Constructor and Description |
---|
UserDefinedSymbols(NamespaceSet referenceNamespaces,
ImmutableSet<Taclet> axioms) |
Modifier and Type | Method and Description |
---|---|
void |
ConsoleUserInterfaceControl.reportWarnings(ImmutableSet<PositionedString> warnings)
Report the occurred warnings.
|
Modifier and Type | Method and Description |
---|---|
static ImmutableSet<Choice> |
SideProofUtil.activateChoice(ImmutableSet<Choice> choices,
Choice choiceToActivate)
removes all choices with the same category as
choiceToActivate from
choices and adds choiceToActivate to the set |
static ImmutableSet<Pair<Sort,IObserverFunction>> |
MiscTools.collectObservers(Term t)
Recursively collect all observers for this term including all of its sub terms.
|
static ImmutableSet<ProgramVariable> |
MiscTools.getLocalIns(ProgramElement pe,
Services services)
All variables read in the specified program element, excluding newly declared variables.
|
static ImmutableSet<ProgramVariable> |
MiscTools.getLocallyDeclaredVars(ProgramElement pe,
Services services)
All variables newly declared in the specified program element.
|
static ImmutableSet<ProgramVariable> |
MiscTools.getLocalOuts(ProgramElement pe,
Services services)
All variables changed in the specified program element, excluding newly declared variables.
|
static ImmutableSet<ProgramVariable> |
MiscTools.getLocalOutsAndDeclared(ProgramElement pe,
Services services)
All variables changed in the specified program element, including newly declared variables.
|
Modifier and Type | Method and Description |
---|---|
static ImmutableSet<Choice> |
SideProofUtil.activateChoice(ImmutableSet<Choice> choices,
Choice choiceToActivate)
removes all choices with the same category as
choiceToActivate from
choices and adds choiceToActivate to the set |
Modifier and Type | Method and Description |
---|---|
static ImmutableSet<LocationVariable> |
MergeRuleUtils.getLocationVariables(Term term,
Services services)
Returns all program variables in the given term.
|
static ImmutableSet<LocationVariable> |
MergeRuleUtils.getUpdateLeftSideLocations(Term u) |
Modifier and Type | Class and Description |
---|---|
class |
DefaultImmutableSet<T>
implementation of a persistent set using the SLListOf
|
Modifier and Type | Method and Description |
---|---|
default ImmutableSet<T> |
ImmutableSet.add(java.lang.Iterable<T> seq) |
ImmutableSet<T> |
ImmutableSet.add(T element)
Adds an element
|
ImmutableSet<T> |
DefaultImmutableSet.add(T element)
adds an element
|
ImmutableSet<T> |
ImmutableSet.addUnique(T element)
adds an element, barfs if the element is already present
|
ImmutableSet<T> |
DefaultImmutableSet.addUnique(T element)
adds an element, barfs if the element is already present
|
static <T> ImmutableSet<T> |
Immutables.createSetFrom(java.lang.Iterable<T> iterable) |
static <T> ImmutableSet<T> |
ImmutableSet.empty() |
static <T> ImmutableSet<T> |
ImmutableSet.fromCollection(java.util.Collection<? extends T> seq) |
static <T> ImmutableSet<T> |
DefaultImmutableSet.fromCollection(java.util.Collection<T> seq) |
static <T> ImmutableSet<T> |
DefaultImmutableSet.fromImmutableList(ImmutableList<T> list)
Create an immutable set from an immutable list.
|
static <T> ImmutableSet<T> |
ImmutableSet.fromSet(java.util.Set<T> set)
Creates an ImmutableSet from a Set.
|
static <T> ImmutableSet<T> |
DefaultImmutableSet.fromSet(java.util.Set<T> set)
Create an immutable set from a mutable set
|
ImmutableSet<T> |
ImmutableSet.intersect(ImmutableSet<? extends T> set) |
ImmutableSet<T> |
DefaultImmutableSet.intersect(ImmutableSet<? extends T> set) |
ImmutableSet<T> |
ImmutableSet.remove(T element) |
ImmutableSet<T> |
DefaultImmutableSet.remove(T element) |
static <T> ImmutableSet<T> |
ImmutableSet.singleton(T obj)
Builds a single set with the given obj.
|
ImmutableSet<T> |
ImmutableSet.union(ImmutableSet<? extends T> set) |
ImmutableSet<T> |
DefaultImmutableSet.union(ImmutableSet<? extends T> set) |
Modifier and Type | Method and Description |
---|---|
static <T> java.util.stream.Collector<T,java.util.Set<T>,ImmutableSet<T>> |
ImmutableSet.collector()
Returns a Collector that accumulates the input elements into a new ImmutableSet.
|
Modifier and Type | Method and Description |
---|---|
ImmutableSet<T> |
ImmutableSet.intersect(ImmutableSet<? extends T> set) |
ImmutableSet<T> |
DefaultImmutableSet.intersect(ImmutableSet<? extends T> set) |
boolean |
ImmutableSet.subset(ImmutableSet<T> s) |
boolean |
DefaultImmutableSet.subset(ImmutableSet<T> s) |
ImmutableSet<T> |
ImmutableSet.union(ImmutableSet<? extends T> set) |
ImmutableSet<T> |
DefaultImmutableSet.union(ImmutableSet<? extends T> set) |
Copyright © 2003-2019 The KeY-Project.