Modifier and Type | Method and Description |
---|---|
Services |
ProofManagementApi.getServices() |
Modifier and Type | Method and Description |
---|---|
void |
Matcher.parseDecls(java.lang.String s,
Services services)
Parse the declaration string for the current pattern and add the variables to the namespace
|
Modifier and Type | Method and Description |
---|---|
AbstractDomainElement |
AbstractDomainLattice.abstractFrom(SymbolicExecutionState state,
Term term,
Services services)
Abstracts from a given element of the concrete domain by returning a
suitable abstract element.
|
AbstractDomainElement |
AbstractDomainLattice.fromString(java.lang.String s,
Services services)
Constructs an Abstract Domain Element from the given String
representation.
|
abstract Term |
AbstractDomainElement.getDefiningAxiom(Term varOrConst,
Services services)
Return the defining axiom, instantiated for a given Term (skolem constant
or logical / program variable).
|
static Term |
AbstractDomainLattice.getSideConditionForAxiom(SymbolicExecutionState state,
Term term,
AbstractDomainElement elem,
Services services)
Returns a side condition which has to hold if elem is a correct
abstraction for term.
|
abstract java.lang.String |
AbstractDomainElement.toParseableString(Services services)
Returns a parseable String representation of this
AbstractDomainElement . |
Modifier and Type | Method and Description |
---|---|
Term |
Top.getDefiningAxiom(Term varOrConst,
Services services) |
Term |
False.getDefiningAxiom(Term varOrConst,
Services services) |
Term |
True.getDefiningAxiom(Term varOrConst,
Services services) |
Term |
Bottom.getDefiningAxiom(Term varOrConst,
Services services) |
java.lang.String |
Top.toParseableString(Services services) |
java.lang.String |
False.toParseableString(Services services) |
java.lang.String |
True.toParseableString(Services services) |
java.lang.String |
Bottom.toParseableString(Services services) |
Modifier and Type | Method and Description |
---|---|
protected Term |
DisjunctivePredicateAbstractionDomainElement.combinePredicates(Term preds,
Term newPred,
Services services) |
protected abstract Term |
AbstractPredicateAbstractionDomainElement.combinePredicates(Term preds,
Term newPred,
Services services)
Combines the given predicate terms (classically using AND or OR).
|
protected Term |
ConjunctivePredicateAbstractionDomainElement.combinePredicates(Term preds,
Term newPred,
Services services) |
protected Term |
SimplePredicateAbstractionDomainElement.combinePredicates(Term preds,
Term newPred,
Services services) |
static AbstractionPredicate |
AbstractionPredicate.create(Sort argSort,
java.util.function.Function<Term,Term> mapping,
Services services)
Creates a new
AbstractionPredicate with the given name and
mapping. |
static AbstractionPredicate |
AbstractionPredicate.create(Term predicate,
LocationVariable placeholder,
Services services)
Creates a new
AbstractionPredicate for the given predicate. |
static java.util.List<AbstractionPredicate> |
AbstractionPredicate.fromString(java.lang.String s,
Services services,
NamespaceSet localNamespaces)
Parses the String representation of an abstraction predicates.
|
Term |
AbstractPredicateAbstractionDomainElement.getDefiningAxiom(Term varOrConst,
Services services) |
java.lang.String |
AbstractionPredicate.toParseableString(Services services)
Returns a parseable String representation of this abstraction predicate
of the form "('[[TYPE]] [[PLACEHOLDER]]', '[[PREDICATE]]')".
|
java.lang.String |
AbstractPredicateAbstractionDomainElement.toParseableString(Services services) |
Modifier and Type | Method and Description |
---|---|
Term |
Top.getDefiningAxiom(Term varOrConst,
Services services) |
Term |
Geq.getDefiningAxiom(Term varOrConst,
Services services) |
Term |
Neg.getDefiningAxiom(Term varOrConst,
Services services) |
Term |
Zero.getDefiningAxiom(Term varOrConst,
Services services) |
Term |
Pos.getDefiningAxiom(Term varOrConst,
Services services) |
Term |
Bottom.getDefiningAxiom(Term varOrConst,
Services services) |
Term |
Leq.getDefiningAxiom(Term varOrConst,
Services services) |
java.lang.String |
Top.toParseableString(Services services) |
java.lang.String |
Geq.toParseableString(Services services) |
java.lang.String |
Neg.toParseableString(Services services) |
java.lang.String |
Zero.toParseableString(Services services) |
java.lang.String |
Pos.toParseableString(Services services) |
java.lang.String |
Bottom.toParseableString(Services services) |
java.lang.String |
Leq.toParseableString(Services services) |
Modifier and Type | Method and Description |
---|---|
Services |
KeYEnvironment.getServices()
Returns the
Services of KeYEnvironment.getInitConfig() . |
Modifier and Type | Method and Description |
---|---|
Services |
TacletInstantiationModel.getServices()
Gets the services in use by this object.
|
Constructor and Description |
---|
TacletAssumesModel(Term ifFma,
ImmutableList<IfFormulaInstantiation> candidates,
TacletApp app,
Goal goal,
Services services,
NamespaceSet nss,
AbbrevMap scm) |
TacletFindModel(TacletApp app,
Services services,
NamespaceSet nss,
AbbrevMap scm,
Goal goal)
Create new data model for tree.
|
Modifier and Type | Method and Description |
---|---|
Services |
KeYMediator.getServices()
returns the Services with the java service classes
|
Modifier and Type | Field and Description |
---|---|
protected Services |
AuxiliaryContractSelectionPanel.services |
Modifier and Type | Method and Description |
---|---|
static BlockContract |
BlockContractSelectionPanel.computeBlockContract(Services services,
java.util.List<BlockContract> selection)
The static access is used e.g.
|
BlockContract |
BlockContractSelectionPanel.computeContract(Services services,
java.util.List<BlockContract> selection)
Computes the selected
BlockContract . |
static Contract |
ContractSelectionPanel.computeContract(Services services,
java.util.List<Contract> selection)
Computes the selected
Contract . |
LoopContract |
LoopContractSelectionPanel.computeContract(Services services,
java.util.List<LoopContract> selection) |
abstract T |
AuxiliaryContractSelectionPanel.computeContract(Services services2,
java.util.List<T> selection) |
static java.lang.String |
ClassTree.getDisplayName(Services services,
IObserverFunction ov)
Returns a human readable display name for the given
ObserverFunction
with use of the given Services . |
LoopSpecification |
InvariantConfigurator.getLoopInvariant(LoopSpecification loopInv,
Services services,
boolean requiresVariant,
java.util.List<LocationVariable> heapContext)
Creates a Dialog.
|
static Term |
InspectorForDecisionPredicates.translate(Services services,
java.lang.String toBeChecked) |
Constructor and Description |
---|
AuxiliaryContractConfigurator(java.lang.String name,
AuxiliaryContractSelectionPanel<T> contractPanel,
java.awt.Frame owner,
Services services,
T[] contracts,
java.lang.String title) |
AuxiliaryContractConfigurator(java.lang.String name,
AuxiliaryContractSelectionPanel<T> contractPanel,
javax.swing.JDialog owner,
Services services,
T[] contracts,
java.lang.String title) |
AuxiliaryContractSelectionPanel(Services services,
boolean multipleSelection) |
BlockContractSelectionPanel(Services services,
boolean multipleSelection) |
ClassTree(boolean addContractTargets,
boolean skipLibraryClasses,
Services services) |
ClassTree(boolean addContractTargets,
boolean skipLibraryClasses,
Services services,
java.util.Map<Pair<KeYJavaType,IObserverFunction>,javax.swing.Icon> targetIcons) |
ContractConfigurator(java.awt.Frame owner,
Services services,
Contract[] contracts,
java.lang.String title,
boolean allowMultipleContracts) |
ContractConfigurator(javax.swing.JDialog owner,
Services services,
Contract[] contracts,
java.lang.String title,
boolean allowMultipleContracts) |
ContractSelectionPanel(Services services,
boolean multipleSelection)
Creates a contract selection panel containing the specified contracts.
|
InspectorForDecisionPredicates(Services services,
Node node,
int cutMode,
java.util.List<ApplicationCheck> additionalChecks) |
LoopContractSelectionPanel(Services services,
boolean multipleSelection) |
Modifier and Type | Method and Description |
---|---|
void |
SequentViewer.setSequent(Sequent sequent,
Services services) |
Constructor and Description |
---|
JoinDialog(java.util.List<ProspectivePartner> partnerList,
Proof proof,
PredicateEstimator estimator,
Services services) |
Constructor and Description |
---|
MergePartnerSelectionDialog(Goal mergeGoal,
PosInOccurrence pio,
ImmutableList<MergePartner> candidates,
Services services)
Creates a new merge partner selection dialog.
|
Modifier and Type | Field and Description |
---|---|
protected Services |
InsertionTacletBrowserMenuItem.services
the services
|
Constructor and Description |
---|
InsertHiddenTacletMenuItem(javax.swing.JFrame parent,
NotationInfo notInfo,
Services services)
creates an instance of the insert hidden menu item
|
InsertionTacletBrowserMenuItem(java.lang.String title,
javax.swing.JFrame parent,
NotationInfo notInfo,
Services services) |
InsertSystemInvariantTacletMenuItem(javax.swing.JFrame parent,
NotationInfo notInfo,
Services services)
creates an instance of the insert hidden menu item
|
PosInSequentTransferable(PosInSequent pis,
Services serv)
creates an instance of this transferable
|
SimpleTacletSelectionMenu(ImmutableList<PosTacletApp> apps,
NotationInfo info,
java.awt.event.ActionListener listener,
Services services)
creates an instance of this menu displaying the applications stored in
apps
|
Constructor and Description |
---|
OriginTermLabelVisualizer(PosInOccurrence pos,
Node node,
Services services)
Creates a new
OriginTermLabelVisualizer . |
Modifier and Type | Method and Description |
---|---|
Services |
ProofDifferenceView.getServices() |
Modifier and Type | Method and Description |
---|---|
static ProofDifference |
ProofDifference.create(Services services,
Node left,
Node right) |
Modifier and Type | Method and Description |
---|---|
static Term |
InspectorForFormulas.translate(Services services,
java.lang.String toBeChecked) |
Constructor and Description |
---|
InspectorForFormulas(Services services) |
Modifier and Type | Method and Description |
---|---|
protected Term |
LoopInvExecutionPO.buildFrameClause(java.util.List<LocationVariable> modHeaps,
java.util.Map<Term,Term> heapToAtPre,
ProgramVariable selfVar,
ImmutableList<ProgramVariable> paramVars,
Services services)
Deprecated.
|
protected Term |
InfFlowContractPO.buildFrameClause(java.util.List<LocationVariable> modHeaps,
java.util.Map<Term,Term> heapToAtPre,
ProgramVariable selfVar,
ImmutableList<ProgramVariable> paramVars,
Services services)
Deprecated.
|
protected Term |
BlockExecutionPO.buildFrameClause(java.util.List<LocationVariable> modHeaps,
java.util.Map<Term,Term> heapToAtPre,
ProgramVariable selfVar,
ImmutableList<ProgramVariable> paramVars,
Services services)
Deprecated.
|
protected Term |
SymbolicExecutionPO.buildFrameClause(java.util.List<LocationVariable> modHeaps,
java.util.Map<Term,Term> heapToAtPre,
ProgramVariable selfVar,
ImmutableList<ProgramVariable> paramVars,
Services services)
Deprecated.
|
protected ImmutableList<StatementBlock> |
LoopInvExecutionPO.buildOperationBlocks(ImmutableList<LocationVariable> formalParVars,
ProgramVariable selfVar,
ProgramVariable resultVar,
Services services)
Deprecated.
|
protected ImmutableList<StatementBlock> |
InfFlowContractPO.buildOperationBlocks(ImmutableList<LocationVariable> formalParVars,
ProgramVariable selfVar,
ProgramVariable resultVar,
Services services)
Deprecated.
|
protected ImmutableList<StatementBlock> |
BlockExecutionPO.buildOperationBlocks(ImmutableList<LocationVariable> formalParVars,
ProgramVariable selfVar,
ProgramVariable resultVar,
Services services)
Deprecated.
|
protected ImmutableList<StatementBlock> |
SymbolicExecutionPO.buildOperationBlocks(ImmutableList<LocationVariable> formalParVars,
ProgramVariable selfVar,
ProgramVariable resultVar,
Services services)
Deprecated.
|
protected Term |
LoopInvExecutionPO.generateMbyAtPreDef(ProgramVariable selfVar,
ImmutableList<ProgramVariable> paramVars,
Services services)
Deprecated.
|
protected Term |
InfFlowContractPO.generateMbyAtPreDef(ProgramVariable selfVar,
ImmutableList<ProgramVariable> paramVars,
Services services)
Deprecated.
|
protected Term |
BlockExecutionPO.generateMbyAtPreDef(ProgramVariable selfVar,
ImmutableList<ProgramVariable> paramVars,
Services services)
Deprecated.
|
protected Term |
SymbolicExecutionPO.generateMbyAtPreDef(ProgramVariable selfVar,
ImmutableList<ProgramVariable> paramVars,
Services services)
Deprecated.
|
protected Term |
LoopInvExecutionPO.getGlobalDefs(LocationVariable heap,
Term heapTerm,
Term selfTerm,
ImmutableList<Term> paramTerms,
Services services) |
protected Term |
InfFlowContractPO.getGlobalDefs(LocationVariable heap,
Term heapTerm,
Term selfTerm,
ImmutableList<Term> paramTerms,
Services services) |
protected Term |
BlockExecutionPO.getGlobalDefs(LocationVariable heap,
Term heapTerm,
Term selfTerm,
ImmutableList<Term> paramTerms,
Services services) |
protected Term |
SymbolicExecutionPO.getGlobalDefs(LocationVariable heap,
Term heapTerm,
Term selfTerm,
ImmutableList<Term> paramTerms,
Services services) |
protected Term |
LoopInvExecutionPO.getPost(java.util.List<LocationVariable> modHeaps,
ProgramVariable selfVar,
ImmutableList<ProgramVariable> paramVars,
ProgramVariable resultVar,
ProgramVariable exceptionVar,
java.util.Map<LocationVariable,LocationVariable> atPreVars,
Services services)
Deprecated.
|
protected Term |
InfFlowContractPO.getPost(java.util.List<LocationVariable> modHeaps,
ProgramVariable selfVar,
ImmutableList<ProgramVariable> paramVars,
ProgramVariable resultVar,
ProgramVariable exceptionVar,
java.util.Map<LocationVariable,LocationVariable> atPreVars,
Services services)
Deprecated.
|
protected Term |
BlockExecutionPO.getPost(java.util.List<LocationVariable> modHeaps,
ProgramVariable selfVar,
ImmutableList<ProgramVariable> paramVars,
ProgramVariable resultVar,
ProgramVariable exceptionVar,
java.util.Map<LocationVariable,LocationVariable> atPreVars,
Services services)
Deprecated.
|
protected Term |
SymbolicExecutionPO.getPost(java.util.List<LocationVariable> modHeaps,
ProgramVariable selfVar,
ImmutableList<ProgramVariable> paramVars,
ProgramVariable resultVar,
ProgramVariable exceptionVar,
java.util.Map<LocationVariable,LocationVariable> atPreVars,
Services services)
Deprecated.
|
protected Term |
LoopInvExecutionPO.getPre(java.util.List<LocationVariable> modHeaps,
ProgramVariable selfVar,
ImmutableList<ProgramVariable> paramVars,
java.util.Map<LocationVariable,LocationVariable> atPreVars,
Services services)
Deprecated.
|
protected Term |
InfFlowContractPO.getPre(java.util.List<LocationVariable> modHeaps,
ProgramVariable selfVar,
ImmutableList<ProgramVariable> paramVars,
java.util.Map<LocationVariable,LocationVariable> atPreVars,
Services services)
Deprecated.
|
protected Term |
BlockExecutionPO.getPre(java.util.List<LocationVariable> modHeaps,
ProgramVariable selfVar,
ImmutableList<ProgramVariable> paramVars,
java.util.Map<LocationVariable,LocationVariable> atPreVars,
Services services)
Deprecated.
|
protected Term |
SymbolicExecutionPO.getPre(java.util.List<LocationVariable> modHeaps,
ProgramVariable selfVar,
ImmutableList<ProgramVariable> paramVars,
java.util.Map<LocationVariable,LocationVariable> atPreVars,
Services services)
Deprecated.
|
static ProgramVariable |
InfFlowProofSymbols.searchPV(java.lang.String s,
Services services) |
Constructor and Description |
---|
BlockExecutionPO(InitConfig initConfig,
BlockContract contract,
ProofObligationVars symbExecVars,
Goal initiatingGoal,
ExecutionContext context,
Services services)
To be used only for auxiliary proofs where the services object of
the actual proof has to be used instead of the initial services form
the InitConfig.
|
IFProofObligationVars(ProofObligationVars symbExecVars,
Services services) |
LoopInvExecutionPO(InitConfig initConfig,
LoopSpecification loopInv,
ProofObligationVars symbExecVars,
Goal initiatingGoal,
ExecutionContext context,
Term guardTerm,
Services services)
To be used only for auxiliary proofs where the services object of
the actual proof has to be used instead of the initial services form
the InitConfig.
|
SymbolicExecutionPO(InitConfig initConfig,
InformationFlowContract contract,
ProofObligationVars symbExecVars,
Goal initiatingGoal,
Services services)
To be used only for auxiliary proofs where the services object of
the actual proof has to be used instead of the initial services form
the InitConfig.
|
Modifier and Type | Method and Description |
---|---|
static StateVars |
StateVars.buildInfFlowPostVars(StateVars origPreVars,
StateVars origPostVars,
StateVars preVars,
java.lang.String postfix,
Services services) |
static StateVars |
StateVars.buildInfFlowPreVars(StateVars origPreVars,
java.lang.String postfix,
Services services) |
static StateVars |
StateVars.buildMethodContractPostVars(StateVars preVars,
IProgramMethod pm,
KeYJavaType kjt,
Services services) |
static StateVars |
StateVars.buildMethodContractPreVars(IProgramMethod pm,
KeYJavaType kjt,
Services services) |
Constructor and Description |
---|
StateVars(StateVars orig,
java.lang.String postfix,
Services services) |
Modifier and Type | Method and Description |
---|---|
protected void |
InfFlowContractAppTacletExecutor.addToAntec(Semisequent semi,
TermLabelState termLabelState,
Taclet.TacletLabelHint labelHint,
SequentChangeInfo currentSequent,
PosInOccurrence pos,
PosInOccurrence applicationPosInOccurrence,
MatchConditions matchCond,
Goal goal,
RuleApp tacletApp,
Services services) |
Constructor and Description |
---|
BlockInfFlowUnfoldTacletBuilder(Services services) |
InfFlowBlockContractTacletBuilder(Services services) |
InfFlowLoopInvariantTacletBuilder(Services services) |
InfFlowMethodContractTacletBuilder(Services services) |
LoopInfFlowUnfoldTacletBuilder(Services services) |
MethodInfFlowUnfoldTacletBuilder(Services services) |
Modifier and Type | Field and Description |
---|---|
protected Services |
JavaInfo.services |
Modifier and Type | Method and Description |
---|---|
Services |
Services.copy(boolean shareCaches)
creates a new services object containing a copy of the java info of
this object and a new TypeConverter (shallow copy)
The copy does not belong to a
Proof object and can hence be used for a new proof. |
Services |
Services.copy(Profile profile,
boolean shareCaches)
|
Services |
Services.copyPreservesLDTInformation()
creates a new service object with the same ldt information
as the actual one
|
Services |
Services.copyProofSpecific(Proof p_proof,
boolean shareCaches) |
Services |
Services.getOverlay(NamespaceSet namespaces) |
Services |
JavaInfo.getServices()
returns the services associated with this JavaInfo
|
Services |
SourceData.getServices()
returns the services object
|
Services |
ConstantExpressionEvaluator.getServices() |
Services |
Services.shallowCopy()
Generate a copy of this object.
|
Modifier and Type | Method and Description |
---|---|
JavaInfo |
JavaInfo.copy(Services serv)
copies this JavaInfo and uses the given Services object as the
Services object of the copied JavaInfo
|
TypeConverter |
TypeConverter.copy(Services services) |
TermProgramVariableCollector |
Services.ITermProgramVariableCollectorFactory.create(Services services) |
static LocalVariableDeclaration |
KeYJavaASTFactory.declare(Services services,
java.lang.String name,
Expression initializer,
KeYJavaType type)
Create a local variable declaration with a unique name.
|
static FieldReference |
KeYJavaASTFactory.fieldReference(Services services,
java.lang.String name,
Expression expression,
ExecutionContext context)
Create a field access.
|
static ExecutionContext |
JavaTools.getInnermostExecutionContext(JavaBlock jb,
Services services) |
static MethodFrame |
JavaTools.getInnermostMethodFrame(JavaBlock jb,
Services services)
Returns the innermost method frame of the passed java block
|
static MethodFrame |
JavaTools.getInnermostMethodFrame(ProgramElement pe,
Services services)
Returns the innermost method frame of the passed java block
|
KeYJavaType |
Expression.getKeYJavaType(Services javaServ,
ExecutionContext ec)
returns the
KeYJavaType of an expression |
static ProgramVariable |
KeYJavaASTFactory.localVariable(Services services,
java.lang.String name,
KeYJavaType type)
Create a local variable with a unique name.
|
protected Recoder2KeYConverter |
Recoder2KeY.makeConverter(Services services,
NamespaceSet nss)
create the ast converter.
|
protected Recoder2KeYConverter |
SchemaRecoder2KeY.makeConverter(Services services,
NamespaceSet nss) |
static JavaBlock |
JavaTools.removeActiveStatement(JavaBlock jb,
Services services)
Returns the passed java block without its active statement.
|
java.lang.String |
JavaProgramElement.reuseSignature(Services services,
ExecutionContext ec)
this is the default implementation of the signature, which is
used to determine program similarity.
|
Constructor and Description |
---|
JavaInfo(JavaInfo proto,
Services s) |
JavaInfo(KeYProgModelInfo kpmi,
Services s)
creates a new JavaInfo object by giving a KeYProgModelInfo to access
the Recoder SourceInfo and using the given
Services object. |
KeYProgModelInfo(Services services,
TypeConverter typeConverter,
KeYRecoderExcHandler keh) |
Recoder2KeY(Services services,
KeYCrossReferenceServiceConfiguration servConf,
KeYRecoderMapping rec2key,
NamespaceSet nss,
TypeConverter tc)
create a new Recoder2KeY transformation object.
|
Recoder2KeY(Services services,
NamespaceSet nss)
create a new Recoder2KeY transformation object.
|
Recoder2KeYConverter(Recoder2KeY rec2key,
Services services,
NamespaceSet nss) |
Recoder2KeYTypeConverter(Services services,
TypeConverter typeConverter,
NamespaceSet namespaces,
Recoder2KeY recoder2key) |
SchemaRecoder2KeY(Services services,
NamespaceSet nss) |
SchemaRecoder2KeYConverter(SchemaRecoder2KeY rec2key,
Services services,
NamespaceSet namespaceSet)
create a new schema-recoder-to-key converter.
|
SourceData(ProgramElement element,
int childPos,
Services services)
creates a new source data object with parent node element whose
childPos-th child has to be matched (-1 denotes element itself
has to be matched
|
Modifier and Type | Method and Description |
---|---|
ImmutableList<Field> |
NullType.getAllFields(Services services)
Returns all visible fields that are defined in this class type
or any of its supertypes.
|
ImmutableList<Field> |
ClassType.getAllFields(Services services)
Returns all visible fields that are defined in this class type
or any of its supertypes.
|
ImmutableList<Method> |
NullType.getAllMethods(Services services)
Returns all visible methods that are defined in this class type
or any of its supertypes.
|
ImmutableList<Method> |
ClassType.getAllMethods(Services services)
Returns all visible methods that are defined in this class type
or any of its supertypes.
|
ImmutableList<ClassType> |
NullType.getAllSupertypes(Services services)
Returns the array of all supertypes of this class type,
in topological order, including the class type isself as first element.
|
ImmutableList<ClassType> |
ClassType.getAllSupertypes(Services services)
Returns the array of all supertypes of this class type,
in topological order, including the class type isself as first element.
|
ImmutableList<ClassType> |
NullType.getAllTypes(Services services)
Returns all class types that are inner types of this class type,
including visible inherited types.
|
ImmutableList<ClassType> |
ClassType.getAllTypes(Services services)
Returns all class types that are inner types of this class type,
including visible inherited types.
|
ImmutableList<Constructor> |
NullType.getConstructors(Services services)
Returns the constructors locally defined within this class type.
|
ImmutableList<Constructor> |
ClassType.getConstructors(Services services)
Returns the constructors locally defined within this class type.
|
ImmutableList<Field> |
NullType.getFields(Services services)
Returns the fields locally defined within this class type.
|
ImmutableList<Field> |
ClassType.getFields(Services services)
Returns the fields locally defined within this class type.
|
ImmutableList<Method> |
NullType.getMethods(Services services)
Returns the methods locally defined within this class type.
|
ImmutableList<Method> |
ClassType.getMethods(Services services)
Returns the methods locally defined within this class type.
|
Modifier and Type | Method and Description |
---|---|
ImmutableList<Field> |
TypeDeclaration.getAllFields(Services services)
[dlohner] The given parameter is obsolete with this implementation.
|
ImmutableList<Method> |
TypeDeclaration.getAllMethods(Services services)
TO BE IMPLEMENTED
|
ImmutableList<ClassType> |
TypeDeclaration.getAllSupertypes(Services services)
TO BE IMPLEMENTED
|
ImmutableList<ClassType> |
TypeDeclaration.getAllTypes(Services services)
TO BE IMPLEMENTED
|
ImmutableList<Constructor> |
TypeDeclaration.getConstructors(Services services)
TO BE IMPLEMENTED
|
ImmutableList<Field> |
TypeDeclaration.getFields(Services services)
TO BE IMPLEMENTED
|
ImmutableList<Method> |
TypeDeclaration.getMethods(Services services)
TO BE IMPLEMENTED
|
Package |
TypeDeclaration.getPackage(Services s)
TO BE IMPLEMENTED
|
ImmutableList<ClassType> |
TypeDeclaration.getTypes(Services services)
TO BE IMPLEMENTED
|
Modifier and Type | Method and Description |
---|---|
abstract KeYJavaType |
Literal.getKeYJavaType(Services javaServ)
retrieves the literal's type
|
KeYJavaType |
Assignment.getKeYJavaType(Services javaServ,
ExecutionContext ec)
retrieves the type of the assignment expression
|
KeYJavaType |
ArrayInitializer.getKeYJavaType(Services javaServ,
ExecutionContext ec) |
KeYJavaType |
Literal.getKeYJavaType(Services javaServ,
ExecutionContext ec)
retrieves the literal's type (as it is independant of the
execution context, it is same as using
Literal.getKeYJavaType(Services) ) |
abstract KeYJavaType |
Operator.getKeYJavaType(Services javaServ,
ExecutionContext ec) |
KeYJavaType |
ParenthesizedExpression.getKeYJavaType(Services javaServ,
ExecutionContext ec) |
java.lang.String |
Assignment.reuseSignature(Services services,
ExecutionContext ec)
overriden from Operator
|
java.lang.String |
Operator.reuseSignature(Services services,
ExecutionContext ec)
overriden from JavaProgramElement.
|
Modifier and Type | Method and Description |
---|---|
KeYJavaType |
EmptySeqLiteral.getKeYJavaType(Services javaServ) |
KeYJavaType |
StringLiteral.getKeYJavaType(Services javaServ) |
KeYJavaType |
DoubleLiteral.getKeYJavaType(Services javaServ) |
KeYJavaType |
NullLiteral.getKeYJavaType(Services javaServ) |
KeYJavaType |
CharLiteral.getKeYJavaType(Services javaServ) |
KeYJavaType |
EmptySetLiteral.getKeYJavaType(Services javaServ) |
KeYJavaType |
RealLiteral.getKeYJavaType(Services javaServ) |
KeYJavaType |
FloatLiteral.getKeYJavaType(Services javaServ) |
KeYJavaType |
BooleanLiteral.getKeYJavaType(Services javaServ) |
KeYJavaType |
IntLiteral.getKeYJavaType(Services javaServ) |
KeYJavaType |
FreeLiteral.getKeYJavaType(Services javaServ) |
KeYJavaType |
LongLiteral.getKeYJavaType(Services javaServ) |
KeYJavaType |
EmptyMapLiteral.getKeYJavaType(Services javaServ) |
Modifier and Type | Method and Description |
---|---|
KeYJavaType |
SeqIndexOf.getKeYJavaType(Services javaServ,
ExecutionContext ec) |
KeYJavaType |
SeqSingleton.getKeYJavaType(Services javaServ,
ExecutionContext ec) |
KeYJavaType |
SeqReverse.getKeYJavaType(Services javaServ,
ExecutionContext ec) |
KeYJavaType |
SeqGet.getKeYJavaType(Services javaServ,
ExecutionContext ec) |
KeYJavaType |
AllFields.getKeYJavaType(Services javaServ,
ExecutionContext ec) |
KeYJavaType |
AllObjects.getKeYJavaType(Services javaServ,
ExecutionContext ec) |
KeYJavaType |
SeqLength.getKeYJavaType(Services javaServ,
ExecutionContext ec) |
KeYJavaType |
SeqSub.getKeYJavaType(Services javaServ,
ExecutionContext ec) |
KeYJavaType |
Singleton.getKeYJavaType(Services javaServ,
ExecutionContext ec) |
Modifier and Type | Method and Description |
---|---|
KeYJavaType |
MethodReference.determineStaticPrefixType(Services services,
ExecutionContext ec)
returns the static KeYJavaType of the methods prefix
|
ProgramElement |
SchemaTypeReference.getConcreteProgramElement(Services services) |
KeYJavaType |
ArrayLengthReference.getKeYJavaType(Services javaServ) |
KeYJavaType |
SchemaTypeReference.getKeYJavaType(Services services) |
KeYJavaType |
MethodReference.getKeYJavaType(Services javaServ) |
KeYJavaType |
VariableReference.getKeYJavaType(Services javaServ) |
KeYJavaType |
ArrayLengthReference.getKeYJavaType(Services javaServ,
ExecutionContext ec) |
KeYJavaType |
MetaClassReference.getKeYJavaType(Services javaServ,
ExecutionContext ec) |
KeYJavaType |
MethodReference.getKeYJavaType(Services services,
ExecutionContext ec) |
KeYJavaType |
ArrayReference.getKeYJavaType(Services services,
ExecutionContext ec) |
KeYJavaType |
SuperReference.getKeYJavaType(Services javaServ,
ExecutionContext ec)
returns the KeYJavaType
|
KeYJavaType |
ThisReference.getKeYJavaType(Services javaServ,
ExecutionContext ec) |
KeYJavaType |
VariableReference.getKeYJavaType(Services javaServ,
ExecutionContext ec)
Gets the KeY java type.
|
ImmutableList<KeYJavaType> |
MethodReference.getMethodSignature(Services services,
ExecutionContext ec)
determines the arguments types and constructs a signature of the current
method
|
IProgramMethod |
MethodReference.method(Services services,
KeYJavaType refPrefixType,
ExecutionContext ec) |
IProgramMethod |
MethodReference.method(Services services,
KeYJavaType classType,
ImmutableList<KeYJavaType> signature,
KeYJavaType context) |
Modifier and Type | Method and Description |
---|---|
Statement |
MethodBodyStatement.getBody(Services services)
Get method body.
|
IProgramMethod |
MethodBodyStatement.getProgramMethod(Services services) |
boolean |
MethodBodyStatement.isStatic(Services services) |
java.lang.String |
MethodBodyStatement.reuseSignature(Services services,
ExecutionContext ec) |
Modifier and Type | Field and Description |
---|---|
protected Services |
JavaASTVisitor.services |
Constructor and Description |
---|
ContainsStatementVisitor(ProgramElement root,
SourceElement toSearch,
Services services)
Constructor.
|
CreatingASTVisitor(ProgramElement root,
boolean preservesPos,
Services services)
create the CreatingASTVisitor
|
DeclarationProgramVariableCollector(ProgramElement root,
Services services)
creates a new declaration visitor
|
FieldReplaceVisitor(ProgramElement pe,
Services services) |
InnerBreakAndContinueReplacer(StatementBlock block,
java.lang.Iterable<Label> loopLabels,
Label breakLabel,
Label continueLabel,
Services services) |
JavaASTVisitor(ProgramElement root,
Services services)
create the JavaASTVisitor
|
LabelCollector(ProgramElement root,
Services services) |
OuterBreakContinueAndReturnCollector(ProgramElement root,
java.util.List<Label> alwaysInnerLabels,
Services services) |
OuterBreakContinueAndReturnReplacer(StatementBlock block,
java.lang.Iterable<Label> alwaysInnerLabels,
Label breakOutLabel,
java.util.Map<Label,ProgramVariable> breakFlags,
java.util.Map<Label,ProgramVariable> continueFlags,
ProgramVariable returnFlag,
ProgramVariable returnValue,
ProgramVariable exception,
Services services) |
ProgramElementReplacer(JavaProgramElement program,
Services services) |
ProgramReplaceVisitor(ProgramElement root,
Services services,
SVInstantiations svi)
create the ProgramReplaceVisitor
|
ProgramVariableCollector(ProgramElement root,
Services services)
collects all program variables occurring in the AST root using
this constructor is equivalent to
ProggramVariableCollector(root, false)
|
ProgVarReplaceVisitor(ProgramElement st,
java.util.Map<ProgramVariable,ProgramVariable> map,
boolean replaceall,
Services services)
creates a visitor that replaces the program variables in the given
statement
|
ProgVarReplaceVisitor(ProgramElement st,
java.util.Map<ProgramVariable,ProgramVariable> map,
Services services)
creates a visitor that replaces the program variables in the given
statement by new ones with the same name
|
UndeclaredProgramVariableCollector(ProgramElement root,
Services services)
Constructor.
|
Modifier and Type | Method and Description |
---|---|
Function |
HeapLDT.getFieldSymbolForPV(LocationVariable fieldPV,
Services services)
Given a "program variable" representing a field or a model field,
returns the function symbol representing the same field.
|
Function |
DoubleLDT.getFunctionFor(Operator op,
Services services,
ExecutionContext ec) |
Function |
CharListLDT.getFunctionFor(Operator op,
Services serv,
ExecutionContext ec) |
Function |
FreeLDT.getFunctionFor(Operator op,
Services services,
ExecutionContext ec) |
Function |
MapLDT.getFunctionFor(Operator op,
Services serv,
ExecutionContext ec) |
Function |
RealLDT.getFunctionFor(Operator op,
Services services,
ExecutionContext ec) |
Function |
BooleanLDT.getFunctionFor(Operator op,
Services services,
ExecutionContext ec) |
Function |
PermissionLDT.getFunctionFor(Operator op,
Services services,
ExecutionContext ec) |
Function |
LocSetLDT.getFunctionFor(Operator op,
Services serv,
ExecutionContext ec) |
Function |
IntegerLDT.getFunctionFor(Operator op,
Services serv,
ExecutionContext ec)
returns the function symbol for the given operation
null if no function is found for the given operator
|
Function |
HeapLDT.getFunctionFor(Operator op,
Services serv,
ExecutionContext ec) |
Function |
FloatLDT.getFunctionFor(Operator op,
Services services,
ExecutionContext ec) |
Function |
SeqLDT.getFunctionFor(Operator op,
Services serv,
ExecutionContext ec) |
abstract Function |
LDT.getFunctionFor(Operator op,
Services services,
ExecutionContext ec)
returns the function symbol for the given operation
|
static java.util.Map<Name,LDT> |
LDT.getNewLDTInstances(Services s) |
boolean |
DoubleLDT.isResponsible(Operator op,
Term[] subs,
Services services,
ExecutionContext ec) |
boolean |
CharListLDT.isResponsible(Operator op,
Term[] subs,
Services services,
ExecutionContext ec) |
boolean |
FreeLDT.isResponsible(Operator op,
Term[] subs,
Services services,
ExecutionContext ec) |
boolean |
MapLDT.isResponsible(Operator op,
Term[] subs,
Services services,
ExecutionContext ec) |
boolean |
RealLDT.isResponsible(Operator op,
Term[] subs,
Services services,
ExecutionContext ec) |
boolean |
BooleanLDT.isResponsible(Operator op,
Term[] subs,
Services services,
ExecutionContext ec) |
boolean |
PermissionLDT.isResponsible(Operator op,
Term[] subs,
Services services,
ExecutionContext ec) |
boolean |
LocSetLDT.isResponsible(Operator op,
Term[] subs,
Services services,
ExecutionContext ec) |
boolean |
IntegerLDT.isResponsible(Operator op,
Term[] subs,
Services services,
ExecutionContext ec) |
boolean |
HeapLDT.isResponsible(Operator op,
Term[] subs,
Services services,
ExecutionContext ec) |
boolean |
FloatLDT.isResponsible(Operator op,
Term[] subs,
Services services,
ExecutionContext ec) |
boolean |
SeqLDT.isResponsible(Operator op,
Term[] subs,
Services services,
ExecutionContext ec) |
abstract boolean |
LDT.isResponsible(Operator op,
Term[] subs,
Services services,
ExecutionContext ec)
returns true if the LDT offers an operation for the given java
operator and the logic subterms
|
boolean |
DoubleLDT.isResponsible(Operator op,
Term left,
Term right,
Services services,
ExecutionContext ec) |
boolean |
CharListLDT.isResponsible(Operator op,
Term left,
Term right,
Services services,
ExecutionContext ec) |
boolean |
FreeLDT.isResponsible(Operator op,
Term left,
Term right,
Services services,
ExecutionContext ec) |
boolean |
MapLDT.isResponsible(Operator op,
Term left,
Term right,
Services services,
ExecutionContext ec) |
boolean |
RealLDT.isResponsible(Operator op,
Term left,
Term right,
Services services,
ExecutionContext ec) |
boolean |
BooleanLDT.isResponsible(Operator op,
Term left,
Term right,
Services services,
ExecutionContext ec) |
boolean |
PermissionLDT.isResponsible(Operator op,
Term left,
Term right,
Services services,
ExecutionContext ec) |
boolean |
LocSetLDT.isResponsible(Operator op,
Term left,
Term right,
Services services,
ExecutionContext ec) |
boolean |
IntegerLDT.isResponsible(Operator op,
Term left,
Term right,
Services services,
ExecutionContext ec) |
boolean |
HeapLDT.isResponsible(Operator op,
Term left,
Term right,
Services services,
ExecutionContext ec) |
boolean |
FloatLDT.isResponsible(Operator op,
Term left,
Term right,
Services services,
ExecutionContext ec) |
boolean |
SeqLDT.isResponsible(Operator op,
Term left,
Term right,
Services services,
ExecutionContext ec) |
abstract boolean |
LDT.isResponsible(Operator op,
Term left,
Term right,
Services services,
ExecutionContext ec)
returns true if the LDT offers an operation for the given
binary java operator and the logic subterms
|
Term |
DoubleLDT.translateLiteral(Literal lit,
Services services) |
Term |
CharListLDT.translateLiteral(Literal lit,
Services services) |
Term |
FreeLDT.translateLiteral(Literal lit,
Services services) |
Term |
MapLDT.translateLiteral(Literal lit,
Services services) |
Term |
RealLDT.translateLiteral(Literal lit,
Services services) |
Term |
BooleanLDT.translateLiteral(Literal lit,
Services services) |
Term |
PermissionLDT.translateLiteral(Literal lit,
Services services) |
Term |
LocSetLDT.translateLiteral(Literal lit,
Services services) |
Term |
IntegerLDT.translateLiteral(Literal lit,
Services services) |
Term |
HeapLDT.translateLiteral(Literal lit,
Services services) |
Term |
FloatLDT.translateLiteral(Literal lit,
Services services) |
Term |
SeqLDT.translateLiteral(Literal lit,
Services services) |
abstract Term |
LDT.translateLiteral(Literal lit,
Services services)
translates a given literal to its logic counterpart
|
Expression |
DoubleLDT.translateTerm(Term t,
ExtList children,
Services services) |
Expression |
CharListLDT.translateTerm(Term t,
ExtList children,
Services services) |
Expression |
FreeLDT.translateTerm(Term t,
ExtList children,
Services services) |
Expression |
MapLDT.translateTerm(Term t,
ExtList children,
Services services) |
Expression |
RealLDT.translateTerm(Term t,
ExtList children,
Services services) |
Expression |
BooleanLDT.translateTerm(Term t,
ExtList children,
Services services) |
Expression |
PermissionLDT.translateTerm(Term t,
ExtList children,
Services services) |
Expression |
LocSetLDT.translateTerm(Term t,
ExtList children,
Services services) |
Expression |
IntegerLDT.translateTerm(Term t,
ExtList children,
Services services) |
Expression |
HeapLDT.translateTerm(Term t,
ExtList children,
Services services) |
Expression |
FloatLDT.translateTerm(Term t,
ExtList children,
Services services) |
Expression |
SeqLDT.translateTerm(Term t,
ExtList children,
Services services) |
abstract Expression |
LDT.translateTerm(Term t,
ExtList children,
Services services)
Is called whenever
hasLiteralFunction() returns true. |
Constructor and Description |
---|
IntegerLDT(Services services) |
PermissionLDT(Services services) |
Modifier and Type | Field and Description |
---|---|
protected Services |
VariableNamer.services
pointer to services object
|
protected Services |
TermBuilder.services |
Modifier and Type | Method and Description |
---|---|
Term |
TermBuilder.bprod(QuantifiableVariable qv,
Term a,
Term b,
Term t,
Services services)
Constructs a bounded product comprehension expression.
|
Term |
TermBuilder.forallHeaps(Services services,
Term t) |
java.lang.String |
VariableNamer.getProposal(TacletApp app,
SchemaVariable var,
Services services,
Node undoAnchor,
ImmutableList<java.lang.String> previousProposals)
proposes a unique name for the instantiation of a schema variable
|
java.lang.String |
VariableNamer.getSuggestiveNameProposalForProgramVariable(SchemaVariable sv,
TacletApp app,
Services services,
ImmutableList<java.lang.String> previousProposals) |
static Term |
GenericTermReplacer.replace(Term t,
java.util.function.Predicate<Term> filter,
java.util.function.Function<Term,Term> replacer,
Services services) |
Constructor and Description |
---|
InnerVariableNamer(Services services) |
TermBuilder(TermFactory tf,
Services services) |
VariableNamer(Services services) |
Modifier and Type | Method and Description |
---|---|
static boolean |
OriginTermLabel.canAddLabel(Operator op,
Services services)
Determines whether an
OriginTermLabel can be added to a term with the specified
operator. |
static boolean |
OriginTermLabel.canAddLabel(Term term,
Services services)
Determines whether an
OriginTermLabel can be added to the specified term. |
static Term |
OriginTermLabel.collectSubtermOrigins(Term term,
Services services)
This method transforms a term in such a way that
every
OriginTermLabel contains all of the correct
OriginTermLabel.getSubtermOrigins() . |
protected TermLabelManager.RefactoringsContainer |
TermLabelManager.computeRefactorings(TermLabelState state,
Services services,
PosInOccurrence applicationPosInOccurrence,
Term applicationTerm,
Rule rule,
Goal goal,
java.lang.Object hint,
Term tacletTerm)
Computes the
TermLabelRefactoring to consider. |
static ImmutableList<Name> |
TermLabelManager.getSupportedTermLabelNames(Services services)
|
static TermLabelManager |
TermLabelManager.getTermLabelManager(Services services)
|
static ImmutableArray<TermLabel> |
TermLabelManager.instantiateLabels(TermLabelState state,
Services services,
PosInOccurrence applicationPosInOccurrence,
Rule rule,
RuleApp ruleApp,
Goal goal,
java.lang.Object hint,
Term tacletTerm,
Operator newTermOp,
ImmutableArray<Term> newTermSubs,
ImmutableArray<QuantifiableVariable> newTermBoundVars,
JavaBlock newTermJavaBlock,
ImmutableArray<TermLabel> newTermOriginalLabels)
|
ImmutableArray<TermLabel> |
TermLabelManager.instantiateLabels(TermLabelState state,
Services services,
PosInOccurrence applicationPosInOccurrence,
Term applicationTerm,
Rule rule,
RuleApp ruleApp,
Goal goal,
java.lang.Object hint,
Term tacletTerm,
Operator newTermOp,
ImmutableArray<Term> newTermSubs,
ImmutableArray<QuantifiableVariable> newTermBoundVars,
JavaBlock newTermJavaBlock,
ImmutableArray<TermLabel> newTermOriginalLabels)
|
static ImmutableArray<TermLabel> |
TermLabelManager.instantiateLabels(TermLabelState state,
Services services,
Term applicationTerm,
PosInOccurrence applicationPosInOccurrence,
Rule rule,
RuleApp ruleApp,
Goal goal,
java.lang.Object hint,
Term tacletTerm,
Operator newTermOp,
ImmutableArray<Term> newTermSubs,
ImmutableArray<QuantifiableVariable> newTermBoundVars,
JavaBlock newTermJavaBlock,
ImmutableArray<TermLabel> newTermOriginalLabels)
|
static Term |
TermLabelManager.label(Services services,
TermLabelState state,
PosInOccurrence applicationPosInOccurrence,
Rule rule,
RuleApp ruleApp,
Goal goal,
java.lang.Object hint,
Term tacletTerm,
Term newTerm)
Computes the
TermLabel s for the new Term via
TermLabelManager.instantiateLabels(TermLabelState, Services, PosInOccurrence, Term, Rule, RuleApp,
Goal, Object, Term, Operator, ImmutableArray, ImmutableArray,
JavaBlock, ImmutableArray)
and refactors the labels below the new Term in addition via
TermLabelManager.refactorTerm(TermLabelState, Services, PosInOccurrence, Term, Goal, Object,
Rule, Term) . |
static Term |
TermLabelManager.label(Services services,
TermLabelState state,
Term applicationTerm,
PosInOccurrence applicationPosInOccurrence,
Rule rule,
RuleApp ruleApp,
Goal goal,
java.lang.Object hint,
Term tacletTerm,
Term newTerm)
Computes the
TermLabel s for the new Term via
TermLabelManager.instantiateLabels(TermLabelState, Services, PosInOccurrence, Term, Rule, RuleApp,
Goal, Object, Term, Operator, ImmutableArray, ImmutableArray,
JavaBlock, ImmutableArray)
and refactors the labels below the new Term in addition via
TermLabelManager.refactorTerm(TermLabelState, Services, PosInOccurrence, Term, Goal, Object,
Rule, Term) . |
Term |
TermLabelManager.label(TermLabelState state,
Services services,
Term applicationTerm,
PosInOccurrence applicationPosInOccurrence,
Rule rule,
RuleApp ruleApp,
Goal goal,
java.lang.Object hint,
Term tacletTerm,
Term newTerm)
Computes the
TermLabel s for the new Term via
TermLabelManager.instantiateLabels(TermLabelState, Services, PosInOccurrence, Term, Rule, RuleApp,
Goal, Object, Term, Operator, ImmutableArray, ImmutableArray,
JavaBlock, ImmutableArray)
and refactors the labels below the new Term in addition via
TermLabelManager.refactorTerm(TermLabelState, Services, PosInOccurrence, Term, Goal, Object,
Rule, Term) . |
static void |
TermLabelManager.mergeLabels(SequentChangeInfo currentSequent,
Services services)
|
protected void |
TermLabelManager.mergeLabels(SequentChangeInfo currentSequent,
Services services,
SequentFormula rejectedSF,
boolean inAntecedent)
|
void |
TermLabelManager.mergeLabels(Services services,
SequentChangeInfo currentSequent)
|
static int |
FormulaTermLabel.newLabelSubID(Services services,
FormulaTermLabel label)
Creates a new label sub ID.
|
static int |
FormulaTermLabel.newLabelSubID(Services services,
int labelId)
Creates a new label sub ID.
|
protected ImmutableArray<TermLabel> |
TermLabelManager.performRefactoring(TermLabelState state,
Services services,
PosInOccurrence applicationPosInOccurrence,
Term applicationTerm,
Rule rule,
Goal goal,
java.lang.Object hint,
Term tacletTerm,
Term term,
ImmutableList<TermLabelRefactoring> activeRefactorings)
Computes the new labels as part of the refactoring for the given
Term . |
protected void |
TermLabelManager.performTermLabelPolicies(TermLabelState state,
Services services,
PosInOccurrence applicationPosInOccurrence,
Term applicationTerm,
Rule rule,
Goal goal,
java.lang.Object hint,
Term tacletTerm,
Operator newTermOp,
ImmutableArray<Term> newTermSubs,
ImmutableArray<QuantifiableVariable> newTermBoundVars,
JavaBlock newTermJavaBlock,
ImmutableArray<TermLabel> newTermOriginalLabels,
java.util.Map<Name,TermLabelPolicy> policies,
java.util.Set<TermLabel> newLabels)
Performs the given
TermLabelPolicy instances. |
protected void |
TermLabelManager.performTermLabelPolicies(TermLabelState state,
Services services,
PosInOccurrence applicationPosInOccurrence,
Term applicationTerm,
Rule rule,
Goal goal,
java.lang.Object hint,
Term tacletTerm,
Operator newTermOp,
ImmutableArray<Term> newTermSubs,
ImmutableArray<QuantifiableVariable> newTermBoundVars,
JavaBlock newTermJavaBlock,
ImmutableArray<TermLabel> newTermOriginalLabels,
java.util.Map<Name,TermLabelPolicy> policies,
java.util.Set<TermLabel> newLabels,
TermLabel label)
Performs the given
TermLabelPolicy instances. |
protected void |
TermLabelManager.performUpdater(TermLabelState state,
Services services,
PosInOccurrence applicationPosInOccurrence,
Term applicationTerm,
Term modalityTerm,
Rule rule,
RuleApp ruleApp,
java.lang.Object hint,
Term tacletTerm,
Operator newTermOp,
ImmutableArray<Term> newTermSubs,
ImmutableArray<QuantifiableVariable> newTermBoundVars,
JavaBlock newTermJavaBlock,
ImmutableList<TermLabelUpdate> updater,
java.util.Set<TermLabel> newLabels)
Performs the given child and grandchild
TermLabelUpdate instances. |
protected Term |
TermLabelManager.refactorApplicationTerm(TermLabelState state,
Services services,
PosInOccurrence applicationPosInOccurrence,
Term applicationTerm,
Rule rule,
Goal goal,
java.lang.Object hint,
Term tacletTerm,
TermLabelManager.RefactoringsContainer refactorings,
TermFactory tf)
Refactors the labels of the application term.
|
static void |
TermLabelManager.refactorGoal(TermLabelState state,
Services services,
PosInOccurrence applicationPosInOccurrence,
Rule rule,
Goal goal,
java.lang.Object hint,
Term tacletTerm)
Refactors all labels in the complete
Sequent . |
void |
TermLabelManager.refactorGoal(TermLabelState state,
Services services,
PosInOccurrence applicationPosInOccurrence,
Term applicationTerm,
Rule rule,
Goal goal,
java.lang.Object hint,
Term tacletTerm)
Refactors all labels in the complete
Sequent . |
protected Term |
TermLabelManager.refactorLabelsRecursive(TermLabelState state,
Services services,
PosInOccurrence applicationPosInOccurrence,
Term applicationTerm,
Rule rule,
Goal goal,
java.lang.Object hint,
Term tacletTerm,
Term term,
ImmutableList<TermLabelRefactoring> activeRefactorings)
|
protected void |
TermLabelManager.refactorSemisequent(TermLabelState state,
Services services,
PosInOccurrence applicationPosInOccurrence,
Term applicationTerm,
Rule rule,
Goal goal,
java.lang.Object hint,
Term tacletTerm,
Semisequent semisequent,
boolean inAntec,
ImmutableList<TermLabelRefactoring> activeRefactorings)
Performs a
TermLabel refactoring on the given Semisequent . |
static void |
TermLabelManager.refactorSequent(TermLabelState state,
Services services,
PosInOccurrence applicationPosInOccurrence,
Rule rule,
Goal goal,
java.lang.Object hint,
Term tacletTerm)
Refactors all labels in the complete
Sequent . |
void |
TermLabelManager.refactorSequent(TermLabelState state,
Services services,
PosInOccurrence applicationPosInOccurrence,
Term applicationTerm,
Rule rule,
Goal goal,
java.lang.Object hint,
Term tacletTerm)
Refactors all labels in the complete
Sequent . |
Term |
TermLabelManager.refactorSequentFormula(TermLabelState state,
Services services,
Term sequentFormula,
PosInOccurrence applicationPosInOccurrence,
Goal goal,
java.lang.Object hint,
Rule rule,
Term tacletTerm)
|
static Term |
TermLabelManager.refactorSequentFormula(TermLabelState state,
Services services,
Term sequentFormula,
PosInOccurrence applicationPosInOccurrence,
Rule rule,
Goal goal,
java.lang.Object hint,
Term tacletTerm)
|
Term |
TermLabelManager.refactorTerm(TermLabelState state,
Services services,
PosInOccurrence applicationPosInOccurrence,
Term applicationTerm,
Goal goal,
java.lang.Object hint,
Rule rule,
Term tacletTerm)
Refactors all labels in the given application
Term . |
static Term |
TermLabelManager.refactorTerm(TermLabelState state,
Services services,
PosInOccurrence applicationPosInOccurrence,
Term applicationTerm,
Rule rule,
Goal goal,
java.lang.Object hint,
Term tacletTerm)
Refactors all labels in the complete
Sequent . |
static Term |
TermLabel.removeIrrelevantLabels(Term term,
Services services)
Remove all irrelevant labels from a term.
|
static SequentChangeInfo |
OriginTermLabel.removeOriginLabels(Sequent seq,
Services services)
Removes all
OriginTermLabel from the specified sequent. |
static Term |
OriginTermLabel.removeOriginLabels(Term term,
Services services)
Removes all
OriginTermLabel from the specified term and its sub-terms. |
protected Term |
TermLabelManager.replaceTerm(TermLabelState state,
PosInOccurrence pio,
Term newTerm,
TermFactory tf,
ImmutableList<TermLabelRefactoring> parentRefactorings,
Services services,
PosInOccurrence applicationPosInOccurrence,
Term applicationTerm,
Rule rule,
Goal goal,
java.lang.Object hint,
Term tacletTerm)
Replaces the
Term at the specified PosInOccurrence . |
Modifier and Type | Method and Description |
---|---|
static java.lang.String |
AbstractTermTransformer.convertToDecimalString(Term term,
Services services) |
int |
IObserverFunction.getHeapCount(Services services)
Check the heap count of the declaration, e.g.
|
int |
ProgramSV.getHeapCount(Services services) |
int |
ObserverFunction.getHeapCount(Services services) |
KeYJavaType |
ProgramVariable.getKeYJavaType(Services javaServ) |
KeYJavaType |
IProgramVariable.getKeYJavaType(Services javaServ) |
KeYJavaType |
ProgramSV.getKeYJavaType(Services javaServ) |
KeYJavaType |
ProgramVariable.getKeYJavaType(Services javaServ,
ExecutionContext ec) |
KeYJavaType |
IProgramVariable.getKeYJavaType(Services javaServ,
ExecutionContext ec) |
KeYJavaType |
ProgramSV.getKeYJavaType(Services javaServ,
ExecutionContext ec) |
Term |
TermTransformer.transform(Term term,
SVInstantiations svInst,
Services services)
initiates term transformation of term.
|
Modifier and Type | Method and Description |
---|---|
boolean |
ProgramSVSort.canStandFor(ProgramElement check,
ExecutionContext ec,
Services services) |
boolean |
ProgramSVSort.SimpleExpressionStringSort.canStandFor(ProgramElement check,
ExecutionContext ec,
Services services) |
boolean |
ProgramSVSort.SimpleExpressionNonStringObjectSort.canStandFor(ProgramElement check,
ExecutionContext ec,
Services services) |
protected abstract boolean |
ProgramSVSort.canStandFor(ProgramElement check,
Services services) |
ImmutableSet<Sort> |
NullSort.extendsSorts(Services services) |
ImmutableSet<Sort> |
AbstractSort.extendsSorts(Services services) |
ImmutableSet<Sort> |
Sort.extendsSorts(Services services) |
Modifier and Type | Field and Description |
---|---|
protected Services |
AbstractCommand.service |
Modifier and Type | Method and Description |
---|---|
static PosInOccurrence |
MacroCommand.extractMatchingPio(Sequent sequent,
java.lang.String matchRegEx,
Services services)
TODO
|
Modifier and Type | Method and Description |
---|---|
Services |
KeyIO.getServices() |
Constructor and Description |
---|
KeyIO(Services services) |
KeyIO(Services services,
NamespaceSet nss) |
Modifier and Type | Field and Description |
---|---|
protected Services |
DefaultBuilder.services |
Modifier and Type | Method and Description |
---|---|
Services |
DefaultBuilder.getServices() |
Constructor and Description |
---|
ContractsAndInvariantsFinder(Services services,
NamespaceSet nss) |
DeclarationBuilder(Services services,
NamespaceSet nss) |
DefaultBuilder(Services services,
NamespaceSet nss) |
ExpressionBuilder(Services services,
NamespaceSet nss) |
ExpressionBuilder(Services services,
NamespaceSet nss,
Namespace<SchemaVariable> schemaNamespace) |
FunctionPredicateBuilder(Services services,
NamespaceSet nss) |
ProblemFinder(Services services,
NamespaceSet nss) |
TacletPBuilder(Services services,
NamespaceSet nss) |
TacletPBuilder(Services services,
NamespaceSet namespaces,
java.util.HashMap<Taclet,TacletBuilder<? extends Taclet>> taclet2Builder) |
Modifier and Type | Method and Description |
---|---|
Services |
ParserConfig.services() |
Modifier and Type | Method and Description |
---|---|
Term |
DefaultTermParser.parse(java.io.Reader in,
Sort sort,
Services services,
Namespace<QuantifiableVariable> var_ns,
Namespace<Function> func_ns,
Namespace<Sort> sort_ns,
Namespace<IProgramVariable> progVar_ns,
AbbrevMap scm)
Deprecated.
The method reads the input and parses a term with the
specified namespaces.
|
Term |
DefaultTermParser.parse(java.io.Reader in,
Sort sort,
Services services,
NamespaceSet nss,
AbbrevMap scm)
Deprecated.
The method reads the input and parses a term with the
specified namespaces.
|
Sequent |
DefaultTermParser.parseSeq(java.io.Reader in,
Services services,
NamespaceSet nss,
AbbrevMap scm)
Deprecated.
The method reads the input and parses a sequent with the
specified namespaces.
|
Constructor and Description |
---|
ParserConfig(Services services,
NamespaceSet nss) |
Modifier and Type | Field and Description |
---|---|
protected Services |
LogicPrinter.services
the services object
|
Modifier and Type | Method and Description |
---|---|
static boolean |
LogicPrinter.printInShortForm(java.lang.String programName,
Sort sort,
Services services)
tests if the program name together with the prefix sort determines the
attribute in a unique way
|
static java.lang.String |
LogicPrinter.quickPrintSemisequent(Semisequent s,
Services services)
Converts a semisequent to a string.
|
static java.lang.String |
LogicPrinter.quickPrintSequent(Sequent s,
Services services)
Converts a sequent to a string.
|
static java.lang.String |
LogicPrinter.quickPrintTerm(Term t,
Services services)
Converts a term to a string.
|
static java.lang.String |
LogicPrinter.quickPrintTerm(Term t,
Services services,
boolean usePrettyPrinting,
boolean useUnicodeSymbols)
Converts a term to a string.
|
void |
NotationInfo.refresh(Services services) |
void |
NotationInfo.refresh(Services services,
boolean usePrettyPrinting,
boolean useUnicodeSymbols) |
Constructor and Description |
---|
LogicPrinter(ProgramPrinter prgPrinter,
NotationInfo notationInfo,
Backend backend,
Services services,
boolean purePrint)
Creates a LogicPrinter.
|
LogicPrinter(ProgramPrinter prgPrinter,
NotationInfo notationInfo,
Services services)
Creates a LogicPrinter.
|
LogicPrinter(ProgramPrinter prgPrinter,
NotationInfo notationInfo,
Services services,
boolean purePrint)
Creates a LogicPrinter.
|
SequentViewLogicPrinter(ProgramPrinter prgPrinter,
NotationInfo notationInfo,
Backend backend,
Services services,
boolean purePrint,
VisibleTermLabels visibleTermLabels) |
SequentViewLogicPrinter(ProgramPrinter prgPrinter,
NotationInfo notationInfo,
Services services,
boolean purePrint,
VisibleTermLabels visibleTermLabels) |
SequentViewLogicPrinter(ProgramPrinter prgPrinter,
NotationInfo notationInfo,
Services services,
VisibleTermLabels visibleTermLabels) |
Modifier and Type | Method and Description |
---|---|
Services |
Proof.getServices()
returns the Services with the java service classes
|
Modifier and Type | Method and Description |
---|---|
TermTacletAppIndex |
TermTacletAppIndex.addTaclets(RuleFilter filter,
PosInOccurrence pos,
Services services,
TacletIndex tacletIndex,
NewRuleListener listener)
Create a new tree of indices that additionally contain the taclets that
are selected by
filter |
SemisequentTacletAppIndex |
SemisequentTacletAppIndex.addTaclets(RuleFilter filter,
Sequent s,
Services services,
TacletIndex tacletIndex,
NewRuleListener listener)
Create an index that additionally contains the taclets that are selected
by
filter |
static TermTacletAppIndex |
TermTacletAppIndex.create(PosInOccurrence pos,
Services services,
TacletIndex tacletIndex,
NewRuleListener listener,
RuleFilter filter,
TermTacletAppIndexCacheSet indexCaches)
Create an index for the given term
|
protected static java.lang.String |
VariableNameProposer.createBaseNameProposalBasedOnCorrespondence(TacletApp p_app,
SchemaVariable p_var,
Services services)
Find a name for the variable
p_var , based on the result
of Taclet.getNameCorrespondent |
java.util.List<TacletApp> |
Goal.getAllTacletApps(Services services) |
ImmutableList<NoPosTacletApp> |
TacletIndex.getAntecedentTaclet(PosInOccurrence pos,
RuleFilter filter,
Services services)
get all Taclets for the antecedent.
|
java.lang.String |
VariableNameProposer.getNameProposal(java.lang.String basename,
Services services,
Node undoAnchor) |
Name |
VariableNameProposer.getNewName(Services services,
Name baseName)
Warning: this method is buggy.
|
ImmutableList<NoPosTacletApp> |
TacletIndex.getNoFindTaclet(RuleFilter filter,
Services services)
get all Taclets having no find expression.
|
ImmutableList<NoPosTacletApp> |
RuleAppIndex.getNoFindTaclet(TacletFilter filter,
Services services)
collects all NoFindTacletInstantiations for the given
heuristics
|
ImmutableList<NoPosTacletApp> |
TacletAppIndex.getNoFindTaclet(TacletFilter filter,
Services services)
collects all NoFindTacletInstantiations
|
java.lang.String |
InstantiationProposer.getProposal(TacletApp app,
SchemaVariable var,
Services services,
Node undoAnchor,
ImmutableList<java.lang.String> previousProposals)
Returns an instantiation proposal for the schema variable var.
|
java.lang.String |
VariableNameProposer.getProposal(TacletApp app,
SchemaVariable var,
Services services,
Node undoAnchor,
ImmutableList<java.lang.String> previousProposals)
Returns an instantiation proposal for the schema variable var.
|
java.lang.String |
InstantiationProposerCollection.getProposal(TacletApp app,
SchemaVariable var,
Services services,
Node undoAnchor,
ImmutableList<java.lang.String> previousProposals) |
ImmutableList<NoPosTacletApp> |
TacletIndex.getRewriteTaclet(PosInOccurrence pos,
RuleFilter filter,
Services services)
get all Rewrite-Taclets.
|
ImmutableList<NoPosTacletApp> |
TacletIndex.getSuccedentTaclet(PosInOccurrence pos,
RuleFilter filter,
Services services)
get all Taclets for the succedent.
|
ImmutableList<TacletApp> |
TacletAppIndex.getTacletAppAt(PosInOccurrence pos,
TacletFilter filter,
Services services)
returns the set of rule applications
at the given position of the given sequent.
|
ImmutableList<TacletApp> |
RuleAppIndex.getTacletAppAt(TacletFilter filter,
PosInOccurrence pos,
Services services)
returns the set of rule applications for
the given heuristics
at the given position of the given sequent.
|
ImmutableList<TacletApp> |
TermTacletAppIndex.getTacletAppAtAndBelow(PosInOccurrence pos,
RuleFilter filter,
Services services) |
ImmutableList<TacletApp> |
SemisequentTacletAppIndex.getTacletAppAtAndBelow(PosInOccurrence pos,
RuleFilter filter,
Services services) |
ImmutableList<TacletApp> |
TacletAppIndex.getTacletAppAtAndBelow(PosInOccurrence pos,
TacletFilter filter,
Services services)
returns the rule applications at the given PosInOccurrence and at all
Positions below this.
|
ImmutableList<TacletApp> |
RuleAppIndex.getTacletAppAtAndBelow(TacletFilter filter,
PosInOccurrence pos,
Services services)
returns the rule applications at the given PosInOccurrence and at all
Positions below this.
|
protected abstract ImmutableList<NoPosTacletApp> |
TacletIndex.matchTaclets(ImmutableList<NoPosTacletApp> tacletApps,
RuleFilter p_filter,
PosInOccurrence pos,
Services services)
Filter the given list of taclet apps, and match their find
parts at the given position of the sequent
|
void |
RuleAppIndex.reportAutomatedRuleApps(NewRuleListener l,
Services services)
Report all rule applications that are supposed to be applied
automatically, and that are currently stored by the index
|
void |
TacletAppIndex.reportRuleApps(NewRuleListener l,
Services services)
Reports all cached rule apps.
|
SemisequentTacletAppIndex |
SemisequentTacletAppIndex.sequentChanged(SequentChangeInfo sci,
Services services,
TacletIndex tacletIndex,
NewRuleListener listener)
called if a formula has been replaced
|
Constructor and Description |
---|
ProgVarReplacer(java.util.Map<ProgramVariable,ProgramVariable> map,
Services services)
creates a ProgVarReplacer that replaces program variables as specified
by the map parameter
|
RuleAppIndex(TacletAppIndex p_tacletAppIndex,
BuiltInRuleAppIndex p_builtInRuleAppIndex,
Services services) |
RuleAppIndex(TacletIndex p_tacletIndex,
BuiltInRuleAppIndex p_builtInRuleAppIndex,
Services services) |
TacletAppIndex(TacletIndex tacletIndex,
Services services) |
TermProgramVariableCollector(Services services) |
TermProgramVariableCollectorKeepUpdatesForBreakpointconditions(Services services,
IBreakpointStopCondition breakpointStopCondition) |
Modifier and Type | Method and Description |
---|---|
static java.util.LinkedHashSet<IProofReference<?>> |
ProofReferenceUtil.computeProofReferences(Node node,
Services services)
Computes the
IProofReference of the given Node . |
static java.util.LinkedHashSet<IProofReference<?>> |
ProofReferenceUtil.computeProofReferences(Node node,
Services services,
ImmutableList<IProofReferencesAnalyst> analysts)
Computes the
IProofReference of the given Node . |
Modifier and Type | Method and Description |
---|---|
java.util.LinkedHashSet<IProofReference<?>> |
ClassAxiomAndInvariantProofReferencesAnalyst.computeReferences(Node node,
Services services)
Computes the
IProofReference for the given Node which
can be null or an empty set if the applied rule is not supported by this IProofReferencesAnalyst . |
java.util.LinkedHashSet<IProofReference<?>> |
ProgramVariableReferencesAnalyst.computeReferences(Node node,
Services services)
Computes the
IProofReference for the given Node which
can be null or an empty set if the applied rule is not supported by this IProofReferencesAnalyst . |
java.util.LinkedHashSet<IProofReference<?>> |
MethodBodyExpandProofReferencesAnalyst.computeReferences(Node node,
Services services)
Computes the
IProofReference for the given Node which
can be null or an empty set if the applied rule is not supported by this IProofReferencesAnalyst . |
java.util.LinkedHashSet<IProofReference<?>> |
ContractProofReferencesAnalyst.computeReferences(Node node,
Services services)
Computes the
IProofReference for the given Node which
can be null or an empty set if the applied rule is not supported by this IProofReferencesAnalyst . |
java.util.LinkedHashSet<IProofReference<?>> |
IProofReferencesAnalyst.computeReferences(Node node,
Services services)
Computes the
IProofReference for the given Node which
can be null or an empty set if the applied rule is not supported by this IProofReferencesAnalyst . |
java.util.LinkedHashSet<IProofReference<?>> |
MethodCallProofReferencesAnalyst.computeReferences(Node node,
Services services)
Computes the
IProofReference for the given Node which
can be null or an empty set if the applied rule is not supported by this IProofReferencesAnalyst . |
protected IProofReference<IProgramMethod> |
MethodCallProofReferencesAnalyst.createReference(Node node,
Services services,
ExecutionContext context,
MethodReference mr)
Creates an
IProofReference to the called IProgramMethod . |
protected ExecutionContext |
MethodCallProofReferencesAnalyst.extractContext(Node node,
Services services)
Extracts the
ExecutionContext . |
protected KeYJavaType |
ClassAxiomAndInvariantProofReferencesAnalyst.findProofsKeYJavaType(Services services)
Returns the
KeYJavaType which provides the proof obligation of the current proof. |
Modifier and Type | Method and Description |
---|---|
Services |
DelayedCut.getServices() |
Modifier and Type | Field and Description |
---|---|
protected Services |
AbstractPO.environmentServices |
Modifier and Type | Method and Description |
---|---|
Services |
InitConfig.getServices()
returns the Services of this initial configuration providing access
to the used program model
|
protected Services |
FunctionalBlockContractPO.postInit()
Initializes the proof configuration.
|
protected Services |
FunctionalLoopContractPO.postInit()
Initializes the proof configuration.
|
protected Services |
AbstractOperationPO.postInit() |
Modifier and Type | Method and Description |
---|---|
static Term |
AbstractOperationPO.addAdditionalUninterpretedPredicateIfRequired(Services services,
Term term,
ImmutableList<LocationVariable> variablesToProtect,
Term exceptionVar)
This method adds the uninterpreted predicate to the given
Term
if the used ProofOblInput is an instance of AbstractOperationPO
and AbstractOperationPO.isAddUninterpretedPredicate() is true . |
static Term |
AbstractOperationPO.addUninterpretedPredicateIfRequired(Services services,
Term term)
This method adds the uninterpreted predicate to the given
Term
if the used ProofOblInput is an instance of AbstractOperationPO
and AbstractOperationPO.isAddUninterpretedPredicate() is true . |
protected abstract Term |
AbstractOperationPO.buildFrameClause(java.util.List<LocationVariable> modHeaps,
java.util.Map<Term,Term> heapToAtPre,
ProgramVariable selfVar,
ImmutableList<ProgramVariable> paramVars,
Services services)
Builds the frame clause including the modifies clause.
|
protected Term |
FunctionalOperationContractPO.buildFrameClause(java.util.List<LocationVariable> modHeaps,
java.util.Map<Term,Term> heapToAtPre,
ProgramVariable selfVar,
ImmutableList<ProgramVariable> paramVars,
Services services)
Builds the frame clause including the modifies clause.
|
protected Term |
AbstractOperationPO.buildFreePre(ProgramVariable selfVar,
KeYJavaType selfKJT,
ImmutableList<ProgramVariable> paramVars,
java.util.List<LocationVariable> heaps,
Services services)
Builds the "general assumption".
|
protected abstract ImmutableList<StatementBlock> |
AbstractOperationPO.buildOperationBlocks(ImmutableList<LocationVariable> formalParVars,
ProgramVariable selfVar,
ProgramVariable resultVar,
Services services)
Builds the code to execute in different statement blocks.
|
protected ImmutableList<StatementBlock> |
FunctionalOperationContractPO.buildOperationBlocks(ImmutableList<LocationVariable> formalParVars,
ProgramVariable selfVar,
ProgramVariable resultVar,
Services services)
Builds the code to execute in different statement blocks.
|
protected Term |
AbstractOperationPO.buildProgramTerm(ImmutableList<ProgramVariable> paramVars,
ImmutableList<LocationVariable> formalParamVars,
ProgramVariable selfVar,
ProgramVariable resultVar,
ProgramVariable exceptionVar,
java.util.Map<LocationVariable,LocationVariable> atPreVars,
Term postTerm,
ImmutableList<StatementBlock> sb,
Services services)
Creates the
Term which contains the modality including
the complete program to execute. |
protected Term |
AbstractOperationPO.buildUpdate(ImmutableList<ProgramVariable> paramVars,
ImmutableList<LocationVariable> formalParamVars,
java.util.Map<LocationVariable,LocationVariable> atPreVars,
Services services)
Builds the initial updates.
|
protected Term |
FunctionalOperationContractPO.buildUpdate(ImmutableList<ProgramVariable> paramVars,
ImmutableList<LocationVariable> formalParamVars,
java.util.Map<LocationVariable,LocationVariable> atPreVars,
Services services)
Builds the initial updates.
|
InitConfig |
InitConfig.copyWithServices(Services services)
returns a copy of this initial configuration copying the namespaces,
the contained JavaInfo while using the immutable set of taclets in the
copy
|
protected Term |
AbstractOperationPO.createUninterpretedPredicate(ImmutableList<LocationVariable> formalParamVars,
Term exceptionVar,
java.lang.String name,
Services services)
|
protected Term |
AbstractOperationPO.ensureUninterpretedPredicateExists(ImmutableList<ProgramVariable> paramVars,
ImmutableList<LocationVariable> formalParamVars,
ProgramVariable exceptionVar,
java.lang.String name,
Services services)
|
protected abstract Term |
AbstractOperationPO.generateMbyAtPreDef(ProgramVariable selfVar,
ImmutableList<ProgramVariable> paramVars,
Services services) |
protected Term |
FunctionalOperationContractPO.generateMbyAtPreDef(ProgramVariable selfVar,
ImmutableList<ProgramVariable> paramVars,
Services services) |
protected Term |
AbstractPO.generateSelfCreated(java.util.List<LocationVariable> heaps,
IProgramMethod pm,
ProgramVariable selfVar,
Services services)
Generates the general assumption that self is created.
|
protected LocationVariable |
AbstractOperationPO.getBaseHeap(Services services)
Returns the base heap.
|
protected abstract Term |
AbstractOperationPO.getGlobalDefs(LocationVariable heap,
Term heapTerm,
Term selfTerm,
ImmutableList<Term> paramTerms,
Services services) |
protected Term |
FunctionalOperationContractPO.getGlobalDefs(LocationVariable heap,
Term heapTerm,
Term selfTerm,
ImmutableList<Term> paramTerms,
Services services) |
protected abstract Term |
AbstractOperationPO.getPost(java.util.List<LocationVariable> modHeaps,
ProgramVariable selfVar,
ImmutableList<ProgramVariable> paramVars,
ProgramVariable resultVar,
ProgramVariable exceptionVar,
java.util.Map<LocationVariable,LocationVariable> atPreVars,
Services services)
Creates the postcondition.
|
protected Term |
FunctionalOperationContractPO.getPost(java.util.List<LocationVariable> modHeaps,
ProgramVariable selfVar,
ImmutableList<ProgramVariable> paramVars,
ProgramVariable resultVar,
ProgramVariable exceptionVar,
java.util.Map<LocationVariable,LocationVariable> atPreVars,
Services services)
Creates the postcondition.
|
protected abstract Term |
AbstractOperationPO.getPre(java.util.List<LocationVariable> modHeaps,
ProgramVariable selfVar,
ImmutableList<ProgramVariable> paramVars,
java.util.Map<LocationVariable,LocationVariable> atPreVars,
Services services)
Creates the precondition.
|
protected Term |
FunctionalOperationContractPO.getPre(java.util.List<LocationVariable> modHeaps,
ProgramVariable selfVar,
ImmutableList<ProgramVariable> paramVars,
java.util.Map<LocationVariable,LocationVariable> atPreVars,
Services services)
Creates the precondition.
|
protected LocationVariable |
AbstractOperationPO.getSavedHeap(Services services)
Returns the saved heap.
|
Term |
POExtension.modifyPostTerm(InitConfig proofConfig,
Services services,
Term postTerm)
Modifies the post condition.
|
protected Term |
AbstractOperationPO.modifyPostTerm(Services proofServices,
Term post)
Modifies the post condition with help of
POExtension.modifyPostTerm(InitConfig, Services, Term) . |
protected Term |
AbstractOperationPO.newAdditionalUninterpretedPredicate(ImmutableList<LocationVariable> formalParamVars,
Term exceptionVar,
java.lang.String name,
Services services)
Creates a new uninterpreted predicate which is added to
AbstractOperationPO.additionalUninterpretedPredicates . |
protected void |
AbstractPO.register(Function f,
Services services) |
protected void |
AbstractPO.register(ImmutableList<ProgramVariable> pvs,
Services services) |
protected void |
AbstractPO.register(ProgramVariable pv,
Services services) |
Constructor and Description |
---|
InitConfig(Services services) |
ProblemInitializer(ProgressMonitor mon,
Services services,
ProblemInitializer.ProblemInitializerListener listener) |
ProofObligationVars(IProgramMethod pm,
KeYJavaType kjt,
Services services) |
ProofObligationVars(ProofObligationVars orig,
java.lang.String postfix,
Services services) |
ProofObligationVars(StateVars pre,
StateVars post,
Services services) |
ProofObligationVars(StateVars pre,
StateVars post,
Term exceptionParameter,
ImmutableList<Term> formalParams,
Services services) |
Modifier and Type | Method and Description |
---|---|
static TacletApp |
IntermediateProofReplayer.parseSV1(TacletApp app,
SchemaVariable sv,
java.lang.String value,
Services services)
Instantiates a schema variable in the given taclet application.
|
static java.lang.String |
OutputStreamProofSaver.printAnything(java.lang.Object val,
Services services) |
static java.lang.StringBuffer |
OutputStreamProofSaver.printAnything(java.lang.Object val,
Services services,
boolean shortAttrNotation) |
static java.lang.StringBuffer |
OutputStreamProofSaver.printTerm(Term t,
Services serv) |
static java.lang.StringBuffer |
OutputStreamProofSaver.printTerm(Term t,
Services serv,
boolean shortAttrNotation) |
Modifier and Type | Method and Description |
---|---|
Services |
ProofEnvironment.getServicesForEnvironment()
returns the
Services instance for the environment |
Modifier and Type | Method and Description |
---|---|
void |
SpecificationRepository.map(java.util.function.UnaryOperator<Term> op,
Services services)
Applies the specified operator to every contract in this repository.
|
Constructor and Description |
---|
SpecificationRepository(Services services) |
Modifier and Type | Field and Description |
---|---|
protected Services |
SyntacticalReplaceVisitor.services |
Services |
AbstractLoopInvariantRule.LoopInvariantInformation.services
The
Services object. |
Modifier and Type | Method and Description |
---|---|
TacletApp |
TacletApp.addCheckedInstantiation(SchemaVariable sv,
ProgramElement pe,
Services services,
boolean interesting)
checks if the instantiation of
sv with pe is
possible. |
TacletApp |
TacletApp.addCheckedInstantiation(SchemaVariable sv,
Term term,
Services services,
boolean interesting)
creates a new Tacletapp where the SchemaVariable sv is instantiated with
the the given Term term.
|
TacletApp |
TacletApp.addInstantiation(SchemaVariable sv,
Name name,
Services services) |
TacletApp |
NoPosTacletApp.addInstantiation(SchemaVariable sv,
java.lang.Object[] list,
boolean interesting,
Services services) |
TacletApp |
PosTacletApp.addInstantiation(SchemaVariable sv,
java.lang.Object[] list,
boolean interesting,
Services services) |
abstract TacletApp |
TacletApp.addInstantiation(SchemaVariable sv,
java.lang.Object[] list,
boolean interesting,
Services services) |
TacletApp |
NoPosTacletApp.addInstantiation(SchemaVariable sv,
ProgramElement pe,
boolean interesting,
Services services)
adds a new instantiation to this TacletApp
|
TacletApp |
PosTacletApp.addInstantiation(SchemaVariable sv,
ProgramElement pe,
boolean interesting,
Services services)
adds a new instantiation to this TacletApp
|
abstract TacletApp |
TacletApp.addInstantiation(SchemaVariable sv,
ProgramElement pe,
boolean interesting,
Services services)
adds a new instantiation to this TacletApp.
|
TacletApp |
NoPosTacletApp.addInstantiation(SchemaVariable sv,
Term term,
boolean interesting,
Services services)
adds a new instantiation to this TacletApp
|
TacletApp |
PosTacletApp.addInstantiation(SchemaVariable sv,
Term term,
boolean interesting,
Services services)
adds a new instantiation to this TacletApp
|
abstract TacletApp |
TacletApp.addInstantiation(SchemaVariable sv,
Term term,
boolean interesting,
Services services)
adds a new instantiation to this TacletApp
|
TacletApp |
NoPosTacletApp.addInstantiation(SVInstantiations svi,
Services services)
creates a new Taclet application containing all the
instantiations given
by the SVInstantiations and hold the old ones
|
TacletApp |
PosTacletApp.addInstantiation(SVInstantiations svi,
Services services)
creates a new Taclet application containing all the
instantiations given
by the SVInstantiations and the ones of this TacletApp
|
abstract TacletApp |
TacletApp.addInstantiation(SVInstantiations svi,
Services services)
creates a new Taclet application containing all the instantiations given
by the SVInstantiations
|
ImmutableList<Goal> |
BlockContractExternalRule.apply(Goal goal,
Services services,
RuleApp ruleApp) |
ImmutableList<Goal> |
Taclet.apply(Goal goal,
Services services,
RuleApp tacletApp)
applies the given rule application to the specified goal
|
ImmutableList<Goal> |
QueryExpand.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> |
OneStepSimplifier.apply(Goal goal,
Services services,
RuleApp ruleApp) |
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> |
UseDependencyContractRule.apply(Goal goal,
Services services,
RuleApp ruleApp) |
ImmutableList<Goal> |
LoopApplyHeadRule.apply(Goal goal,
Services services,
RuleApp application) |
ImmutableList<Goal> |
UseOperationContractRule.apply(Goal goal,
Services services,
RuleApp ruleApp) |
ImmutableList<Goal> |
LoopScopeInvariantRule.apply(Goal goal,
Services services,
RuleApp ruleApp) |
protected static Term |
AbstractBlockContractRule.buildAfterVar(Term varTerm,
java.lang.String suffix,
Services services) |
protected static ImmutableList<Term> |
AbstractBlockContractRule.buildLocalOutsAtPost(ImmutableList<Term> varTerms,
Services services) |
protected static ImmutableList<Term> |
AbstractBlockContractRule.buildLocalOutsAtPre(ImmutableList<Term> varTerms,
Services services) |
Term |
AuxiliaryContractBuilders.ConditionsAndClausesBuilder.buildSelfConditions(java.util.List<LocationVariable> heaps,
IProgramMethod pm,
KeYJavaType selfKJT,
Term self,
Services services)
Builds the assumptions for the
self variable
(self != null & self.created == true & exactInstance(self) ) |
MatchConditions |
VariableConditionAdapter.check(SchemaVariable var,
SVSubstitute instCandidate,
MatchConditions mc,
Services services) |
MatchConditions |
VariableCondition.check(SchemaVariable var,
SVSubstitute instCandidate,
MatchConditions matchCond,
Services services)
checks if the condition for a correct instantiation is fulfilled
|
abstract boolean |
VariableConditionAdapter.check(SchemaVariable var,
SVSubstitute instCandidate,
SVInstantiations instMap,
Services services)
checks if the condition for a correct instantiation is fulfilled
|
AbstractContractRuleApp |
AbstractContractRuleApp.check(Services services) |
MatchConditions |
TacletMatcher.checkConditions(MatchConditions p_matchconditions,
Services services)
checks the provided matches against the variable conditions of this taclet
It returns the resulting match conditions or
null if the found matches
do not satisfy the variable conditions. |
MatchConditions |
TacletMatcher.checkVariableConditions(SchemaVariable var,
SVSubstitute instantiationCandidate,
MatchConditions matchCond,
Services services)
checks if the conditions for a correct instantiation are satisfied
|
static UseOperationContractRule.Instantiation |
UseOperationContractRule.computeInstantiation(Term focusTerm,
Services services)
Computes instantiation for contract rule on passed focus term.
|
protected static Term |
AbstractLoopInvariantRule.conjunctFreeInv(Services services,
AbstractLoopInvariantRule.Instantiation inst,
java.util.Map<LocationVariable,Term> atPres,
java.util.List<LocationVariable> heapContext)
Creates a conjunction of all free invariant formulas for the
LocationVariable s in heapContext. |
protected static Term |
AbstractLoopInvariantRule.conjunctInv(Services services,
AbstractLoopInvariantRule.Instantiation inst,
java.util.Map<LocationVariable,Term> atPres,
java.util.List<LocationVariable> heapContext)
Creates a conjunction of all invariant formulas for the
LocationVariable s in heapContext. |
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 AbstractLoopInvariantRule.AnonUpdateData |
AbstractLoopInvariantRule.createAnonUpdate(LocationVariable heap,
Term mod,
LoopSpecification inv,
Services services)
Computes the anonymizing update, the loop heap, the base heap, and the
anonymized heap.
|
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.
|
static NoPosTacletApp |
NoPosTacletApp.createFixedNoPosTacletApp(Taclet taclet,
SVInstantiations instantiations,
Services services)
Create TacletApp with immutable "instantiations", i.e.
|
static ImmutableList<IfFormulaInstantiation> |
IfFormulaInstSeq.createList(Sequent p_s,
boolean antec,
Services services) |
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 ProgramVariable |
AbstractAuxiliaryContractRule.createLocalVariable(java.lang.String nameBase,
KeYJavaType type,
Services services) |
static NoPosTacletApp |
NoPosTacletApp.createNoPosTacletApp(Taclet taclet,
MatchConditions matchCond,
Services services) |
static NoPosTacletApp |
NoPosTacletApp.createNoPosTacletApp(Taclet taclet,
SVInstantiations instantiations,
ImmutableList<IfFormulaInstantiation> ifInstantiations,
Services services) |
static NoPosTacletApp |
NoPosTacletApp.createNoPosTacletApp(Taclet taclet,
SVInstantiations instantiations,
Services services)
creates a NoPosTacletApp for the given taclet with some known
instantiations and CHECKS variable conditions as well as it
resolves collisions
The ifInstantiations parameter is not
matched against the if sequence, but only stored.
|
static PosTacletApp |
PosTacletApp.createPosTacletApp(FindTaclet taclet,
MatchConditions matchCond,
PosInOccurrence pos,
Services services) |
static PosTacletApp |
PosTacletApp.createPosTacletApp(FindTaclet taclet,
SVInstantiations instantiations,
ImmutableList<IfFormulaInstantiation> ifInstantiations,
PosInOccurrence pos,
Services services) |
static PosTacletApp |
PosTacletApp.createPosTacletApp(FindTaclet taclet,
SVInstantiations instantiations,
PosInOccurrence pos,
Services services)
creates a PosTacletApp for the given taclet with some known instantiations
and a position information
and CHECKS variable conditions as well as it resolves
collisions
The ifInstantiations parameter is not
matched against the if sequence, but only stored.
|
TacletApp |
TacletApp.createSkolemConstant(java.lang.String instantiation,
SchemaVariable sv,
boolean interesting,
Services services)
Create a new constant named "instantiation" and instantiate "sv" with.
|
TacletApp |
TacletApp.createSkolemConstant(java.lang.String instantiation,
SchemaVariable sv,
Sort sort,
boolean interesting,
Services services) |
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.
|
Term |
QueryExpand.evaluateQueries(Services services,
Term term,
boolean positiveContext,
boolean allowExpandBelowInstQuantifier)
Apply "evaluate query" to the queries that occur in
term . |
ImmutableList<Goal> |
AbstractBuiltInRuleApp.execute(Goal goal,
Services services)
applies the specified rule at the specified position
if all schema variables have been instantiated
|
ImmutableList<Goal> |
TacletApp.execute(Goal goal,
Services services)
applies the specified rule at the specified position if all schema
variables have been instantiated
|
ImmutableList<Goal> |
RuleApp.execute(Goal goal,
Services services)
applies the specified rule at the specified position
if all schema variables have been instantiated
|
ImmutableList<TacletApp> |
TacletApp.findIfFormulaInstantiations(Sequent p_seq,
Services p_services)
Find all possible instantiations of the if sequent formulas within the
sequent "p_seq".
|
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<FunctionalOperationContract> |
UseOperationContractRule.getApplicableContracts(UseOperationContractRule.Instantiation inst,
Services services)
Returns the operation contracts which are applicable for the passed instantiation.
|
ProgramElement |
AbstractProgramElement.getConcreteProgramElement(Services services) |
SchemaVariable |
Taclet.getNameCorrespondent(SchemaVariable p,
Services services)
Find a schema variable that could be used to choose a name for
an instantiation (a new variable or constant) of "p"
|
IObserverFunction |
UseDependencyContractApp.getObserverFunction(Services services) |
abstract IObserverFunction |
AbstractContractRuleApp.getObserverFunction(Services services) |
IObserverFunction |
ContractRuleApp.getObserverFunction(Services services) |
ProgramElement |
TacletApp.getProgramElement(java.lang.String instantiation,
SchemaVariable sv,
Services services) |
SequentFormula |
RewriteTaclet.getRewriteResult(Goal goal,
TermLabelState termLabelState,
Services services,
TacletApp app) |
static java.util.List<PosInOccurrence> |
UseDependencyContractRule.getSteps(java.util.List<LocationVariable> heapContext,
PosInOccurrence pos,
Sequent seq,
Services services) |
protected boolean |
AbstractBlockContractRule.Instantiator.hasApplicableContracts(Services services,
JavaStatement statement,
Modality modality,
Goal goal) |
protected abstract boolean |
AbstractAuxiliaryContractRule.Instantiator.hasApplicableContracts(Services services,
JavaStatement element,
Modality modality,
Goal goal) |
protected boolean |
AbstractLoopContractRule.Instantiator.hasApplicableContracts(Services services,
JavaStatement statement,
Modality modality,
Goal goal) |
protected static AbstractLoopInvariantRule.Instantiation |
AbstractLoopInvariantRule.instantiate(LoopInvariantBuiltInRuleApp app,
Services services)
Constructs the
AbstractLoopInvariantRule.Instantiation object containing the relevant
parameters for this LoopScopeInvariantRule application. |
AbstractAuxiliaryContractRule.Instantiation |
AbstractBlockContractRule.instantiate(Term formula,
Goal goal,
Services services) |
AbstractAuxiliaryContractRule.Instantiation |
AbstractLoopContractRule.instantiate(Term formula,
Goal goal,
Services services) |
protected static <T> Term |
AbstractLoopInvariantRule.mapAndConjunct(Services services,
java.util.function.Function<T,Term> fct,
java.util.List<T> listOfT)
Creates a conjunction of
Term s that are produced by fct from the
elements in listOfT. |
NoPosTacletApp |
NoPosTacletApp.matchFind(PosInOccurrence pos,
Services services)
PRECONDITION: ifFormulaInstantiations () == null &&
( pos == null || termConstraint.isSatisfiable () )
|
NoPosTacletApp |
NoPosTacletApp.matchFind(PosInOccurrence pos,
Services services,
Term t) |
MatchConditions |
TacletMatcher.matchFind(Term term,
MatchConditions matchCond,
Services services)
matches the given term against the taclet's find term
if the taclet has no find term or the match is unsuccessful
null
is returned |
IfMatchResult |
TacletMatcher.matchIf(ImmutableList<IfFormulaInstantiation> p_toMatch,
Term p_template,
MatchConditions p_matchCond,
Services p_services)
Match the given template (which is probably a formula of the if
sequence) against a list of constraint formulas (probably the
formulas of the antecedent or the succedent), starting with the
given instantiations and constraint p_matchCond.
|
MatchConditions |
TacletMatcher.matchIf(java.lang.Iterable<IfFormulaInstantiation> p_toMatch,
MatchConditions p_matchCond,
Services p_services)
Match the whole if sequent using the given list of
instantiations of all if sequent formulas, starting with the
instantiations given by p_matchCond.
|
MatchConditions |
TacletMatcher.matchSV(SchemaVariable sv,
ProgramElement term,
MatchConditions matchCond,
Services services)
|
MatchConditions |
TacletMatcher.matchSV(SchemaVariable sv,
Term term,
MatchConditions matchCond,
Services services)
|
TacletApp |
TacletApp.prepareUserInstantiation(Services services)
checks if there are name conflicts (i.e.
|
Pair<Term,Term> |
QueryExpand.queryEvalTerm(Services services,
Term query,
LogicVariable[] instVars)
Creates an invocation of a query in a modal operator and stores the value in a
new symbol.
|
protected static void |
AbstractAuxiliaryContractRule.register(ProgramVariable pv,
Services services)
Adds
pv to the sevices ' program variable namespace. |
protected static SVInstantiations |
TacletApp.replaceInstantiation(Taclet taclet,
SVInstantiations insts,
SchemaVariable varSV,
Services services)
returns a new SVInstantiations that modifies the given SVInstantiations
insts at the bound SchemaVariable varSV to a new LogicVariable.
|
protected static SVInstantiations |
TacletApp.resolveCollisionVarSV(Taclet taclet,
SVInstantiations insts,
Services services)
resolves collisions between bound SchemaVariables in an SVInstantiation
|
LoopSpecification |
LoopInvariantBuiltInRuleApp.retrieveLoopInvariantFromSpecification(Services services) |
protected TacletApp |
NoPosTacletApp.setAllInstantiations(MatchConditions mc,
ImmutableList<IfFormulaInstantiation> ifInstantiations,
Services services)
creates a new Taclet application containing all the
instantiations, constraints, new metavariables and if formula
instantiations given and forget the old ones
|
protected TacletApp |
PosTacletApp.setAllInstantiations(MatchConditions mc,
ImmutableList<IfFormulaInstantiation> ifInstantiations,
Services services)
creates a new Taclet application containing all the
instantiations, constraints, new metavariables and if formula
instantiations given and forget the old ones
|
protected abstract TacletApp |
TacletApp.setAllInstantiations(MatchConditions mc,
ImmutableList<IfFormulaInstantiation> ifInstantiations,
Services services)
creates a new Taclet application containing all the instantiations,
constraints, new metavariables and if formula instantiations given and
forget the old ones
|
TacletApp |
TacletApp.setIfFormulaInstantiations(ImmutableList<IfFormulaInstantiation> p_list,
Services p_services)
Creates a new Taclet application by matching the given formulas against
the formulas of the if sequent, adding SV instantiations, constraints and
metavariables as needed.
|
protected TacletApp |
NoPosTacletApp.setInstantiation(SVInstantiations svi,
Services services)
creates a new Taclet application containing all the
instantiations given
by the SVInstantiations and forget the ones in this TacletApp
|
protected TacletApp |
PosTacletApp.setInstantiation(SVInstantiations svi,
Services services)
creates a new Taclet application containing all the
instantiations given
by the SVInstantiations and forget the old ones.
|
protected abstract TacletApp |
TacletApp.setInstantiation(SVInstantiations svi,
Services services)
creates a new Taclet application containing all the instantiations given
by the SVInstantiations and forget the old ones
|
TacletApp |
NoPosTacletApp.setMatchConditions(MatchConditions mc,
Services services)
creates a new Taclet application containing all the
instantiations, constraints and new metavariables given
by the mc object and forget the old ones
|
TacletApp |
PosTacletApp.setMatchConditions(MatchConditions mc,
Services services)
creates a new Taclet application containing all the
instantiations, constraints and new metavariables given
by the mc object and forget the old ones
|
abstract TacletApp |
TacletApp.setMatchConditions(MatchConditions mc,
Services services)
creates a new Taclet application containing all the instantiations,
constraints and new metavariables given by the mc object and forget the
old ones
|
PosTacletApp |
TacletApp.setPosInOccurrence(PosInOccurrence pos,
Services services)
returns a new PosTacletApp that is equal to this TacletApp except that
the position is set to the given PosInOccurrence.
|
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) |
java.lang.String |
IfFormulaInstSeq.toString(Services services) |
java.lang.String |
IfFormulaInstantiation.toString(Services services) |
java.lang.String |
IfFormulaInstDirect.toString(Services services) |
TacletApp |
TacletApp.tryToInstantiate(Services services) |
TacletApp |
TacletApp.tryToInstantiateAsMuchAsPossible(Services services) |
UseDependencyContractApp |
UseDependencyContractApp.tryToInstantiateContract(Services services) |
Modifier and Type | Method and Description |
---|---|
MatchConditions |
FieldTypeToSortCondition.check(SchemaVariable var,
SVSubstitute svSubst,
MatchConditions matchCond,
Services services) |
MatchConditions |
DropEffectlessElementariesCondition.check(SchemaVariable var,
SVSubstitute instCandidate,
MatchConditions mc,
Services services) |
MatchConditions |
NewJumpLabelCondition.check(SchemaVariable var,
SVSubstitute instCandidate,
MatchConditions matchCond,
Services services) |
MatchConditions |
IsLabeledCondition.check(SchemaVariable sv,
SVSubstitute instCandidate,
MatchConditions matchCond,
Services services) |
MatchConditions |
SimplifyIfThenElseUpdateCondition.check(SchemaVariable var,
SVSubstitute instCandidate,
MatchConditions mc,
Services services) |
MatchConditions |
LoopVariantCondition.check(SchemaVariable var,
SVSubstitute instCandidate,
MatchConditions matchCond,
Services services) |
MatchConditions |
StoreStmtInCondition.check(SchemaVariable sv,
SVSubstitute instCandidate,
MatchConditions matchCond,
Services services) |
MatchConditions |
ObserverCondition.check(SchemaVariable var,
SVSubstitute instCandidate,
MatchConditions mc,
Services services) |
MatchConditions |
HasLoopInvariantCondition.check(SchemaVariable var,
SVSubstitute instCandidate,
MatchConditions matchCond,
Services services) |
MatchConditions |
LoopFreeInvariantCondition.check(SchemaVariable var,
SVSubstitute instCandidate,
MatchConditions matchCond,
Services services) |
MatchConditions |
EqualUniqueCondition.check(SchemaVariable var,
SVSubstitute instCandidate,
MatchConditions mc,
Services services) |
MatchConditions |
ApplyUpdateOnRigidCondition.check(SchemaVariable var,
SVSubstitute instCandidate,
MatchConditions mc,
Services services) |
MatchConditions |
JavaTypeToSortCondition.check(SchemaVariable var,
SVSubstitute svSubst,
MatchConditions matchCond,
Services services) |
MatchConditions |
LoopInvariantCondition.check(SchemaVariable var,
SVSubstitute instCandidate,
MatchConditions matchCond,
Services services) |
MatchConditions |
DropEffectlessStoresCondition.check(SchemaVariable var,
SVSubstitute instCandidate,
MatchConditions mc,
Services services) |
MatchConditions |
StoreTermInCondition.check(SchemaVariable sv,
SVSubstitute instCandidate,
MatchConditions matchCond,
Services services) |
MatchConditions |
SameObserverCondition.check(SchemaVariable var,
SVSubstitute instCandidate,
MatchConditions mc,
Services services) |
boolean |
AlternativeVariableCondition.check(SchemaVariable var,
SVSubstitute subst,
SVInstantiations svInst,
Services services)
check whether any of the two delegates apply
|
boolean |
ContainsAssignmentCondition.check(SchemaVariable var,
SVSubstitute instCandidate,
SVInstantiations instMap,
Services services)
checks if the condition for a correct instantiation is fulfilled
|
boolean |
AbstractOrInterfaceType.check(SchemaVariable var,
SVSubstitute instCandidate,
SVInstantiations instMap,
Services services) |
boolean |
MayExpandMethodCondition.check(SchemaVariable var,
SVSubstitute subst,
SVInstantiations svInst,
Services services) |
boolean |
TypeComparisonCondition.check(SchemaVariable var,
SVSubstitute subst,
SVInstantiations svInst,
Services services) |
boolean |
ArrayComponentTypeCondition.check(SchemaVariable var,
SVSubstitute candidate,
SVInstantiations svInst,
Services services) |
boolean |
DifferentInstantiationCondition.check(SchemaVariable var,
SVSubstitute candidate,
SVInstantiations svInst,
Services services) |
boolean |
ArrayTypeCondition.check(SchemaVariable var,
SVSubstitute candidate,
SVInstantiations svInst,
Services services) |
boolean |
IsThisReference.check(SchemaVariable var,
SVSubstitute instCandidate,
SVInstantiations instMap,
Services services) |
boolean |
EnumTypeCondition.check(SchemaVariable var,
SVSubstitute candidate,
SVInstantiations svInst,
Services services) |
boolean |
StaticFieldCondition.check(SchemaVariable var,
SVSubstitute instCandidate,
SVInstantiations instMap,
Services services) |
boolean |
TermLabelCondition.check(SchemaVariable var,
SVSubstitute instCandidate,
SVInstantiations instMap,
Services services) |
boolean |
TypeCondition.check(SchemaVariable p_var,
SVSubstitute candidate,
SVInstantiations svInst,
Services services) |
boolean |
LocalVariableCondition.check(SchemaVariable var,
SVSubstitute candidate,
SVInstantiations svInst,
Services services) |
boolean |
SubFormulaCondition.check(SchemaVariable var,
SVSubstitute instCandidate,
SVInstantiations instMap,
Services services) |
boolean |
MetaDisjointCondition.check(SchemaVariable var,
SVSubstitute subst,
SVInstantiations svInst,
Services services) |
boolean |
DifferentFields.check(SchemaVariable var,
SVSubstitute instCandidate,
SVInstantiations instMap,
Services services) |
boolean |
ConstantCondition.check(SchemaVariable var,
SVSubstitute instCandidate,
SVInstantiations instMap,
Services services) |
boolean |
FinalReferenceCondition.check(SchemaVariable var,
SVSubstitute subst,
SVInstantiations svInst,
Services services) |
boolean |
FreeLabelInVariableCondition.check(SchemaVariable var,
SVSubstitute instCandidate,
SVInstantiations instMap,
Services services) |
boolean |
StaticMethodCondition.check(SchemaVariable var,
SVSubstitute subst,
SVInstantiations svInst,
Services services) |
boolean |
EnumConstantCondition.check(SchemaVariable var,
SVSubstitute subst,
SVInstantiations svInst,
Services services) |
boolean |
ArrayLengthCondition.check(SchemaVariable var,
SVSubstitute subst,
SVInstantiations svInst,
Services services) |
boolean |
StaticReferenceCondition.check(SchemaVariable var,
SVSubstitute subst,
SVInstantiations svInst,
Services services) |
abstract Sort |
TypeResolver.resolveSort(SchemaVariable sv,
SVSubstitute instCandidate,
SVInstantiations instMap,
Services services) |
Sort |
TypeResolver.GenericSortResolver.resolveSort(SchemaVariable sv,
SVSubstitute instCandidate,
SVInstantiations instMap,
Services services) |
Sort |
TypeResolver.NonGenericSortResolver.resolveSort(SchemaVariable sv,
SVSubstitute instCandidate,
SVInstantiations instMap,
Services services) |
Sort |
TypeResolver.ElementTypeResolverForSV.resolveSort(SchemaVariable sv,
SVSubstitute instCandidate,
SVInstantiations instMap,
Services services) |
Sort |
TypeResolver.ContainerTypeResolver.resolveSort(SchemaVariable sv,
SVSubstitute instCandidate,
SVInstantiations instMap,
Services services) |
Modifier and Type | Method and Description |
---|---|
ImmutableList<Goal> |
RuleExecutor.apply(Goal goal,
Services services,
RuleApp ruleApp)
applies the given rule application to the specified goal
|
Modifier and Type | Method and Description |
---|---|
protected void |
TacletExecutor.addToAntec(Semisequent semi,
TermLabelState termLabelState,
Taclet.TacletLabelHint labelHint,
SequentChangeInfo currentSequent,
PosInOccurrence pos,
PosInOccurrence applicationPosInOccurrence,
MatchConditions matchCond,
Goal goal,
RuleApp tacletApp,
Services services)
adds SequentFormula to antecedent depending on
position information (if none is handed over it is added at the
head of the antecedent).
|
protected void |
TacletExecutor.addToSucc(Semisequent semi,
TermLabelState termLabelState,
Taclet.TacletLabelHint labelHint,
SequentChangeInfo currentSequent,
PosInOccurrence pos,
PosInOccurrence applicationPosInOccurrence,
MatchConditions matchCond,
Goal goal,
RuleApp ruleApp,
Services services)
adds SequentFormula to succedent depending on
position information (if none is handed over it is added at the
head of the succedent).
|
ImmutableList<Goal> |
NoFindTacletExecutor.apply(Goal goal,
Services services,
RuleApp ruleApp)
the rule is applied on the given goal using the
information of rule application.
|
abstract ImmutableList<Goal> |
TacletExecutor.apply(Goal goal,
Services services,
RuleApp tacletApp)
applies the given rule application to the specified goal
|
ImmutableList<Goal> |
FindTacletExecutor.apply(Goal goal,
Services services,
RuleApp ruleApp)
the rule is applied on the given goal using the
information of rule application.
|
protected void |
RewriteTacletExecutor.applyAdd(Sequent add,
TermLabelState termLabelState,
SequentChangeInfo currentSequent,
PosInOccurrence whereToAdd,
PosInOccurrence posOfFind,
MatchConditions matchCond,
Goal goal,
RuleApp ruleApp,
Services services)
adds the sequent of the add part of the Taclet to the goal sequent
|
protected void |
SuccTacletExecutor.applyAdd(Sequent add,
TermLabelState termLabelState,
SequentChangeInfo currentSequent,
PosInOccurrence whereToAdd,
PosInOccurrence posOfFind,
MatchConditions matchCond,
Goal goal,
RuleApp ruleApp,
Services services)
applies the
add -expressions of taclet goal descriptions |
protected abstract void |
FindTacletExecutor.applyAdd(Sequent add,
TermLabelState termLabelState,
SequentChangeInfo currentSequent,
PosInOccurrence whereToAdd,
PosInOccurrence posOfFind,
MatchConditions matchCond,
Goal goal,
RuleApp ruleApp,
Services services)
applies the
add -expressions of taclet goal descriptions |
protected void |
AntecTacletExecutor.applyAdd(Sequent add,
TermLabelState termLabelState,
SequentChangeInfo currentSequent,
PosInOccurrence whereToAdd,
PosInOccurrence posOfFind,
MatchConditions matchCond,
Goal goal,
RuleApp ruleApp,
Services services)
applies the
add -expressions of taclet goal descriptions |
protected void |
NoFindTacletExecutor.applyAdd(TermLabelState termLabelState,
Sequent add,
SequentChangeInfo currentSequent,
Services services,
MatchConditions matchCond,
Goal goal,
RuleApp ruleApp)
adds the sequent of the add part of the Taclet to the goal sequent
|
protected void |
TacletExecutor.applyAddProgVars(ImmutableSet<SchemaVariable> pvs,
SequentChangeInfo currentSequent,
Goal goal,
PosInOccurrence posOfFind,
Services services,
MatchConditions matchCond) |
protected void |
TacletExecutor.applyAddrule(ImmutableList<Taclet> rules,
Goal goal,
Services services,
MatchConditions matchCond)
adds the given rules (i.e.
|
protected void |
RewriteTacletExecutor.applyReplacewith(TacletGoalTemplate gt,
TermLabelState termLabelState,
SequentChangeInfo currentSequent,
PosInOccurrence posOfFind,
MatchConditions matchCond,
Goal goal,
RuleApp ruleApp,
Services services)
applies the
replacewith -expression of taclet goal descriptions |
protected void |
SuccTacletExecutor.applyReplacewith(TacletGoalTemplate gt,
TermLabelState termLabelState,
SequentChangeInfo currentSequent,
PosInOccurrence posOfFind,
MatchConditions matchCond,
Goal goal,
RuleApp ruleApp,
Services services)
applies the
replacewith -expression of taclet goal descriptions |
protected abstract void |
FindTacletExecutor.applyReplacewith(TacletGoalTemplate gt,
TermLabelState termLabelState,
SequentChangeInfo currentSequent,
PosInOccurrence posOfFind,
MatchConditions matchCond,
Goal goal,
RuleApp ruleApp,
Services services)
applies the
replacewith -expression of taclet goal descriptions |
protected void |
AntecTacletExecutor.applyReplacewith(TacletGoalTemplate gt,
TermLabelState termLabelState,
SequentChangeInfo currentSequent,
PosInOccurrence posOfFind,
MatchConditions matchCond,
Goal goal,
RuleApp ruleApp,
Services services)
applies the
replacewith -expression of taclet goal descriptions |
SequentFormula |
RewriteTacletExecutor.getRewriteResult(Goal goal,
TermLabelState termLabelState,
Services services,
TacletApp app) |
protected ImmutableList<SequentFormula> |
TacletExecutor.instantiateSemisequent(Semisequent semi,
TermLabelState termLabelState,
Taclet.TacletLabelHint labelHint,
PosInOccurrence applicationPosInOccurrence,
MatchConditions matchCond,
Goal goal,
RuleApp tacletApp,
Services services)
instantiates the given semisequent with the instantiations found in
Matchconditions
|
protected void |
TacletExecutor.replaceAtPos(Semisequent semi,
TermLabelState termLabelState,
SequentChangeInfo currentSequent,
PosInOccurrence pos,
MatchConditions matchCond,
Taclet.TacletLabelHint labelHint,
Goal goal,
RuleApp ruleApp,
Services services)
replaces the constrained formula at the given position with the first
formula in the given semisequent and adds possible other formulas of the
semisequent starting at the position
|
protected Term |
TacletExecutor.syntacticalReplace(Term term,
TermLabelState termLabelState,
Taclet.TacletLabelHint labelHint,
PosInOccurrence applicationPosInOccurrence,
MatchConditions mc,
Goal goal,
RuleApp ruleApp,
Services services)
a new term is created by replacing variables of term whose replacement is
found in the given SVInstantiations
|
Modifier and Type | Method and Description |
---|---|
SVInstantiations |
SVInstantiations.add(GenericSortCondition p_c,
Services services)
Add the given additional condition for the generic sort instantiations
|
SVInstantiations |
SVInstantiations.add(ModalOperatorSV sv,
Operator op,
Services services) |
SVInstantiations |
SVInstantiations.add(PosInProgram prefix,
PosInProgram postfix,
ExecutionContext activeStatementContext,
ProgramElement pe,
Services services)
adds the given pair to the instantiations for the context.If the context
has been instantiated already, the new pair is taken without a warning.
|
SVInstantiations |
SVInstantiations.add(SchemaVariable sv,
ImmutableArray<TermLabel> labels,
Services services) |
SVInstantiations |
SVInstantiations.add(SchemaVariable sv,
InstantiationEntry<?> entry,
Services services)
adds the given pair to the instantiations.
|
SVInstantiations |
SVInstantiations.add(SchemaVariable sv,
ProgramElement pe,
Services services)
adds the given pair to the instantiations.
|
SVInstantiations |
SVInstantiations.add(SchemaVariable sv,
ProgramList pes,
Services services) |
SVInstantiations |
SVInstantiations.add(SchemaVariable sv,
Term subst,
Services services)
adds the given pair to the instantiations.
|
SVInstantiations |
SVInstantiations.addInteresting(SchemaVariable sv,
InstantiationEntry<?> entry,
Services services) |
SVInstantiations |
SVInstantiations.addInteresting(SchemaVariable sv,
Name name,
Services services) |
SVInstantiations |
SVInstantiations.addInteresting(SchemaVariable sv,
ProgramElement pe,
Services services) |
SVInstantiations |
SVInstantiations.addInteresting(SchemaVariable sv,
Term subst,
Services services) |
SVInstantiations |
SVInstantiations.addInterestingList(SchemaVariable sv,
java.lang.Object[] list,
Services services) |
SVInstantiations |
SVInstantiations.addList(SchemaVariable sv,
java.lang.Object[] list,
Services services) |
static GenericSortInstantiations |
GenericSortInstantiations.create(ImmutableList<GenericSort> p_sorts,
ImmutableList<GenericSortCondition> p_conditions,
Services services)
Create an object that holds instantiations of the generic sorts
"p_sorts" satisfying the conditions "p_conditions"
|
static GenericSortInstantiations |
GenericSortInstantiations.create(java.util.Iterator<ImmutableMapEntry<SchemaVariable,InstantiationEntry<?>>> p_instantiations,
ImmutableList<GenericSortCondition> p_conditions,
Services services)
Create an object that solves the conditions given by the
instantiation iterator, i.e.
|
Term |
SVInstantiations.getTermInstantiation(SchemaVariable sv,
ExecutionContext ec,
Services services)
returns the instantiation of the given SchemaVariable as Term.
|
SVInstantiations |
SVInstantiations.makeInteresting(SchemaVariable sv,
Services services)
adds the schemvariable to the set of interesting ones
|
SVInstantiations |
SVInstantiations.replace(PosInProgram prefix,
PosInProgram postfix,
ExecutionContext activeStatementContext,
ProgramElement pe,
Services services)
replaces the given pair in the instantiations.
|
SVInstantiations |
SVInstantiations.replace(SchemaVariable sv,
ImmutableArray<ProgramElement> pes,
Services services)
replaces the given pair in the instantiations.
|
SVInstantiations |
SVInstantiations.replace(SchemaVariable sv,
InstantiationEntry<?> entry,
Services services)
replaces the given pair in the instantiations.
|
SVInstantiations |
SVInstantiations.replace(SchemaVariable sv,
ProgramElement pe,
Services services)
replaces the given pair in the instantiations.
|
SVInstantiations |
SVInstantiations.replace(SchemaVariable sv,
Term term,
Services services)
replaces the given pair in the instantiations.
|
SVInstantiations |
SVInstantiations.union(SVInstantiations other,
Services services) |
Modifier and Type | Method and Description |
---|---|
TermLabelRefactoring.RefactoringScope |
TermLabelRefactoring.defineRefactoringScope(TermLabelState state,
Services services,
PosInOccurrence applicationPosInOccurrence,
Term applicationTerm,
Rule rule,
Goal goal,
java.lang.Object hint,
Term tacletTerm)
Defines if a refactoring is required and if so in which
TermLabelRefactoring.RefactoringScope . |
TermLabelRefactoring.RefactoringScope |
OriginTermLabelRefactoring.defineRefactoringScope(TermLabelState state,
Services services,
PosInOccurrence applicationPosInOccurrence,
Term applicationTerm,
Rule rule,
Goal goal,
java.lang.Object hint,
Term tacletTerm) |
TermLabelRefactoring.RefactoringScope |
FormulaTermLabelRefactoring.defineRefactoringScope(TermLabelState state,
Services services,
PosInOccurrence applicationPosInOccurrence,
Term applicationTerm,
Rule rule,
Goal goal,
java.lang.Object hint,
Term tacletTerm)
Defines if a refactoring is required and if so in which
TermLabelRefactoring.RefactoringScope . |
TermLabelRefactoring.RefactoringScope |
RemoveInCheckBranchesTermLabelRefactoring.defineRefactoringScope(TermLabelState state,
Services services,
PosInOccurrence applicationPosInOccurrence,
Term applicationTerm,
Rule rule,
Goal goal,
java.lang.Object hint,
Term tacletTerm)
Defines if a refactoring is required and if so in which
TermLabelRefactoring.RefactoringScope . |
TermLabel |
OriginTermLabelPolicy.keepLabel(TermLabelState state,
Services services,
PosInOccurrence applicationPosInOccurrence,
Term applicationTerm,
Rule rule,
Goal goal,
java.lang.Object hint,
Term tacletTerm,
Operator newTermOp,
ImmutableArray<Term> newTermSubs,
ImmutableArray<QuantifiableVariable> newTermBoundVars,
JavaBlock newTermJavaBlock,
ImmutableArray<TermLabel> newTermOriginalLabels,
TermLabel label) |
TermLabel |
TermLabelPolicy.keepLabel(TermLabelState state,
Services services,
PosInOccurrence applicationPosInOccurrence,
Term applicationTerm,
Rule rule,
Goal goal,
java.lang.Object hint,
Term tacletTerm,
Operator newTermOp,
ImmutableArray<Term> newTermSubs,
ImmutableArray<QuantifiableVariable> newTermBoundVars,
JavaBlock newTermJavaBlock,
ImmutableArray<TermLabel> newTermOriginalLabels,
TermLabel label)
|
TermLabel |
PerpetualTermLabelPolicy.keepLabel(TermLabelState state,
Services services,
PosInOccurrence applicationPosInOccurrence,
Term applicationTerm,
Rule rule,
Goal goal,
java.lang.Object hint,
Term tacletTerm,
Operator newTermOp,
ImmutableArray<Term> newTermSubs,
ImmutableArray<QuantifiableVariable> newTermBoundVars,
JavaBlock newTermJavaBlock,
ImmutableArray<TermLabel> newTermOriginalLabels,
TermLabel label) |
TermLabel |
StayOnOperatorTermLabelPolicy.keepLabel(TermLabelState state,
Services services,
PosInOccurrence applicationPosInOccurrence,
Term applicationTerm,
Rule rule,
Goal goal,
java.lang.Object hint,
Term tacletTerm,
Operator newTermOp,
ImmutableArray<Term> newTermSubs,
ImmutableArray<QuantifiableVariable> newTermBoundVars,
JavaBlock newTermJavaBlock,
ImmutableArray<TermLabel> newTermOriginalLabels,
TermLabel label)
|
TermLabel |
StayOnFormulaTermLabelPolicy.keepLabel(TermLabelState state,
Services services,
PosInOccurrence applicationPosInOccurrence,
Term applicationTerm,
Rule rule,
Goal goal,
java.lang.Object hint,
Term tacletTerm,
Operator newTermOp,
ImmutableArray<Term> newTermSubs,
ImmutableArray<QuantifiableVariable> newTermBoundVars,
JavaBlock newTermJavaBlock,
ImmutableArray<TermLabel> newTermOriginalLabels,
TermLabel label)
|
protected void |
FormulaTermLabelRefactoring.refactorInCaseOfNewIdRequired(TermLabelState state,
Goal goal,
Term term,
Services services,
java.util.List<TermLabel> labels)
Refactors in case that the inner most label needs a new ID.
|
void |
TermLabelRefactoring.refactorLabels(TermLabelState state,
Services services,
PosInOccurrence applicationPosInOccurrence,
Term applicationTerm,
Rule rule,
Goal goal,
java.lang.Object hint,
Term tacletTerm,
Term term,
java.util.List<TermLabel> labels)
This method is used to refactor the labels of the given
Term . |
void |
OriginTermLabelRefactoring.refactorLabels(TermLabelState state,
Services services,
PosInOccurrence applicationPosInOccurrence,
Term applicationTerm,
Rule rule,
Goal goal,
java.lang.Object hint,
Term tacletTerm,
Term term,
java.util.List<TermLabel> labels) |
void |
FormulaTermLabelRefactoring.refactorLabels(TermLabelState state,
Services services,
PosInOccurrence applicationPosInOccurrence,
Term applicationTerm,
Rule rule,
Goal goal,
java.lang.Object hint,
Term tacletTerm,
Term term,
java.util.List<TermLabel> labels)
This method is used to refactor the labels of the given
Term . |
void |
RemoveInCheckBranchesTermLabelRefactoring.refactorLabels(TermLabelState state,
Services services,
PosInOccurrence applicationPosInOccurrence,
Term applicationTerm,
Rule rule,
Goal goal,
java.lang.Object hint,
Term tacletTerm,
Term term,
java.util.List<TermLabel> labels)
This method is used to refactor the labels of the given
Term . |
protected void |
FormulaTermLabelRefactoring.refactorSequentFormulas(TermLabelState state,
Services services,
Term term,
java.util.List<TermLabel> labels)
Refactors the specified
SequentFormula s. |
protected void |
FormulaTermLabelRefactoring.refactorSpecificationApplication(Term term,
Goal goal,
Services services,
java.util.List<TermLabel> labels,
java.lang.Object hint)
Refactors a specification application.
|
void |
TermLabelUpdate.updateLabels(TermLabelState state,
Services services,
PosInOccurrence applicationPosInOccurrence,
Term applicationTerm,
Term modalityTerm,
Rule rule,
RuleApp ruleApp,
java.lang.Object hint,
Term tacletTerm,
Operator newTermOp,
ImmutableArray<Term> newTermSubs,
ImmutableArray<QuantifiableVariable> newTermBoundVars,
JavaBlock newTermJavaBlock,
java.util.Set<TermLabel> labels)
|
void |
FormulaTermLabelUpdate.updateLabels(TermLabelState state,
Services services,
PosInOccurrence applicationPosInOccurrence,
Term applicationTerm,
Term modalityTerm,
Rule rule,
RuleApp ruleApp,
java.lang.Object hint,
Term tacletTerm,
Operator newTermOp,
ImmutableArray<Term> newTermSubs,
ImmutableArray<QuantifiableVariable> newTermBoundVars,
JavaBlock newTermJavaBlock,
java.util.Set<TermLabel> labels)
|
void |
LoopBodyTermLabelUpdate.updateLabels(TermLabelState state,
Services services,
PosInOccurrence applicationPosInOccurrence,
Term applicationTerm,
Term modalityTerm,
Rule rule,
RuleApp ruleApp,
java.lang.Object hint,
Term tacletTerm,
Operator newTermOp,
ImmutableArray<Term> newTermSubs,
ImmutableArray<QuantifiableVariable> newTermBoundVars,
JavaBlock newTermJavaBlock,
java.util.Set<TermLabel> labels)
|
void |
BlockContractValidityTermLabelUpdate.updateLabels(TermLabelState state,
Services services,
PosInOccurrence applicationPosInOccurrence,
Term applicationTerm,
Term modalityTerm,
Rule rule,
RuleApp ruleApp,
java.lang.Object hint,
Term tacletTerm,
Operator newTermOp,
ImmutableArray<Term> newTermSubs,
ImmutableArray<QuantifiableVariable> newTermBoundVars,
JavaBlock newTermJavaBlock,
java.util.Set<TermLabel> labels)
|
void |
SymbolicExecutionTermLabelUpdate.updateLabels(TermLabelState state,
Services services,
PosInOccurrence applicationPosInOccurrence,
Term applicationTerm,
Term modalityTerm,
Rule rule,
RuleApp ruleApp,
java.lang.Object hint,
Term tacletTerm,
Operator newTermOp,
ImmutableArray<Term> newTermSubs,
ImmutableArray<QuantifiableVariable> newTermBoundVars,
JavaBlock newTermJavaBlock,
java.util.Set<TermLabel> labels)
|
void |
LoopInvariantNormalBehaviorTermLabelUpdate.updateLabels(TermLabelState state,
Services services,
PosInOccurrence applicationPosInOccurrence,
Term applicationTerm,
Term modalityTerm,
Rule rule,
RuleApp ruleApp,
java.lang.Object hint,
Term tacletTerm,
Operator newTermOp,
ImmutableArray<Term> newTermSubs,
ImmutableArray<QuantifiableVariable> newTermBoundVars,
JavaBlock newTermJavaBlock,
java.util.Set<TermLabel> labels)
|
Modifier and Type | Method and Description |
---|---|
MatchConditions |
LegacyTacletMatcher.checkConditions(MatchConditions cond,
Services services)
checks the provided matches against the variable conditions of this taclet
It returns the resulting match conditions or
null if the found matches
do not satisfy the variable conditions. |
MatchConditions |
LegacyTacletMatcher.checkVariableConditions(SchemaVariable var,
SVSubstitute instantiationCandidate,
MatchConditions matchCond,
Services services)
checks if the conditions for a correct instantiation are satisfied
|
abstract MatchConditions |
ElementMatcher.match(T op,
SVSubstitute subst,
MatchConditions mc,
Services services) |
MatchConditions |
LegacyTacletMatcher.matchFind(Term term,
MatchConditions matchCond,
Services services)
matches the given term against the taclet's find term
if the taclet has no find term or the match is unsuccessful
null
is returned |
IfMatchResult |
LegacyTacletMatcher.matchIf(ImmutableList<IfFormulaInstantiation> p_toMatch,
Term p_template,
MatchConditions p_matchCond,
Services p_services)
(non-Javadoc)
|
MatchConditions |
LegacyTacletMatcher.matchIf(java.lang.Iterable<IfFormulaInstantiation> p_toMatch,
MatchConditions p_matchCond,
Services p_services) |
protected MatchConditions |
LegacyTacletMatcher.matchJavaBlock(Term term,
Term template,
MatchConditions matchCond,
Services services)
returns the matchconditions that are required if the java block of the
given term matches the schema given by the template term or null if no
match is possible
(marked as final to help the compiler inlining methods)
|
MatchConditions |
LegacyTacletMatcher.matchSV(SchemaVariable sv,
ProgramElement pe,
MatchConditions matchCond,
Services services)
|
MatchConditions |
LegacyTacletMatcher.matchSV(SchemaVariable sv,
Term term,
MatchConditions matchCond,
Services services)
|
Modifier and Type | Method and Description |
---|---|
MatchConditions |
VMTacletMatcher.checkConditions(MatchConditions cond,
Services services)
checks the provided matches against the variable conditions of this taclet
It returns the resulting match conditions or
null if the found matches
do not satisfy the variable conditions. |
MatchConditions |
VMTacletMatcher.checkVariableConditions(SchemaVariable var,
SVSubstitute instantiationCandidate,
MatchConditions matchCond,
Services services)
checks if the conditions for a correct instantiation are satisfied
|
MatchConditions |
TacletMatchProgram.match(Term p_toMatch,
MatchConditions p_matchCond,
Services services)
executes the program and tries to match the provided term; additional restrictions are provided via match conditions.
|
MatchConditions |
VMTacletMatcher.matchFind(Term term,
MatchConditions matchCond,
Services services)
matches the given term against the taclet's find term
if the taclet has no find term or the match is unsuccessful
null
is returned |
IfMatchResult |
VMTacletMatcher.matchIf(ImmutableList<IfFormulaInstantiation> p_toMatch,
Term p_template,
MatchConditions p_matchCond,
Services p_services)
(non-Javadoc)
|
MatchConditions |
VMTacletMatcher.matchIf(java.lang.Iterable<IfFormulaInstantiation> p_toMatch,
MatchConditions p_matchCond,
Services p_services) |
MatchConditions |
VMTacletMatcher.matchSV(SchemaVariable sv,
ProgramElement pe,
MatchConditions matchCond,
Services services)
|
MatchConditions |
VMTacletMatcher.matchSV(SchemaVariable sv,
Term term,
MatchConditions matchCond,
Services services)
|
Modifier and Type | Method and Description |
---|---|
protected MatchConditions |
MatchProgramSVInstruction.addInstantiation(ProgramElement pe,
MatchConditions matchCond,
Services services)
tries to add the pair (this,pe) to the match conditions.
|
protected MatchConditions |
MatchSchemaVariableInstruction.addInstantiation(Term term,
MatchConditions matchCond,
Services services)
Tries to add the pair (this,term) to the match conditions.
|
MatchConditions |
MatchProgramSVInstruction.match(Operator instantiationCandidate,
MatchConditions matchConditions,
Services services) |
MatchConditions |
MatchOperatorInstruction.match(Operator instantiationCandidate,
MatchConditions matchConditions,
Services services) |
MatchConditions |
MatchOpIdentityInstruction.match(Operator instantiationCandidate,
MatchConditions matchConditions,
Services services) |
MatchConditions |
MatchProgramSVInstruction.match(ProgramElement instantiationCandidate,
MatchConditions matchCond,
Services services)
tries to match the schema variable of this instruction with the specified
ProgramElement instantiationCandidate
w.r.t. |
MatchConditions |
MatchSchemaVariableInstruction.match(ProgramElement instantiationCandidate,
MatchConditions mc,
Services services)
tries to match the schema variable of this instruction with the specified
ProgramElement instantiationCandidate
w.r.t. |
MatchConditions |
MatchUpdateSVInstruction.match(Term subst,
MatchConditions mc,
Services services)
tries to match the schema variable of this instruction with the specified
Term instantiationCandidate
w.r.t. |
MatchConditions |
MatchProgramSVInstruction.match(Term instantiationCandidate,
MatchConditions matchCond,
Services services)
tries to match the schema variable of this instruction with the specified
Term instantiationCandidate
w.r.t. |
MatchConditions |
MatchFormulaSVInstruction.match(Term subst,
MatchConditions mc,
Services services)
tries to match the schema variable of this instruction with the specified
Term instantiationCandidate
w.r.t. |
MatchConditions |
MatchElementaryUpdateInstruction.match(Term instantiationCandidate,
MatchConditions matchCond,
Services services) |
MatchConditions |
MatchModalOperatorSVInstruction.match(Term subst,
MatchConditions mc,
Services services) |
abstract MatchConditions |
Instruction.match(Term instantiationCandidate,
MatchConditions matchCond,
Services services)
tries to match the schema variable of this instruction with the specified
Term instantiationCandidate
w.r.t. |
MatchConditions |
MatchOpIdentityInstruction.match(Term instantiationCandidate,
MatchConditions matchConditions,
Services services)
tries to match the schema variable of this instruction with the specified
Term instantiationCandidate
w.r.t. |
MatchConditions |
MatchTermSVInstruction.match(Term subst,
MatchConditions mc,
Services services)
tries to match the schema variable of this instruction with the specified
Term instantiationCandidate
w.r.t. |
MatchConditions |
MatchVariableSVInstruction.match(Term subst,
MatchConditions mc,
Services services)
tries to match the schema variable of this instruction with the specified
Term instantiationCandidate
w.r.t. |
MatchConditions |
MatchSortDependingFunctionInstruction.match(Term instantiationCandidate,
MatchConditions matchConditions,
Services services)
Tries to match the top level operator of the given term with this instruction's sort depending function symbol.
|
MatchConditions |
MatchUpdateSVInstruction.match(TermNavigator termPosition,
MatchConditions mc,
Services services) |
MatchConditions |
MatchProgramSVInstruction.match(TermNavigator termPosition,
MatchConditions mc,
Services services) |
MatchConditions |
MatchFormulaSVInstruction.match(TermNavigator termPosition,
MatchConditions mc,
Services services) |
MatchConditions |
MatchElementaryUpdateInstruction.match(TermNavigator termPosition,
MatchConditions matchConditions,
Services services) |
MatchConditions |
MatchModalOperatorSVInstruction.match(TermNavigator termPosition,
MatchConditions mc,
Services services) |
MatchConditions |
MatchProgramInstruction.match(TermNavigator termPosition,
MatchConditions matchConditions,
Services services) |
MatchConditions |
MatchTermLabelInstruction.match(TermNavigator termPosition,
MatchConditions matchConditions,
Services services) |
MatchConditions |
MatchOpIdentityInstruction.match(TermNavigator termPosition,
MatchConditions matchConditions,
Services services) |
MatchConditions |
MatchTermSVInstruction.match(TermNavigator termPosition,
MatchConditions mc,
Services services) |
MatchConditions |
MatchVariableSVInstruction.match(TermNavigator termPosition,
MatchConditions mc,
Services services) |
MatchConditions |
UnbindVariablesInstruction.match(TermNavigator termPosition,
MatchConditions matchConditions,
Services services) |
MatchConditions |
MatchSortDependingFunctionInstruction.match(TermNavigator termPosition,
MatchConditions mc,
Services services) |
MatchConditions |
MatchInstruction.match(TermNavigator termPosition,
MatchConditions matchConditions,
Services services) |
MatchConditions |
BindVariablesInstruction.match(TermNavigator termPosition,
MatchConditions matchConditions,
Services services) |
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) |
protected MergeProcedure.ValuesMergeResult |
MergeRule.mergeHeaps(MergeProcedure mergeRule,
LocationVariable heapVar,
Term heap1,
Term heap2,
SymbolicExecutionState state1,
SymbolicExecutionState state2,
Term distinguishingFormula,
Services services)
Merges two heaps in a zip-like procedure.
|
protected Triple<SymbolicExecutionState,java.util.LinkedHashSet<Name>,java.util.LinkedHashSet<Term>> |
MergeRule.mergeStates(MergeProcedure mergeRule,
SymbolicExecutionState state1,
SymbolicExecutionState state2,
Term programCounter,
Term distinguishingFormula,
Services services)
Merges two SE states (U1,C1,p) and (U2,C2,p) according to the method
MergeRule#mergeValuesInStates(LocationVariable, SymbolicExecutionState, Term, SymbolicExecutionState, Term, Services)
. |
abstract MergeProcedure.ValuesMergeResult |
MergeProcedure.mergeValuesInStates(Term v,
SymbolicExecutionState state1,
Term valueInState1,
SymbolicExecutionState state2,
Term valueInState2,
Term distinguishingFormula,
Services services)
Merges two values valueInState1 and valueInState2 of corresponding SE
states state1 and state2 to a new value of a merge state.
|
Modifier and Type | Method and Description |
---|---|
static Term |
MergeByIfThenElse.createIfThenElseTerm(SymbolicExecutionState state1,
SymbolicExecutionState state2,
Term ifTerm,
Term elseTerm,
Term distinguishingFormula,
Services services)
Creates an if-then-else term for the variable v.
|
protected abstract AbstractDomainLattice |
MergeWithLatticeAbstraction.getAbstractDomainForSort(Sort s,
Services services)
Returns the abstract domain lattice for the given sort or null if there
has no lattice been specified for that sort.
|
AbstractDomainLattice |
MergeWithPredicateAbstraction.getAbstractDomainForSort(Sort s,
Services services) |
static AbstractDomainLattice |
MergeWithPredicateAbstraction.instantiateAbstractDomain(Sort s,
java.util.List<AbstractionPredicate> applicablePredicates,
java.lang.Class<? extends AbstractPredicateAbstractionLattice> latticeType,
Services services)
Instantiates the abstract domain lattice for the given sort or null if
there has no lattice been specified for that sort.
|
MergeProcedure.ValuesMergeResult |
MergeWithLatticeAbstraction.mergeValuesInStates(Term v,
SymbolicExecutionState state1,
Term valueInState1,
SymbolicExecutionState state2,
Term valueInState2,
Term distinguishingFormula,
Services services) |
MergeProcedure.ValuesMergeResult |
MergeWithPredicateAbstractionFactory.mergeValuesInStates(Term v,
SymbolicExecutionState state1,
Term valueInState1,
SymbolicExecutionState state2,
Term valueInState2,
Term distinguishingFormula,
Services services) |
MergeProcedure.ValuesMergeResult |
MergeIfThenElseAntecedent.mergeValuesInStates(Term v,
SymbolicExecutionState state1,
Term valueInState1,
SymbolicExecutionState state2,
Term valueInState2,
Term distinguishingFormula,
Services services) |
MergeProcedure.ValuesMergeResult |
MergeTotalWeakening.mergeValuesInStates(Term v,
SymbolicExecutionState state1,
Term valueInState1,
SymbolicExecutionState state2,
Term valueInState2,
Term distinguishingFormula,
Services services) |
MergeProcedure.ValuesMergeResult |
MergeByIfThenElse.mergeValuesInStates(Term v,
SymbolicExecutionState state1,
Term valueInState1,
SymbolicExecutionState state2,
Term valueInState2,
Term distinguishingFormula,
Services services) |
Modifier and Type | Method and Description |
---|---|
protected java.util.List<Statement> |
ConstructorCall.constructorCallSequence(New constructorReference,
KeYJavaType classType,
SVInstantiations svInst,
Services services)
returns a sequence of statements modelling the Java constructor call
semantics explicitly
|
static ProgramVariable |
EvaluateArgs.evaluate(Expression e,
java.util.List<? super LocalVariableDeclaration> l,
Services services,
ExecutionContext ec)
TODO Comment.
|
protected ProgramVariable[] |
InitArray.evaluateInitializers(Statement[] p_stmnts,
NewArray p_creationExpression,
Services services)
The variable initializers have to be evaluated and assigned to
temporary variables (the initializers may itself be array
initializers, in which case valid creation expressions are
created by inserting the new-operator)
|
KeYJavaType |
ProgramTransformer.getKeYJavaType(Services javaServ,
ExecutionContext ec) |
protected IProgramMethod |
MethodCall.getMethod(KeYJavaType prefixType,
MethodReference mr,
Services services)
Returns the method.
|
protected Statement |
MethodCall.makeIfCascade(ImmutableList<KeYJavaType> imps,
Services services)
TODO
|
ProgramElement[] |
ReattachLoopInvariant.transform(ProgramElement pe,
Services services,
SVInstantiations svInst) |
ProgramElement[] |
SpecialConstructorCall.transform(ProgramElement pe,
Services services,
SVInstantiations svInst) |
ProgramElement[] |
UnwindLoop.transform(ProgramElement pe,
Services services,
SVInstantiations svInst) |
ProgramElement[] |
ForToWhile.transform(ProgramElement pe,
Services services,
SVInstantiations svInst) |
ProgramElement[] |
StaticInitialisation.transform(ProgramElement pe,
Services services,
SVInstantiations insts) |
ProgramElement[] |
InitArrayCreation.transform(ProgramElement pe,
Services services,
SVInstantiations svInst) |
ProgramElement[] |
ArrayLength.transform(ProgramElement pe,
Services services,
SVInstantiations insts) |
ProgramElement[] |
IsStatic.transform(ProgramElement pe,
Services services,
SVInstantiations svInst) |
ProgramElement[] |
MultipleVarDecl.transform(ProgramElement pe,
Services services,
SVInstantiations svInst) |
ProgramElement[] |
EvaluateArgs.transform(ProgramElement pe,
Services services,
SVInstantiations svInst) |
ProgramElement[] |
TypeOf.transform(ProgramElement pe,
Services services,
SVInstantiations insts) |
ProgramElement[] |
ArrayPostDecl.transform(ProgramElement pe,
Services services,
SVInstantiations svInst) |
ProgramElement[] |
DoBreak.transform(ProgramElement pe,
Services services,
SVInstantiations insts)
performs the program transformation needed for symbolic program
transformation
|
ProgramElement[] |
ConstructorCall.transform(ProgramElement pe,
Services services,
SVInstantiations svInst) |
ProgramElement[] |
MethodCall.transform(ProgramElement pe,
Services services,
SVInstantiations svInst)
performs the program transformation needed for symbolic program execution
|
ProgramElement[] |
ForInitUnfoldTransformer.transform(ProgramElement pe,
Services services,
SVInstantiations svInst) |
ProgramElement[] |
EnhancedForElimination.transform(ProgramElement pe,
Services services,
SVInstantiations svInst)
An enhanced for loop is executed by transforming it into a "normal" for loop.
|
ProgramElement[] |
Unpack.transform(ProgramElement pe,
Services services,
SVInstantiations svInst) |
ProgramElement[] |
PostWork.transform(ProgramElement pe,
Services services,
SVInstantiations svInst)
performs the program transformation needed for symbolic program
transformation
|
abstract ProgramElement[] |
ProgramTransformer.transform(ProgramElement pe,
Services services,
SVInstantiations svInst)
performs the program transformation needed for symbolic
program transformation
|
ProgramElement[] |
SwitchToIf.transform(ProgramElement pe,
Services services,
SVInstantiations insts) |
ProgramElement[] |
CreateObject.transform(ProgramElement pe,
Services services,
SVInstantiations svInst) |
ProgramElement[] |
ExpandMethodBody.transform(ProgramElement pe,
Services services,
SVInstantiations svInst) |
Term |
WhileInvariantTransformer.transform(TermLabelState termLabelState,
Rule rule,
RuleApp ruleApp,
Goal goal,
Sequent applicationSequent,
PosInOccurrence applicationPos,
Term initialPost,
Term invariantFramingTermination,
SVInstantiations svInst,
Services services)
calculates the resulting term.
|
Term |
AddCast.transform(Term term,
SVInstantiations svInst,
Services services) |
Term |
CreateBeforeLoopUpdate.transform(Term term,
SVInstantiations svInst,
Services services) |
Term |
CreateLocalAnonUpdate.transform(Term term,
SVInstantiations svInst,
Services services) |
Term |
ConstantValue.transform(Term term,
SVInstantiations svInst,
Services services) |
Term |
CreateFrameCond.transform(Term term,
SVInstantiations svInst,
Services services) |
Term |
ExpandQueriesMetaConstruct.transform(Term term,
SVInstantiations svInst,
Services services)
term.sub(0) is the term that possibly contains queries.
|
Term |
MemberPVToField.transform(Term term,
SVInstantiations svInst,
Services services) |
Term |
CreateWellformedCond.transform(Term term,
SVInstantiations svInst,
Services services) |
Term |
EnumConstantValue.transform(Term term,
SVInstantiations svInst,
Services services)
calculates the resulting term.
|
Term |
ArrayBaseInstanceOf.transform(Term term,
SVInstantiations svInst,
Services services)
returns an G::instance(term.sub(1)) term for the element sort of
the given array .
|
Term |
CreateHeapAnonUpdate.transform(Term term,
SVInstantiations svInst,
Services services) |
Term |
IntroAtPreDefsOp.transform(Term term,
SVInstantiations svInst,
Services services) |
Term |
ObserverEqualityMetaConstruct.transform(Term term,
SVInstantiations svInst,
Services services)
Given two terms termExt and termBase, produce a formula which implies
equality of the two terms.
|
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 |
Constructor and Description |
---|
ForToWhileTransformation(ProgramElement root,
ProgramElementName outerLabel,
ProgramElementName innerLabel,
Services services) |
ReplaceWhileLoop(ProgramElement root,
StatementBlock toInsert,
Services services)
creates the WhileLoopTransformation for the transformation mode
|
ReplaceWhileLoop(ProgramElement root,
SVInstantiations inst,
StatementBlock toInsert,
Services services)
creates the WhileLoopTransformation for the check mode
|
WhileInvariantTransformation(ProgramElement root,
ProgramElementName outerLabel,
ProgramElementName innerLabel,
ProgramVariable cont,
ProgramVariable exc,
ProgramVariable excParam,
ProgramVariable thrownException,
ProgramVariable brk,
ProgramVariable rtrn,
ProgramVariable returnExpr,
java.util.LinkedList<de.uka.ilkd.key.rule.metaconstruct.BreakToBeReplaced> breakList,
Services services)
creates the WhileLoopTransformation for the transformation mode
|
WhileInvariantTransformation(ProgramElement root,
SVInstantiations inst,
Services services)
creates the WhileLoopTransformation for the check mode
|
WhileLoopTransformation(ProgramElement root,
ProgramElementName outerLabel,
ProgramElementName innerLabel,
Services services)
creates the WhileLoopTransformation for the transformation mode
|
WhileLoopTransformation(ProgramElement root,
SVInstantiations inst,
Services services)
creates the WhileLoopTransformation for the check mode
|
Modifier and Type | Method and Description |
---|---|
static Polynomial |
Polynomial.create(Term polyTerm,
Services services) |
static Monomial |
Monomial.create(Term monoTerm,
Services services) |
Term |
Polynomial.toTerm(Services services)
Creates a term from this polynomial expression.
|
Term |
Monomial.toTerm(Services services) |
Term |
MetaGreater.transform(Term term,
SVInstantiations svInst,
Services services) |
Term |
MetaEqual.transform(Term term,
SVInstantiations svInst,
Services services) |
Term |
MetaArithBitMaskOp.transform(Term term,
SVInstantiations svInst,
Services services) |
Term |
DivideMonomials.transform(Term term,
SVInstantiations svInst,
Services services)
calculates the resulting term.
|
Term |
MetaLeq.transform(Term term,
SVInstantiations svInst,
Services services) |
Term |
MetaSub.transform(Term term,
SVInstantiations svInst,
Services services) |
Term |
DivideLCRMonomials.transform(Term term,
SVInstantiations svInst,
Services services)
calculates the resulting term.
|
Term |
MetaShift.transform(Term term,
SVInstantiations svInst,
Services services) |
Term |
MetaPow.transform(Term term,
SVInstantiations svInst,
Services services)
calculates the resulting term.
|
Term |
MetaDiv.transform(Term term,
SVInstantiations svInst,
Services services)
calculates the resulting term.
|
Term |
MetaLess.transform(Term term,
SVInstantiations svInst,
Services services) |
Term |
MetaGeq.transform(Term term,
SVInstantiations svInst,
Services services) |
Term |
MetaAdd.transform(Term term,
SVInstantiations svInst,
Services services) |
Term |
MetaMul.transform(Term term,
SVInstantiations svInst,
Services services) |
Modifier and Type | Method and Description |
---|---|
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) |
Modifier and Type | Method and Description |
---|---|
ImmutableList<Goal> |
RuleAppSMT.SMTRule.apply(Goal goal,
Services services,
RuleApp ruleApp) |
SMTSolver |
SolverType.createSolver(SMTProblem problem,
de.uka.ilkd.key.smt.SolverListener listener,
Services services)
Creates an instance of SMTSolver representing a concrete instance of that solver.
|
SMTTranslator |
SolverType.createTranslator(Services services)
The translator to be used.
|
void |
SolverLauncher.launch(java.util.Collection<SolverType> solverTypes,
java.util.Collection<SMTProblem> problems,
Services services)
Launches several solvers for the problems that are handed over.
|
void |
SolverLauncher.launch(SMTProblem problem,
Services services,
SolverType... solverTypes)
Launches several solvers for the problem that is handed over.
Note: Calling this methods does not create an extra thread, i.e. |
static Term |
SMTProblem.sequentToTerm(Sequent s,
Services services) |
void |
ProblemTypeInformation.setServices(Services services) |
java.lang.StringBuffer |
SMTObjTranslator.translateProblem(Sequent sequent,
Services services,
SMTSettings settings) |
java.lang.StringBuffer |
AbstractSMTTranslator.translateProblem(Sequent sequent,
Services services,
SMTSettings settings) |
java.lang.CharSequence |
SMTTranslator.translateProblem(Sequent sequent,
Services services,
SMTSettings settings)
Translates a problem into the given syntax.
|
java.util.ArrayList<java.lang.StringBuffer> |
AbstractSMTTranslator.translateTaclets(Services services,
SMTSettings settings)
Translates the list
tacletFormulae to the given syntax. |
protected java.lang.StringBuffer |
AbstractSMTTranslator.translateTerm(Term term,
java.util.Vector<QuantifiableVariable> quantifiedVars,
Services services)
Translates the given term into input syntax and adds the resulting
string to the StringBuffer sb.
|
protected java.lang.StringBuffer |
AbstractSMTTranslator.translateUnknown(Term term,
java.util.Vector<QuantifiableVariable> quantifiedVars,
Services services)
Takes care of sequent tree parts that were not matched in
translate(term, skolemization).
|
Constructor and Description |
---|
AbstractSMTTranslator(Sequent sequent,
Services services,
AbstractSMTTranslator.Configuration config)
Just a constructor which starts the conversion to Simplify syntax.
|
AbstractSMTTranslator(Services s,
AbstractSMTTranslator.Configuration config)
For translating only terms and not complete sequents.
|
SimplifyTranslator(Sequent sequent,
Services services,
AbstractSMTTranslator.Configuration config)
Just a constructor which starts the conversion to Simplify syntax.
|
SimplifyTranslator(Services services,
AbstractSMTTranslator.Configuration config) |
SmtLib2Translator(Sequent sequent,
Services services,
AbstractSMTTranslator.Configuration config)
Just a constructor which starts the conversion to Simplify syntax.
|
SmtLib2Translator(Services s,
AbstractSMTTranslator.Configuration config)
For translating only terms and not complete sequents.
|
SmtLibTranslator(Sequent sequent,
Services services,
AbstractSMTTranslator.Configuration config)
Just a constructor which starts the conversion to Simplify syntax.
|
SmtLibTranslator(Services s,
AbstractSMTTranslator.Configuration config)
For translating only terms and not complete sequents.
|
SMTObjTranslator(SMTSettings settings,
Services services,
KeYJavaType typeOfClassUnderTest) |
SMTProblem(Sequent s,
Services services) |
SortHierarchy(java.util.HashMap<Sort,java.lang.StringBuffer> sortnames,
java.util.HashMap<Sort,java.lang.StringBuffer> prednames,
boolean explicitNullHierarchy,
boolean explicitHierarchy,
Services services)
Create a Sort Hierarchy.
|
Constructor and Description |
---|
TypeHierarchy(Services services) |
Modifier and Type | Method and Description |
---|---|
T |
SMTHandlerProperty.get(Services services)
Extract a value of this property from a Services object.
|
java.util.List<SMTHandler> |
SMTHandlerServices.getFreshHandlers(Services services,
MasterHandler mh)
Get a copy of freshly created
SMTHandler s by cloning the reference
handlers. |
void |
DefinedSymbolsHandler.init(MasterHandler masterHandler,
Services services,
java.util.Properties handlerSnippets) |
void |
SeqDefHandler.init(MasterHandler masterHandler,
Services services,
java.util.Properties handlerSnippets) |
void |
CastingFunctionsHandler.init(MasterHandler masterHandler,
Services services,
java.util.Properties handlerSnippets) |
void |
QuantifierHandler.init(MasterHandler masterHandler,
Services services,
java.util.Properties handlerSnippets) |
void |
LogicalVariableHandler.init(MasterHandler masterHandler,
Services services,
java.util.Properties handlerSnippets) |
void |
SMTHandler.init(MasterHandler masterHandler,
Services services,
java.util.Properties handlerSnippets)
Initialise this handler.
|
void |
BooleanConnectiveHandler.init(MasterHandler masterHandler,
Services services,
java.util.Properties handlerSnippets) |
void |
UninterpretedSymbolsHandler.init(MasterHandler masterHandler,
Services services,
java.util.Properties handlerSnippets) |
void |
PolymorphicHandler.init(MasterHandler masterHandler,
Services services,
java.util.Properties handlerSnippets) |
void |
InstanceOfHandler.init(MasterHandler masterHandler,
Services services,
java.util.Properties handlerSnippets) |
void |
IntegerOpHandler.init(MasterHandler masterHandler,
Services services,
java.util.Properties handlerSnippets) |
void |
FieldConstantHandler.init(MasterHandler masterHandler,
Services services,
java.util.Properties handlerSnippets) |
void |
UpdateHandler.init(MasterHandler masterHandler,
Services services,
java.util.Properties handlerSnippets) |
void |
SumProdHandler.init(MasterHandler masterHandler,
Services services,
java.util.Properties handlerSnippets) |
void |
NumberConstantsHandler.init(MasterHandler masterHandler,
Services services,
java.util.Properties handlerSnippets) |
void |
CastHandler.init(MasterHandler masterHandler,
Services services,
java.util.Properties handlerSnippets) |
java.lang.CharSequence |
ModularSMTLib2Translator.translateProblem(Sequent sequent,
Services services,
SMTSettings settings) |
Constructor and Description |
---|
MasterHandler(Services services,
SMTSettings settings)
Create a new handler.
|
SMTTacletTranslator(Services services) |
Modifier and Type | Method and Description |
---|---|
static BlockContract |
BlockContractImpl.combine(ImmutableSet<BlockContract> contracts,
Services services) |
static LoopContract |
LoopContractImpl.combine(ImmutableSet<LoopContract> contracts,
Services services) |
static AuxiliaryContract.Variables |
AuxiliaryContract.Variables.create(LoopStatement loop,
java.util.List<Label> labels,
IProgramMethod method,
Services services)
Creates a new instance.
|
static AuxiliaryContract.Variables |
AuxiliaryContract.Variables.create(StatementBlock block,
java.util.List<Label> labels,
IProgramMethod method,
Services services)
Creates a new instance.
|
static ImmutableSet<RewriteTaclet> |
ClassWellDefinedness.createInvTaclet(Services services)
Creates a well-definedness taclet for an invariant reference.
|
RewriteTaclet |
MethodWellDefinedness.createOperationTaclet(Services services)
Creates a well-definedness for a (pure) method invocation of this method.
|
protected java.util.Map<ProgramVariable,ProgramVariable> |
AbstractAuxiliaryContractImpl.createReplacementMap(AuxiliaryContract.Variables newVariables,
Services services) |
protected java.util.Map<Term,Term> |
AbstractAuxiliaryContractImpl.createReplacementMap(Term newHeap,
AuxiliaryContract.Terms newTerms,
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.
|
java.util.ArrayList<AbstractionPredicate> |
PredicateAbstractionMergeContract.getAbstractionPredicates(java.util.Map<LocationVariable,Term> atPres,
Services services)
TODO
|
Term |
FunctionalOperationContractImpl.getAnyMod(Term mod,
ProgramVariable selfVar,
ImmutableList<ProgramVariable> paramVars,
Services services) |
static java.util.Map<LocationVariable,Term> |
HeapContext.getAtPres(java.util.Map<LocationVariable,LocationVariable> atPreVars,
Services services) |
Term |
RepresentsAxiom.getAxiom(ParsableVariable heapVar,
ParsableVariable selfVar,
Services services) |
Term |
LoopContract.getDecreases(AuxiliaryContract.Variables variables,
Services services) |
Term |
LoopContractImpl.getDecreases(AuxiliaryContract.Variables variables,
Services services) |
Term |
LoopContract.getDecreases(Term heap,
Term self,
Services services) |
Term |
LoopContractImpl.getDecreases(Term heap,
Term self,
Services services) |
Term |
FunctionalAuxiliaryContract.getDep(LocationVariable heap,
boolean atPre,
ProgramVariable selfVar,
ImmutableList<ProgramVariable> paramVars,
java.util.Map<LocationVariable,? extends ProgramVariable> atPreVars,
Services services) |
Term |
FunctionalOperationContractImpl.getDep(LocationVariable heap,
boolean atPre,
ProgramVariable selfVar,
ImmutableList<ProgramVariable> paramVars,
java.util.Map<LocationVariable,? extends ProgramVariable> atPreVars,
Services services) |
Term |
InformationFlowContractImpl.getDep(LocationVariable heap,
boolean atPre,
ProgramVariable selfVar,
ImmutableList<ProgramVariable> paramVars,
java.util.Map<LocationVariable,? extends ProgramVariable> atPreVars,
Services services) |
Term |
DependencyContractImpl.getDep(LocationVariable heap,
boolean atPre,
ProgramVariable selfVar,
ImmutableList<ProgramVariable> paramVars,
java.util.Map<LocationVariable,? extends ProgramVariable> atPreVars,
Services services) |
Term |
WellDefinednessCheck.getDep(LocationVariable heap,
boolean atPre,
ProgramVariable selfVar,
ImmutableList<ProgramVariable> paramVars,
java.util.Map<LocationVariable,? extends ProgramVariable> atPreVars,
Services services)
Deprecated.
|
Term |
Contract.getDep(LocationVariable heap,
boolean atPre,
ProgramVariable selfVar,
ImmutableList<ProgramVariable> paramVars,
java.util.Map<LocationVariable,? extends ProgramVariable> atPreVars,
Services services)
Returns the dependency set of the contract.
|
Term |
FunctionalAuxiliaryContract.getDep(LocationVariable heap,
boolean atPre,
Term heapTerm,
Term selfTerm,
ImmutableList<Term> paramTerms,
java.util.Map<LocationVariable,Term> atPres,
Services services) |
Term |
FunctionalOperationContractImpl.getDep(LocationVariable heap,
boolean atPre,
Term heapTerm,
Term selfTerm,
ImmutableList<Term> paramTerms,
java.util.Map<LocationVariable,Term> atPres,
Services services) |
Term |
InformationFlowContractImpl.getDep(LocationVariable heap,
boolean atPre,
Term heapTerm,
Term selfTerm,
ImmutableList<Term> paramTerms,
java.util.Map<LocationVariable,Term> atPres,
Services services) |
Term |
DependencyContractImpl.getDep(LocationVariable heap,
boolean atPre,
Term heapTerm,
Term selfTerm,
ImmutableList<Term> paramTerms,
java.util.Map<LocationVariable,Term> atPres,
Services services) |
Term |
WellDefinednessCheck.getDep(LocationVariable heap,
boolean atPre,
Term heapTerm,
Term selfTerm,
ImmutableList<Term> paramTerms,
java.util.Map<LocationVariable,Term> atPres,
Services services)
Deprecated.
|
Term |
Contract.getDep(LocationVariable heap,
boolean atPre,
Term heapTerm,
Term selfTerm,
ImmutableList<Term> paramTerms,
java.util.Map<LocationVariable,Term> atPres,
Services services)
Returns the dependency set of the contract.
|
Term |
LoopSpecification.getFreeInvariant(LocationVariable heap,
Term selfTerm,
java.util.Map<LocationVariable,Term> atPres,
Services services)
Returns the free invariant formula.
|
Term |
LoopSpecImpl.getFreeInvariant(LocationVariable heap,
Term selfTerm,
java.util.Map<LocationVariable,Term> atPres,
Services services) |
Term |
LoopSpecification.getFreeInvariant(Services services) |
Term |
LoopSpecImpl.getFreeInvariant(Services services) |
Term |
FunctionalOperationContractImpl.getFreePost(java.util.List<LocationVariable> heapContext,
java.util.Map<LocationVariable,Term> heapTerms,
Term selfTerm,
ImmutableList<Term> paramTerms,
Term resultTerm,
Term excTerm,
java.util.Map<LocationVariable,Term> atPres,
Services services) |
Term |
FunctionalOperationContract.getFreePost(java.util.List<LocationVariable> heapContext,
java.util.Map<LocationVariable,Term> heapTerms,
Term selfTerm,
ImmutableList<Term> paramTerms,
Term resultTerm,
Term excTerm,
java.util.Map<LocationVariable,Term> atPres,
Services services) |
Term |
FunctionalOperationContractImpl.getFreePost(LocationVariable heap,
ProgramVariable selfVar,
ImmutableList<ProgramVariable> paramVars,
ProgramVariable resultVar,
ProgramVariable excVar,
java.util.Map<LocationVariable,? extends ProgramVariable> atPreVars,
Services services) |
Term |
FunctionalOperationContract.getFreePost(LocationVariable heap,
ProgramVariable selfVar,
ImmutableList<ProgramVariable> paramVars,
ProgramVariable resultVar,
ProgramVariable excVar,
java.util.Map<LocationVariable,? extends ProgramVariable> atPreVars,
Services services) |
Term |
FunctionalOperationContractImpl.getFreePost(LocationVariable heap,
Term heapTerm,
Term selfTerm,
ImmutableList<Term> paramTerms,
Term resultTerm,
Term excTerm,
java.util.Map<LocationVariable,Term> atPres,
Services services) |
Term |
FunctionalOperationContract.getFreePost(LocationVariable heap,
Term heapTerm,
Term selfTerm,
ImmutableList<Term> paramTerms,
Term resultTerm,
Term excTerm,
java.util.Map<LocationVariable,Term> atPres,
Services services) |
Term |
AbstractAuxiliaryContractImpl.getFreePost(Services services) |
Term |
AuxiliaryContract.getFreePost(Services services) |
Term |
AbstractAuxiliaryContractImpl.getFreePostcondition(LocationVariable heap,
AuxiliaryContract.Variables variables,
Services services) |
Term |
AuxiliaryContract.getFreePostcondition(LocationVariable heap,
AuxiliaryContract.Variables variables,
Services services) |
Term |
AbstractAuxiliaryContractImpl.getFreePostcondition(LocationVariable heap,
Services services) |
Term |
AuxiliaryContract.getFreePostcondition(LocationVariable heap,
Services services) |
Term |
AbstractAuxiliaryContractImpl.getFreePostcondition(LocationVariable heapVariable,
Term heap,
AuxiliaryContract.Terms terms,
Services services) |
Term |
AuxiliaryContract.getFreePostcondition(LocationVariable heapVariable,
Term heap,
AuxiliaryContract.Terms terms,
Services services) |
Term |
FunctionalOperationContractImpl.getFreePre(java.util.List<LocationVariable> heapContext,
ProgramVariable selfVar,
ImmutableList<ProgramVariable> paramVars,
java.util.Map<LocationVariable,? extends ProgramVariable> atPreVars,
Services services) |
Term |
OperationContract.getFreePre(java.util.List<LocationVariable> heapContext,
ProgramVariable selfVar,
ImmutableList<ProgramVariable> paramVars,
java.util.Map<LocationVariable,? extends ProgramVariable> atPreVars,
Services services) |
Term |
FunctionalOperationContractImpl.getFreePre(LocationVariable heap,
ProgramVariable selfVar,
ImmutableList<ProgramVariable> paramVars,
java.util.Map<LocationVariable,? extends ProgramVariable> atPreVars,
Services services) |
Term |
OperationContract.getFreePre(LocationVariable heap,
ProgramVariable selfVar,
ImmutableList<ProgramVariable> paramVars,
java.util.Map<LocationVariable,? extends ProgramVariable> atPreVars,
Services services) |
Term |
FunctionalOperationContractImpl.getFreePre(LocationVariable heap,
Term heapTerm,
Term selfTerm,
ImmutableList<Term> paramTerms,
java.util.Map<LocationVariable,Term> atPres,
Services services) |
Term |
OperationContract.getFreePre(LocationVariable heap,
Term heapTerm,
Term selfTerm,
ImmutableList<Term> paramTerms,
java.util.Map<LocationVariable,Term> atPres,
Services services) |
Term |
AbstractAuxiliaryContractImpl.getFreePre(Services services) |
Term |
AuxiliaryContract.getFreePre(Services services) |
Term |
AbstractAuxiliaryContractImpl.getFreePrecondition(LocationVariable heap,
AuxiliaryContract.Variables variables,
Services services) |
Term |
AuxiliaryContract.getFreePrecondition(LocationVariable heap,
AuxiliaryContract.Variables variables,
Services services) |
Term |
AbstractAuxiliaryContractImpl.getFreePrecondition(LocationVariable heap,
ProgramVariable self,
java.util.Map<LocationVariable,LocationVariable> atPres,
Services services) |
Term |
AuxiliaryContract.getFreePrecondition(LocationVariable heap,
ProgramVariable self,
java.util.Map<LocationVariable,LocationVariable> atPres,
Services services) |
Term |
AbstractAuxiliaryContractImpl.getFreePrecondition(LocationVariable heap,
Services services) |
Term |
AuxiliaryContract.getFreePrecondition(LocationVariable heap,
Services services) |
Term |
AbstractAuxiliaryContractImpl.getFreePrecondition(LocationVariable heapVariable,
Term heap,
AuxiliaryContract.Terms terms,
Services services) |
Term |
AuxiliaryContract.getFreePrecondition(LocationVariable heapVariable,
Term heap,
AuxiliaryContract.Terms terms,
Services services) |
Term |
AbstractAuxiliaryContractImpl.getFreePrecondition(LocationVariable heapVariable,
Term heap,
Term self,
java.util.Map<LocationVariable,Term> atPres,
Services services) |
Term |
AuxiliaryContract.getFreePrecondition(LocationVariable heapVariable,
Term heap,
Term self,
java.util.Map<LocationVariable,Term> atPres,
Services services) |
Term |
FunctionalAuxiliaryContract.getGlobalDefs(LocationVariable heap,
Term heapTerm,
Term selfTerm,
ImmutableList<Term> paramTerms,
Services services) |
Term |
FunctionalOperationContractImpl.getGlobalDefs(LocationVariable heap,
Term heapTerm,
Term selfTerm,
ImmutableList<Term> paramTerms,
Services services) |
Term |
InformationFlowContractImpl.getGlobalDefs(LocationVariable heap,
Term heapTerm,
Term selfTerm,
ImmutableList<Term> paramTerms,
Services services) |
Term |
DependencyContractImpl.getGlobalDefs(LocationVariable heap,
Term heapTerm,
Term selfTerm,
ImmutableList<Term> paramTerms,
Services services) |
Term |
WellDefinednessCheck.getGlobalDefs(LocationVariable heap,
Term heapTerm,
Term selfTerm,
ImmutableList<Term> paramTerms,
Services services)
Deprecated.
|
Term |
Contract.getGlobalDefs(LocationVariable heap,
Term heapTerm,
Term selfTerm,
ImmutableList<Term> paramTerms,
Services services) |
java.lang.String |
InformationFlowContractImpl.getHTMLBody(Services services) |
protected java.lang.String |
InformationFlowContractImpl.getHTMLFor(Term originalTerm,
java.lang.String htmlName,
Services services) |
java.lang.String |
AbstractAuxiliaryContractImpl.getHtmlText(Services services) |
java.lang.String |
AuxiliaryContract.getHtmlText(Services services) |
java.lang.String |
FunctionalAuxiliaryContract.getHTMLText(Services services) |
java.lang.String |
FunctionalOperationContractImpl.getHTMLText(Services services) |
java.lang.String |
InformationFlowContractImpl.getHTMLText(Services services) |
java.lang.String |
DependencyContractImpl.getHTMLText(Services services) |
java.lang.String |
WellDefinednessCheck.getHTMLText(Services services) |
java.lang.String |
Contract.getHTMLText(Services services)
Returns the contract in pretty HTML format.
|
ImmutableList<InfFlowSpec> |
LoopSpecification.getInfFlowSpecs(LocationVariable heap,
Term selfTerm,
java.util.Map<LocationVariable,Term> atPres,
Services services) |
ImmutableList<InfFlowSpec> |
LoopSpecImpl.getInfFlowSpecs(LocationVariable heap,
Term selfTerm,
java.util.Map<LocationVariable,Term> atPres,
Services services) |
ImmutableList<InfFlowSpec> |
LoopSpecification.getInfFlowSpecs(Services services) |
ImmutableList<InfFlowSpec> |
LoopSpecImpl.getInfFlowSpecs(Services services) |
MergeProcedure |
PredicateAbstractionMergeContract.getInstantiatedMergeProcedure(Services services) |
MergeProcedure |
UnparameterizedMergeContract.getInstantiatedMergeProcedure(Services services) |
MergeProcedure |
MergeContract.getInstantiatedMergeProcedure(Services services) |
Term |
LoopSpecification.getInvariant(LocationVariable heap,
Term selfTerm,
java.util.Map<LocationVariable,Term> atPres,
Services services)
Returns the invariant formula.
|
Term |
LoopSpecImpl.getInvariant(LocationVariable heap,
Term selfTerm,
java.util.Map<LocationVariable,Term> atPres,
Services services) |
Term |
LoopSpecification.getInvariant(Services services) |
Term |
LoopSpecImpl.getInvariant(Services services) |
Term |
AbstractAuxiliaryContractImpl.getMby(AuxiliaryContract.Variables variables,
Services services) |
Term |
AuxiliaryContract.getMby(AuxiliaryContract.Variables variables,
Services services) |
Term |
FunctionalAuxiliaryContract.getMby(java.util.Map<LocationVariable,Term> heapTerms,
Term selfTerm,
ImmutableList<Term> paramTerms,
java.util.Map<LocationVariable,Term> atPres,
Services services) |
Term |
FunctionalOperationContractImpl.getMby(java.util.Map<LocationVariable,Term> heapTerms,
Term selfTerm,
ImmutableList<Term> paramTerms,
java.util.Map<LocationVariable,Term> atPres,
Services services) |
Term |
InformationFlowContractImpl.getMby(java.util.Map<LocationVariable,Term> heapTerms,
Term selfTerm,
ImmutableList<Term> paramTerms,
java.util.Map<LocationVariable,Term> atPres,
Services services)
Deprecated.
|
Term |
DependencyContractImpl.getMby(java.util.Map<LocationVariable,Term> heapTerms,
Term selfTerm,
ImmutableList<Term> paramTerms,
java.util.Map<LocationVariable,Term> atPres,
Services services) |
Term |
WellDefinednessCheck.getMby(java.util.Map<LocationVariable,Term> heapTerms,
Term selfTerm,
ImmutableList<Term> paramTerms,
java.util.Map<LocationVariable,Term> atPres,
Services services)
Deprecated.
|
Term |
Contract.getMby(java.util.Map<LocationVariable,Term> heapTerms,
Term selfTerm,
ImmutableList<Term> paramTerms,
java.util.Map<LocationVariable,Term> atPres,
Services services)
Returns the measured_by clause of the contract.
|
Term |
AbstractAuxiliaryContractImpl.getMby(java.util.Map<LocationVariable,Term> heapTerms,
Term selfTerm,
java.util.Map<LocationVariable,Term> atPres,
Services services) |
Term |
AuxiliaryContract.getMby(java.util.Map<LocationVariable,Term> heapTerms,
Term selfTerm,
java.util.Map<LocationVariable,Term> atPres,
Services services) |
Term |
FunctionalAuxiliaryContract.getMby(ProgramVariable selfVar,
ImmutableList<ProgramVariable> paramVars,
Services services) |
Term |
FunctionalOperationContractImpl.getMby(ProgramVariable selfVar,
ImmutableList<ProgramVariable> paramVars,
Services services) |
Term |
InformationFlowContractImpl.getMby(ProgramVariable selfVar,
ImmutableList<ProgramVariable> paramVars,
Services services)
Deprecated.
|
Term |
DependencyContractImpl.getMby(ProgramVariable selfVar,
ImmutableList<ProgramVariable> paramVars,
Services services) |
Term |
WellDefinednessCheck.getMby(ProgramVariable selfVar,
ImmutableList<ProgramVariable> paramVars,
Services services)
Deprecated.
|
Term |
Contract.getMby(ProgramVariable selfVar,
ImmutableList<ProgramVariable> paramVars,
Services services)
Returns the measured_by clause of the contract.
|
Term |
AbstractAuxiliaryContractImpl.getMby(ProgramVariable selfVar,
Services services) |
Term |
AuxiliaryContract.getMby(ProgramVariable selfVar,
Services services) |
Term |
FunctionalOperationContractImpl.getMod(LocationVariable heap,
ProgramVariable selfVar,
ImmutableList<ProgramVariable> paramVars,
Services services) |
Term |
OperationContract.getMod(LocationVariable heapVar,
ProgramVariable selfVar,
ImmutableList<ProgramVariable> paramVars,
Services services)
Returns the modifies clause of the contract.
|
Term |
FunctionalOperationContractImpl.getMod(LocationVariable heap,
Term heapTerm,
Term selfTerm,
ImmutableList<Term> paramTerms,
Services services) |
Term |
OperationContract.getMod(LocationVariable heapVar,
Term heapTerm,
Term selfTerm,
ImmutableList<Term> paramTerms,
Services services)
Returns the modifies clause of the contract.
|
Term |
AbstractAuxiliaryContractImpl.getMod(Services services) |
Term |
AuxiliaryContract.getMod(Services services) |
static java.util.List<LocationVariable> |
HeapContext.getModHeaps(Services services,
boolean transaction) |
Term |
LoopSpecification.getModifies(LocationVariable heap,
Term selfTerm,
java.util.Map<LocationVariable,Term> atPres,
Services services)
Returns the modifies clause.
|
Term |
LoopSpecImpl.getModifies(LocationVariable heap,
Term selfTerm,
java.util.Map<LocationVariable,Term> atPres,
Services services) |
Term |
LoopSpecification.getModifies(Term selfTerm,
java.util.Map<LocationVariable,Term> atPres,
Services services)
Returns the modifies clause.
|
Term |
LoopSpecImpl.getModifies(Term selfTerm,
java.util.Map<LocationVariable,Term> atPres,
Services services) |
Term |
AbstractAuxiliaryContractImpl.getModifiesClause(LocationVariable heap,
AuxiliaryContract.Variables variables,
Services services) |
Term |
AuxiliaryContract.getModifiesClause(LocationVariable heap,
AuxiliaryContract.Variables variables,
Services services) |
Term |
AbstractAuxiliaryContractImpl.getModifiesClause(LocationVariable heap,
ProgramVariable self,
Services services) |
Term |
AuxiliaryContract.getModifiesClause(LocationVariable heap,
ProgramVariable self,
Services services) |
Term |
AbstractAuxiliaryContractImpl.getModifiesClause(LocationVariable heap,
Services services) |
Term |
AuxiliaryContract.getModifiesClause(LocationVariable heap,
Services services) |
Term |
AbstractAuxiliaryContractImpl.getModifiesClause(LocationVariable heapVariable,
Term heap,
Term self,
Services services) |
Term |
AuxiliaryContract.getModifiesClause(LocationVariable heapVariable,
Term heap,
Term self,
Services services) |
java.lang.String |
AbstractAuxiliaryContractImpl.getPlainText(Services services) |
java.lang.String |
FunctionalAuxiliaryContract.getPlainText(Services services) |
java.lang.String |
FunctionalOperationContractImpl.getPlainText(Services services) |
java.lang.String |
InformationFlowContractImpl.getPlainText(Services services) |
java.lang.String |
DependencyContractImpl.getPlainText(Services services) |
java.lang.String |
WellDefinednessCheck.getPlainText(Services services) |
java.lang.String |
Contract.getPlainText(Services services)
Returns the contract in pretty plain text format.
|
java.lang.String |
AuxiliaryContract.getPlainText(Services services) |
java.lang.String |
AbstractAuxiliaryContractImpl.getPlainText(Services services,
AuxiliaryContract.Terms terms) |
java.lang.String |
AuxiliaryContract.getPlainText(Services services,
AuxiliaryContract.Terms terms) |
java.lang.String |
LoopSpecImpl.getPlainText(Services services,
boolean usePrettyPrinting,
boolean useUnicodeSymbols)
Return a plain text representation of this loop specification.
|
java.lang.String |
LoopSpecification.getPlainText(Services services,
java.lang.Iterable<LocationVariable> heapContext,
boolean usePrettyPrinting,
boolean useUnicodeSymbols)
Returns the invariant in pretty plain text format.
|
java.lang.String |
LoopSpecImpl.getPlainText(Services services,
java.lang.Iterable<LocationVariable> heapContext,
boolean usePrettyPrinting,
boolean useUnicodeSymbols) |
Term |
FunctionalOperationContractImpl.getPost(java.util.List<LocationVariable> heapContext,
java.util.Map<LocationVariable,Term> heapTerms,
Term selfTerm,
ImmutableList<Term> paramTerms,
Term resultTerm,
Term excTerm,
java.util.Map<LocationVariable,Term> atPres,
Services services) |
Term |
FunctionalOperationContract.getPost(java.util.List<LocationVariable> heapContext,
java.util.Map<LocationVariable,Term> heapTerms,
Term selfTerm,
ImmutableList<Term> paramTerms,
Term resultTerm,
Term excTerm,
java.util.Map<LocationVariable,Term> atPres,
Services services) |
Term |
FunctionalOperationContractImpl.getPost(java.util.List<LocationVariable> heapContext,
ProgramVariable selfVar,
ImmutableList<ProgramVariable> paramVars,
ProgramVariable resultVar,
ProgramVariable excVar,
java.util.Map<LocationVariable,? extends ProgramVariable> atPreVars,
Services services) |
Term |
FunctionalOperationContract.getPost(java.util.List<LocationVariable> heapContext,
ProgramVariable selfVar,
ImmutableList<ProgramVariable> paramVars,
ProgramVariable resultVar,
ProgramVariable excVar,
java.util.Map<LocationVariable,? extends ProgramVariable> atPreVars,
Services services) |
Term |
FunctionalOperationContractImpl.getPost(LocationVariable heap,
ProgramVariable selfVar,
ImmutableList<ProgramVariable> paramVars,
ProgramVariable resultVar,
ProgramVariable excVar,
java.util.Map<LocationVariable,? extends ProgramVariable> atPreVars,
Services services) |
Term |
FunctionalOperationContract.getPost(LocationVariable heap,
ProgramVariable selfVar,
ImmutableList<ProgramVariable> paramVars,
ProgramVariable resultVar,
ProgramVariable excVar,
java.util.Map<LocationVariable,? extends ProgramVariable> atPreVars,
Services services)
Returns the postcondition of the contract.
|
Term |
FunctionalOperationContractImpl.getPost(LocationVariable heap,
Term heapTerm,
Term selfTerm,
ImmutableList<Term> paramTerms,
Term resultTerm,
Term excTerm,
java.util.Map<LocationVariable,Term> atPres,
Services services) |
Term |
FunctionalOperationContract.getPost(LocationVariable heap,
Term heapTerm,
Term selfTerm,
ImmutableList<Term> paramTerms,
Term resultTerm,
Term excTerm,
java.util.Map<LocationVariable,Term> atPres,
Services services)
Returns the postcondition of the contract.
|
Term |
AbstractAuxiliaryContractImpl.getPost(Services services) |
Term |
AuxiliaryContract.getPost(Services services) |
Term |
AbstractAuxiliaryContractImpl.getPostcondition(LocationVariable heap,
AuxiliaryContract.Variables variables,
Services services) |
Term |
AuxiliaryContract.getPostcondition(LocationVariable heap,
AuxiliaryContract.Variables variables,
Services services) |
Term |
AbstractAuxiliaryContractImpl.getPostcondition(LocationVariable heap,
Services services) |
Term |
AuxiliaryContract.getPostcondition(LocationVariable heap,
Services services) |
Term |
AbstractAuxiliaryContractImpl.getPostcondition(LocationVariable heapVariable,
Term heap,
AuxiliaryContract.Terms terms,
Services services) |
Term |
AuxiliaryContract.getPostcondition(LocationVariable heapVariable,
Term heap,
AuxiliaryContract.Terms terms,
Services services) |
Term |
FunctionalAuxiliaryContract.getPre(java.util.List<LocationVariable> heapContext,
java.util.Map<LocationVariable,Term> heapTerms,
Term selfTerm,
ImmutableList<Term> paramTerms,
java.util.Map<LocationVariable,Term> atPres,
Services services) |
Term |
FunctionalOperationContractImpl.getPre(java.util.List<LocationVariable> heapContext,
java.util.Map<LocationVariable,Term> heapTerms,
Term selfTerm,
ImmutableList<Term> paramTerms,
java.util.Map<LocationVariable,Term> atPres,
Services services) |
Term |
InformationFlowContractImpl.getPre(java.util.List<LocationVariable> heapContext,
java.util.Map<LocationVariable,Term> heapTerms,
Term selfTerm,
ImmutableList<Term> paramTerms,
java.util.Map<LocationVariable,Term> atPres,
Services services)
Deprecated.
|
Term |
DependencyContractImpl.getPre(java.util.List<LocationVariable> heapContext,
java.util.Map<LocationVariable,Term> heapTerms,
Term selfTerm,
ImmutableList<Term> paramTerms,
java.util.Map<LocationVariable,Term> atPres,
Services services) |
Term |
WellDefinednessCheck.getPre(java.util.List<LocationVariable> heapContext,
java.util.Map<LocationVariable,Term> heapTerms,
Term selfTerm,
ImmutableList<Term> paramTerms,
java.util.Map<LocationVariable,Term> atPres,
Services services)
Deprecated.
|
Term |
Contract.getPre(java.util.List<LocationVariable> heapContext,
java.util.Map<LocationVariable,Term> heapTerms,
Term selfTerm,
ImmutableList<Term> paramTerms,
java.util.Map<LocationVariable,Term> atPres,
Services services)
Returns the precondition of the contract.
|
Term |
FunctionalAuxiliaryContract.getPre(java.util.List<LocationVariable> heapContext,
ProgramVariable selfVar,
ImmutableList<ProgramVariable> paramVars,
java.util.Map<LocationVariable,? extends ProgramVariable> atPreVars,
Services services) |
Term |
FunctionalOperationContractImpl.getPre(java.util.List<LocationVariable> heapContext,
ProgramVariable selfVar,
ImmutableList<ProgramVariable> paramVars,
java.util.Map<LocationVariable,? extends ProgramVariable> atPreVars,
Services services) |
Term |
InformationFlowContractImpl.getPre(java.util.List<LocationVariable> heapContext,
ProgramVariable selfVar,
ImmutableList<ProgramVariable> paramVars,
java.util.Map<LocationVariable,? extends ProgramVariable> atPreVars,
Services services)
Deprecated.
|
Term |
DependencyContractImpl.getPre(java.util.List<LocationVariable> heapContext,
ProgramVariable selfVar,
ImmutableList<ProgramVariable> paramVars,
java.util.Map<LocationVariable,? extends ProgramVariable> atPreVars,
Services services) |
Term |
WellDefinednessCheck.getPre(java.util.List<LocationVariable> heapContext,
ProgramVariable selfVar,
ImmutableList<ProgramVariable> paramVars,
java.util.Map<LocationVariable,? extends ProgramVariable> atPreVars,
Services services)
Deprecated.
|
Term |
Contract.getPre(java.util.List<LocationVariable> heapContext,
ProgramVariable selfVar,
ImmutableList<ProgramVariable> paramVars,
java.util.Map<LocationVariable,? extends ProgramVariable> atPreVars,
Services services)
Returns the precondition of the contract.
|
Term |
FunctionalAuxiliaryContract.getPre(LocationVariable heap,
ProgramVariable selfVar,
ImmutableList<ProgramVariable> paramVars,
java.util.Map<LocationVariable,? extends ProgramVariable> atPreVars,
Services services) |
Term |
FunctionalOperationContractImpl.getPre(LocationVariable heap,
ProgramVariable selfVar,
ImmutableList<ProgramVariable> paramVars,
java.util.Map<LocationVariable,? extends ProgramVariable> atPreVars,
Services services) |
Term |
InformationFlowContractImpl.getPre(LocationVariable heap,
ProgramVariable selfVar,
ImmutableList<ProgramVariable> paramVars,
java.util.Map<LocationVariable,? extends ProgramVariable> atPreVars,
Services services)
Deprecated.
|
Term |
DependencyContractImpl.getPre(LocationVariable heap,
ProgramVariable selfVar,
ImmutableList<ProgramVariable> paramVars,
java.util.Map<LocationVariable,? extends ProgramVariable> atPreVars,
Services services) |
Term |
WellDefinednessCheck.getPre(LocationVariable heap,
ProgramVariable selfVar,
ImmutableList<ProgramVariable> paramVars,
java.util.Map<LocationVariable,? extends ProgramVariable> atPreVars,
Services services)
Deprecated.
|
Term |
Contract.getPre(LocationVariable heap,
ProgramVariable selfVar,
ImmutableList<ProgramVariable> paramVars,
java.util.Map<LocationVariable,? extends ProgramVariable> atPreVars,
Services services)
Returns the precondition of the contract.
|
Term |
FunctionalAuxiliaryContract.getPre(LocationVariable heap,
Term heapTerm,
Term selfTerm,
ImmutableList<Term> paramTerms,
java.util.Map<LocationVariable,Term> atPres,
Services services) |
Term |
FunctionalOperationContractImpl.getPre(LocationVariable heap,
Term heapTerm,
Term selfTerm,
ImmutableList<Term> paramTerms,
java.util.Map<LocationVariable,Term> atPres,
Services services) |
Term |
InformationFlowContractImpl.getPre(LocationVariable heap,
Term heapTerm,
Term selfTerm,
ImmutableList<Term> paramTerms,
java.util.Map<LocationVariable,Term> atPres,
Services services)
Deprecated.
|
Term |
DependencyContractImpl.getPre(LocationVariable heap,
Term heapTerm,
Term selfTerm,
ImmutableList<Term> paramTerms,
java.util.Map<LocationVariable,Term> atPres,
Services services) |
Term |
WellDefinednessCheck.getPre(LocationVariable heap,
Term heapTerm,
Term selfTerm,
ImmutableList<Term> paramTerms,
java.util.Map<LocationVariable,Term> atPres,
Services services)
Deprecated.
|
Term |
Contract.getPre(LocationVariable heap,
Term heapTerm,
Term selfTerm,
ImmutableList<Term> paramTerms,
java.util.Map<LocationVariable,Term> atPres,
Services services)
Returns the precondition of the contract.
|
Term |
AbstractAuxiliaryContractImpl.getPre(Services services) |
Term |
AuxiliaryContract.getPre(Services services) |
WellDefinednessCheck.TermAndFunc |
WellDefinednessCheck.getPre(de.uka.ilkd.key.speclang.WellDefinednessCheck.Condition pre,
ParsableVariable self,
ParsableVariable heap,
ImmutableList<? extends ParsableVariable> parameters,
boolean taclet,
Services services)
Gets the full valid precondition, which holds in the element's pre-state.
|
Term |
AbstractAuxiliaryContractImpl.getPrecondition(LocationVariable heap,
AuxiliaryContract.Variables variables,
Services services) |
Term |
AuxiliaryContract.getPrecondition(LocationVariable heap,
AuxiliaryContract.Variables variables,
Services services) |
Term |
AbstractAuxiliaryContractImpl.getPrecondition(LocationVariable heap,
ProgramVariable self,
java.util.Map<LocationVariable,LocationVariable> atPres,
Services services) |
Term |
AuxiliaryContract.getPrecondition(LocationVariable heap,
ProgramVariable self,
java.util.Map<LocationVariable,LocationVariable> atPres,
Services services) |
Term |
AbstractAuxiliaryContractImpl.getPrecondition(LocationVariable heap,
Services services) |
Term |
AuxiliaryContract.getPrecondition(LocationVariable heap,
Services services) |
Term |
AbstractAuxiliaryContractImpl.getPrecondition(LocationVariable heapVariable,
Term heap,
AuxiliaryContract.Terms terms,
Services services) |
Term |
AuxiliaryContract.getPrecondition(LocationVariable heapVariable,
Term heap,
AuxiliaryContract.Terms terms,
Services services) |
Term |
AbstractAuxiliaryContractImpl.getPrecondition(LocationVariable heapVariable,
Term heap,
Term self,
java.util.Map<LocationVariable,Term> atPres,
Services services) |
Term |
AuxiliaryContract.getPrecondition(LocationVariable heapVariable,
Term heap,
Term self,
java.util.Map<LocationVariable,Term> atPres,
Services services) |
ProofOblInput |
FunctionalAuxiliaryContract.getProofObl(Services services) |
ProofOblInput |
FunctionalOperationContractImpl.getProofObl(Services services) |
ProofOblInput |
InformationFlowContractImpl.getProofObl(Services services) |
ProofOblInput |
DependencyContractImpl.getProofObl(Services services) |
ProofOblInput |
WellDefinednessCheck.getProofObl(Services services) |
ProofOblInput |
Contract.getProofObl(Services services)
Lookup the proof obligation belonging to the contract in the specification repository.
|
protected java.util.Map<Term,Term> |
FunctionalOperationContractImpl.getReplaceMap(LocationVariable heap,
Term heapTerm,
Term selfTerm,
ImmutableList<Term> paramTerms,
Services services)
Deprecated.
|
protected java.util.Map<Term,Term> |
FunctionalOperationContractImpl.getReplaceMap(LocationVariable heap,
Term heapTerm,
Term selfTerm,
ImmutableList<Term> paramTerms,
Term resultTerm,
Term excTerm,
Term atPre,
Services services)
Deprecated.
|
protected java.util.Map<Term,Term> |
FunctionalOperationContractImpl.getReplaceMap(java.util.Map<LocationVariable,Term> heapTerms,
Term selfTerm,
ImmutableList<Term> paramTerms,
Term resultTerm,
Term excTerm,
java.util.Map<LocationVariable,Term> atPres,
Services services)
Get the according replace map for the given variable terms.
|
protected java.util.Map<ProgramVariable,ProgramVariable> |
FunctionalOperationContractImpl.getReplaceMap(ProgramVariable selfVar,
ImmutableList<ProgramVariable> paramVars,
ProgramVariable resultVar,
ProgramVariable excVar,
java.util.Map<LocationVariable,? extends ProgramVariable> atPreVars,
Services services)
Get the according replace map for the given variables.
|
Term |
FunctionalOperationContractImpl.getRepresentsAxiom(LocationVariable heap,
ProgramVariable selfVar,
ImmutableList<ProgramVariable> paramVars,
ProgramVariable resultVar,
java.util.Map<LocationVariable,? extends ProgramVariable> atPreVars,
Services services) |
Term |
FunctionalOperationContract.getRepresentsAxiom(LocationVariable heap,
ProgramVariable selfVar,
ImmutableList<ProgramVariable> paramVars,
ProgramVariable resultVar,
java.util.Map<LocationVariable,? extends ProgramVariable> atPreVars,
Services services)
Returns the model method definition for model method contracts
|
Term |
FunctionalOperationContractImpl.getRepresentsAxiom(LocationVariable heap,
Term heapTerm,
Term selfTerm,
ImmutableList<Term> paramTerms,
Term resultTerm,
Term excTerm,
java.util.Map<LocationVariable,Term> atPres,
Services services) |
Term |
FunctionalOperationContract.getRepresentsAxiom(LocationVariable heap,
Term heapTerm,
Term selfTerm,
ImmutableList<Term> paramTerms,
Term resultTerm,
Term excTerm,
java.util.Map<LocationVariable,Term> atPres,
Services services) |
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) |
Term |
AbstractAuxiliaryContractImpl.getTerm(Term term,
AuxiliaryContract.Variables variables,
Services services)
Replaces variables in a map of terms
|
Term |
AbstractAuxiliaryContractImpl.getTerm(Term term,
Term heap,
AuxiliaryContract.Terms terms,
Services services)
Replaces variables in a map of terms
|
static java.lang.String |
FunctionalOperationContractImpl.getText(FunctionalOperationContract contract,
ImmutableList<Term> contractParams,
Term resultTerm,
Term contractSelf,
Term excTerm,
LocationVariable baseHeap,
Term baseHeapTerm,
java.util.List<LocationVariable> heapContext,
java.util.Map<LocationVariable,Term> atPres,
boolean includeHtmlMarkup,
Services services,
boolean usePrettyPrinting,
boolean useUnicodeSymbols) |
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) |
AuxiliaryContract.Terms |
AbstractAuxiliaryContractImpl.getVariablesAsTerms(Services services) |
AuxiliaryContract.Terms |
AuxiliaryContract.getVariablesAsTerms(Services services) |
Term |
LoopSpecification.getVariant(Term selfTerm,
java.util.Map<LocationVariable,Term> atPres,
Services services)
Returns the variant term.
|
Term |
LoopSpecImpl.getVariant(Term selfTerm,
java.util.Map<LocationVariable,Term> atPres,
Services services) |
boolean |
LoopSpecification.hasInfFlowSpec(Services services) |
boolean |
LoopSpecImpl.hasInfFlowSpec(Services services) |
boolean |
AbstractAuxiliaryContractImpl.isReadOnly(Services services) |
boolean |
AuxiliaryContract.isReadOnly(Services services) |
boolean |
FunctionalOperationContractImpl.isReadOnlyContract(Services services) |
boolean |
FunctionalOperationContract.isReadOnlyContract(Services services) |
PredicateAbstractionMergeContract |
PredicateAbstractionMergeContract.map(java.util.function.UnaryOperator<Term> op,
Services services) |
MethodWellDefinedness |
MethodWellDefinedness.map(java.util.function.UnaryOperator<Term> op,
Services services) |
ClassAxiomImpl |
ClassAxiomImpl.map(java.util.function.UnaryOperator<Term> op,
Services services) |
FunctionalOperationContract |
FunctionalOperationContractImpl.map(java.util.function.UnaryOperator<Term> op,
Services services) |
ClassWellDefinedness |
ClassWellDefinedness.map(java.util.function.UnaryOperator<Term> op,
Services services) |
ClassInvariant |
ClassInvariantImpl.map(java.util.function.UnaryOperator<Term> op,
Services services) |
LoopContract |
LoopContract.map(java.util.function.UnaryOperator<Term> op,
Services services) |
InformationFlowContract |
InformationFlowContractImpl.map(java.util.function.UnaryOperator<Term> op,
Services services) |
InitiallyClause |
InitiallyClauseImpl.map(java.util.function.UnaryOperator<Term> op,
Services services) |
FunctionalBlockContract |
FunctionalBlockContract.map(java.util.function.UnaryOperator<Term> op,
Services services) |
QueryAxiom |
QueryAxiom.map(java.util.function.UnaryOperator<Term> op,
Services services) |
InformationFlowContract |
InformationFlowContract.map(java.util.function.UnaryOperator<Term> op,
Services services) |
ClassInvariant |
ClassInvariant.map(java.util.function.UnaryOperator<Term> op,
Services services) |
UnparameterizedMergeContract |
UnparameterizedMergeContract.map(java.util.function.UnaryOperator<Term> op,
Services services) |
FunctionalOperationContract |
FunctionalOperationContract.map(java.util.function.UnaryOperator<Term> op,
Services services) |
SpecificationElement |
PartialInvAxiom.map(java.util.function.UnaryOperator<Term> op,
Services services) |
ContractAxiom |
ContractAxiom.map(java.util.function.UnaryOperator<Term> op,
Services services) |
LoopSpecification |
LoopSpecification.map(java.util.function.UnaryOperator<Term> op,
Services services) |
InitiallyClause |
InitiallyClause.map(java.util.function.UnaryOperator<Term> op,
Services services) |
DependencyContract |
DependencyContractImpl.map(java.util.function.UnaryOperator<Term> op,
Services services) |
OperationContract |
OperationContract.map(java.util.function.UnaryOperator<Term> op,
Services services) |
abstract WellDefinednessCheck |
WellDefinednessCheck.map(java.util.function.UnaryOperator<Term> op,
Services services) |
BlockContract |
BlockContractImpl.map(java.util.function.UnaryOperator<Term> op,
Services services) |
SpecificationElement |
RepresentsAxiom.map(java.util.function.UnaryOperator<Term> op,
Services services) |
Contract |
Contract.map(java.util.function.UnaryOperator<Term> op,
Services services) |
MergeContract |
MergeContract.map(java.util.function.UnaryOperator<Term> op,
Services services) |
LoopWellDefinedness |
LoopWellDefinedness.map(java.util.function.UnaryOperator<Term> op,
Services services) |
BlockContract |
BlockContract.map(java.util.function.UnaryOperator<Term> op,
Services services) |
DependencyContract |
DependencyContract.map(java.util.function.UnaryOperator<Term> op,
Services services) |
LoopContract |
LoopContractImpl.map(java.util.function.UnaryOperator<Term> op,
Services services) |
BlockWellDefinedness |
BlockWellDefinedness.map(java.util.function.UnaryOperator<Term> op,
Services services) |
SpecificationElement |
SpecificationElement.map(java.util.function.UnaryOperator<Term> op,
Services services)
Applies a unary operator to every term in this specification element.
|
FunctionalLoopContract |
FunctionalLoopContract.map(java.util.function.UnaryOperator<Term> op,
Services services) |
ModelMethodExecution |
ModelMethodExecution.map(java.util.function.UnaryOperator<Term> op,
Services services) |
AuxiliaryContract |
AuxiliaryContract.map(java.util.function.UnaryOperator<Term> op,
Services services) |
abstract StatementWellDefinedness |
StatementWellDefinedness.map(java.util.function.UnaryOperator<Term> op,
Services services) |
LoopSpecification |
LoopSpecImpl.map(java.util.function.UnaryOperator<Term> op,
Services services) |
java.lang.String |
FunctionalAuxiliaryContract.proofToString(Services services) |
java.lang.String |
FunctionalOperationContractImpl.proofToString(Services services) |
java.lang.String |
InformationFlowContractImpl.proofToString(Services services) |
java.lang.String |
DependencyContractImpl.proofToString(Services services) |
java.lang.String |
WellDefinednessCheck.proofToString(Services services) |
java.lang.String |
Contract.proofToString(Services services)
Returns a parseable String representation of the contract.
|
void |
FunctionalLoopContract.replaceEnhancedForVariables(Services services)
Replaces
\index and \values with the proper variables in all terms of this
contract. |
LoopContract |
LoopContract.replaceEnhancedForVariables(StatementBlock newBlock,
Services services)
Replaces
\index and \values with the proper variables in all terms of this
contract. |
LoopContract |
LoopContractImpl.replaceEnhancedForVariables(StatementBlock newBlock,
Services services) |
LoopSpecification |
LoopSpecification.setInvariant(java.util.Map<LocationVariable,Term> invariants,
java.util.Map<LocationVariable,Term> freeInvariants,
Term selfTerm,
java.util.Map<LocationVariable,Term> atPres,
Services services)
Returns a new loop invariant where the invariant formula has been
replaced with the passed one.
|
LoopSpecification |
LoopSpecImpl.setInvariant(java.util.Map<LocationVariable,Term> invariants,
java.util.Map<LocationVariable,Term> freeInvariants,
Term selfTerm,
java.util.Map<LocationVariable,Term> atPres,
Services services) |
Constructor and Description |
---|
BlockWellDefinedness(BlockContract block,
AuxiliaryContract.Variables variables,
ImmutableSet<ProgramVariable> params,
Services services)
Creates a contract to check well-definedness of a block contract
|
ClassWellDefinedness(ClassInvariant inv,
IObserverFunction target,
Term accessible,
Term mby,
Services services) |
Combinator(BlockContract[] contracts,
Services services) |
Combinator(LoopContract[] contracts,
Services services) |
Combinator(T[] contracts,
Services services) |
ContractFactory(Services services)
Creates a new contract factory.
|
Creator(java.lang.String baseName,
LoopStatement loop,
java.util.List<Label> labels,
IProgramMethod method,
Behavior behavior,
AuxiliaryContract.Variables variables,
java.util.Map<LocationVariable,Term> requires,
java.util.Map<LocationVariable,Term> requiresFree,
Term measuredBy,
java.util.Map<LocationVariable,Term> ensures,
java.util.Map<LocationVariable,Term> ensuresFree,
ImmutableList<InfFlowSpec> infFlowSpecs,
java.util.Map<Label,Term> breaks,
java.util.Map<Label,Term> continues,
Term returns,
Term signals,
Term signalsOnly,
Term diverges,
java.util.Map<LocationVariable,Term> assignables,
java.util.Map<LocationVariable,java.lang.Boolean> hasMod,
Term decreases,
Services services)
Creates loop contract for a loop.
|
Creator(java.lang.String baseName,
StatementBlock block,
java.util.List<Label> labels,
IProgramMethod method,
Behavior behavior,
AuxiliaryContract.Variables variables,
java.util.Map<LocationVariable,Term> requires,
java.util.Map<LocationVariable,Term> requiresFree,
Term measuredBy,
java.util.Map<LocationVariable,Term> ensures,
java.util.Map<LocationVariable,Term> ensuresFree,
ImmutableList<InfFlowSpec> infFlowSpecs,
java.util.Map<Label,Term> breaks,
java.util.Map<Label,Term> continues,
Term returns,
Term signals,
Term signalsOnly,
Term diverges,
java.util.Map<LocationVariable,Term> assignables,
java.util.Map<LocationVariable,java.lang.Boolean> hasMod,
Services services) |
Creator(java.lang.String baseName,
StatementBlock block,
java.util.List<Label> labels,
IProgramMethod method,
Behavior behavior,
AuxiliaryContract.Variables variables,
java.util.Map<LocationVariable,Term> requires,
java.util.Map<LocationVariable,Term> requiresFree,
Term measuredBy,
java.util.Map<LocationVariable,Term> ensures,
java.util.Map<LocationVariable,Term> ensuresFree,
ImmutableList<InfFlowSpec> infFlowSpecs,
java.util.Map<Label,Term> breaks,
java.util.Map<Label,Term> continues,
Term returns,
Term signals,
Term signalsOnly,
Term diverges,
java.util.Map<LocationVariable,Term> assignables,
java.util.Map<LocationVariable,java.lang.Boolean> hasMod,
Services services) |
Creator(java.lang.String baseName,
StatementBlock block,
java.util.List<Label> labels,
IProgramMethod method,
Behavior behavior,
AuxiliaryContract.Variables variables,
java.util.Map<LocationVariable,Term> requires,
java.util.Map<LocationVariable,Term> requiresFree,
Term measuredBy,
java.util.Map<LocationVariable,Term> ensures,
java.util.Map<LocationVariable,Term> ensuresFree,
ImmutableList<InfFlowSpec> infFlowSpecs,
java.util.Map<Label,Term> breaks,
java.util.Map<Label,Term> continues,
Term returns,
Term signals,
Term signalsOnly,
Term diverges,
java.util.Map<LocationVariable,Term> assignables,
java.util.Map<LocationVariable,java.lang.Boolean> hasMod,
Term decreases,
Services services)
Creates loop contract for a block that starts with a loop.
|
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) |
MethodWellDefinedness(DependencyContract contract,
Services services) |
MethodWellDefinedness(FunctionalOperationContract contract,
Services services) |
MethodWellDefinedness(RepresentsAxiom rep,
Services services) |
PartialInvAxiom(ClassInvariant inv,
boolean isStatic,
Services services)
Creates a new class axiom.
|
PartialInvAxiom(ClassInvariant inv,
java.lang.String displayName,
Services services) |
VariablesCreator(JavaStatement statement,
java.util.List<Label> labels,
IProgramMethod method,
Services services)
Constructor.
|
Constructor and Description |
---|
DLSpecFactory(Services services) |
Modifier and Type | Method and Description |
---|---|
static int |
JMLSpecExtractor.arrayDepth(Type type,
Services services)
Get the depth for the nonNull predicate.
|
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
|
Constructor and Description |
---|
JMLSpecExtractor(Services services) |
Modifier and Type | Field and Description |
---|---|
protected Services |
JMLSpecFactory.services |
Constructor and Description |
---|
JMLSpecFactory(Services services) |
Modifier and Type | Field and Description |
---|---|
Services |
JmlTermFactory.services |
Modifier and Type | Method and Description |
---|---|
JmlIO |
JmlIO.services(Services services)
Sets the current services
|
SLExpression |
JmlTermFactory.translateMapExpressionToJDL(java.lang.String text,
ImmutableList<SLExpression> list,
Services services) |
SLExpression |
JmlTermFactory.translateMapExpressionToJDL(org.antlr.runtime.Token t,
ImmutableList<SLExpression> list,
Services services) |
SLExpression |
JmlTermFactory.translateToJDLTerm(org.antlr.runtime.Token escape,
java.lang.String functName,
Services services,
TermBuilder tb,
ImmutableList<SLExpression> list) |
Constructor and Description |
---|
JmlIO(Services services,
KeYJavaType specInClass,
ProgramVariable selfVar,
ImmutableList<ProgramVariable> paramVars,
ProgramVariable resultVar,
ProgramVariable excVar,
java.util.Map<LocationVariable,Term> atPres,
java.util.Map<LocationVariable,Term> atBefores)
Full constructor of this class.
|
JmlTermFactory(SLExceptionFactory exc,
Services services,
JavaIntegerSemanticsHelper intHelper) |
Modifier and Type | Field and Description |
---|---|
protected Services |
SLExpressionResolver.services |
Modifier and Type | Method and Description |
---|---|
ImmutableList<KeYJavaType> |
SLParameters.getSignature(Services services)
returns the type signature of the parameter list
|
Constructor and Description |
---|
JavaIntegerSemanticsHelper(Services services,
SLExceptionFactory excManager) |
Modifier and Type | Method and Description |
---|---|
protected Services |
JavaCardDLStrategy.getServices() |
Modifier and Type | Method and Description |
---|---|
protected Term |
IsInRangeProvable.createConsequence(PosInOccurrence pos,
Services services)
creates the term to be proven to follow from a (possibly empty) set of axioms
|
protected boolean |
IsInRangeProvable.isProvable(Sequent seq,
Services services)
checks if the sequent is provable
|
Modifier and Type | Method and Description |
---|---|
static Feature |
ThrownExceptionFeature.create(java.lang.String[] blockedExceptions,
Services services) |
protected boolean |
ThrownExceptionFeature.filter(Term term,
Services services,
ExecutionContext ec) |
Modifier and Type | Method and Description |
---|---|
static long |
PredictCostProver.computerInstanceCost(Substitution sub,
Term matrix,
ImmutableSet<Term> assertList,
Services services) |
protected boolean |
RecAndExistentiallyConnectedClausesFeature.filter(Term term,
Services services) |
protected boolean |
EliminableQuantifierTF.filter(Term term,
Services services) |
Term |
Constraint.getInstantiation(Metavariable p_mv,
Services services)
Deprecated.
Find a term the given metavariable can be instantiated with which
is consistent with every instantiation that satisfies this
constraint (that means, the term such an instantiation
substitutes the metavariable with can always be unified with the
returned term).
|
Term |
Constraint.Top.getInstantiation(Metavariable p_mv,
Services services)
Deprecated.
as this constraint is unsatisfiable it just returns the metavariable given as argument
|
Term |
EqualityConstraint.getInstantiation(Metavariable p_mv,
Services services)
Deprecated.
Find a term the given metavariable can be instantiated with which
is consistent with every instantiation that satisfies this
constraint (that means, the term such an instantiation
substitutes the metavariable with can always be unified with the
returned term).
|
ImmutableSet<Substitution> |
Trigger.getSubstitutionsFromTerms(ImmutableSet<Term> targetTerm,
Services services) |
static Term |
HandleArith.provedByArith(Term problem,
Services services)
try to prove atom by using polynomial
|
static Term |
HandleArith.provedByArith(Term problem,
Term axiom,
Services services)
Try to prove problem by know that axiom is true.
|
Constructor and Description |
---|
ConstraintAwareSyntacticalReplaceVisitor(TermLabelState termLabelState,
Services services,
Constraint metavariableInst,
PosInOccurrence applicationPosInOccurrence,
Rule rule,
RuleApp ruleApp,
Taclet.TacletLabelHint labelHint,
Goal goal) |
Modifier and Type | Method and Description |
---|---|
RuleAppCost |
SubTermFeature.compute(Term term,
Services services) |
RuleAppCost |
BinarySumTermFeature.compute(Term term,
Services services) |
RuleAppCost |
RecSubTermFeature.compute(Term term,
Services services) |
RuleAppCost |
ConstTermFeature.compute(Term term,
Services services) |
RuleAppCost |
ShannonTermFeature.compute(Term term,
Services services) |
RuleAppCost |
BinaryTermFeature.compute(Term term,
Services services) |
RuleAppCost |
PrintTermFeature.compute(Term term,
Services services) |
RuleAppCost |
TermFeature.compute(Term term,
Services services) |
protected boolean |
OperatorTF.filter(Term term,
Services services) |
protected boolean |
AtomTermFeature.filter(Term term,
Services services) |
protected boolean |
IsPostConditionTermFeature.filter(Term t,
Services services) |
protected boolean |
TermLabelTermFeature.filter(Term term,
Services services) |
protected boolean |
EqTermFeature.filter(Term term,
Services services) |
protected boolean |
AnonHeapTermFeature.filter(Term t,
Services services) |
protected boolean |
IsInductionVariable.filter(Term term,
Services services) |
protected boolean |
PrimitiveHeapTermFeature.filter(Term t,
Services services) |
protected boolean |
IsNonRigidTermFeature.filter(Term term,
Services services) |
protected boolean |
SimplifiedSelectTermFeature.filter(Term t,
Services services) |
protected boolean |
SortExtendsTransTermFeature.filter(Term term,
Services services) |
protected boolean |
OperatorClassTF.filter(Term term,
Services services) |
protected boolean |
ClosedExpressionTermFeature.filter(Term term,
Services services) |
protected boolean |
IsSelectSkolemConstantTermFeature.filter(Term t,
Services services) |
protected abstract boolean |
BinaryTermFeature.filter(Term term,
Services services) |
protected boolean |
IsHeapFunctionTermFeature.filter(Term t,
Services services) |
protected boolean |
ContainsExecutableCodeTermFeature.filter(Term t,
Services services) |
protected boolean |
ConstantTermFeature.filter(Term term,
Services services) |
Modifier and Type | Method and Description |
---|---|
static TermGenerator |
SuperTermGenerator.upwards(TermFeature cond,
Services services) |
static TermGenerator |
SuperTermGenerator.upwardsWithIndex(TermFeature cond,
Services services) |
Modifier and Type | Method and Description |
---|---|
protected Term |
MonomialColumnOp.divide(Monomial numerator,
java.math.BigInteger denominator,
Services services) |
protected abstract Term |
AbstractDividePolynomialsProjection.divide(Monomial numerator,
java.math.BigInteger denominator,
Services services) |
Modifier and Type | Method and Description |
---|---|
Services |
ExecutionNodeReader.AbstractKeYlessExecutionElement.getServices()
Returns the
Services used by IExecutionElement.getProof() . |
protected Services |
AbstractUpdateExtractor.getServices()
|
Modifier and Type | Method and Description |
---|---|
protected static void |
TruthValueTracingUtil.analyzeTacletGoal(Node parent,
TacletApp tacletApp,
TacletGoalTemplate tacletGoal,
java.util.List<de.uka.ilkd.key.symbolic_execution.TruthValueTracingUtil.LabelOccurrence> labels,
Services services,
java.util.Map<java.lang.String,TruthValueTracingUtil.MultiEvaluationResult> results)
Analyzes the given
TacletGoalTemplate . |
protected static void |
TruthValueTracingUtil.evaluateNode(Node evaluationNode,
boolean useUnicode,
boolean usePrettyPrinting,
Node child,
int childIndexOnParent,
Name termLabelName,
java.util.Map<java.lang.String,TruthValueTracingUtil.MultiEvaluationResult> nodeResult,
TruthValueTracingUtil.TruthValueTracingResult result,
Services services)
|
protected void |
SymbolicExecutionTreeBuilder.initMethodCallStack(Node root,
Services services)
This method initializes
#methodCallStack in case that the
initial Sequent contains MethodFrame s in its modality. |
java.lang.String |
TruthValueTracingUtil.MultiEvaluationResult.toPrettyString(Services services)
Creates a pretty printed
String . |
Modifier and Type | Method and Description |
---|---|
Services |
IExecutionElement.getServices()
Returns the
Services used by IExecutionElement.getProof() . |
Modifier and Type | Method and Description |
---|---|
Services |
AbstractExecutionElement.getServices()
Returns the
Services used by IExecutionElement.getProof() . |
Modifier and Type | Method and Description |
---|---|
protected java.util.Set<Term> |
AbstractExecutionValue.collectRelevantTerms(Services services,
Term term)
Collects all
Term s contained in relevant constraints. |
protected static LocationVariable |
ExecutionOperationContract.extractResultVariableFromPostBranch(Node node,
Services services)
Extracts the result variable from the given post branch.
|
protected void |
AbstractExecutionValue.fillRelevantTerms(Services services,
Term term,
java.util.Set<Term> toFill)
Utility method used by
AbstractExecutionValue.collectRelevantTerms(Services, Term) . |
protected java.lang.String |
AbstractExecutionElement.formatTerm(Term term,
Services services)
|
protected void |
ExecutionVariable.groupGoalsByValue(ImmutableList<Goal> goals,
Operator operator,
Term siteProofSelectTerm,
Term siteProofCondition,
java.util.Map<Term,java.util.List<Goal>> valueMap,
java.util.List<Goal> unknownValues,
Services services)
Groups all
Goal s which provides the same value. |
protected ExecutionValue[] |
ExecutionVariable.instantiateValuesFromSideProof(InitConfig initConfig,
Services services,
TermBuilder tb,
ApplyStrategyInfo info,
Operator resultOperator,
Term siteProofSelectTerm,
Term siteProofCondition)
Analyzes the side proof defined by the
ApplyStrategyInfo
and creates ExecutionValue s from it. |
protected Term |
ExecutionOperationContract.searchConstructorSelfDefinition(Term term,
KeYJavaType staticType,
Services services)
Tries to find the self
Term of the given KeYJavaType . |
protected Term |
ExecutionOperationContract.searchResultTerm(FunctionalOperationContract contract,
UseOperationContractRule.Instantiation inst,
Services services)
Searches the result
Term . |
Modifier and Type | Method and Description |
---|---|
protected java.lang.String |
AbstractElement.formatTerm(Term term,
Services services)
|
Constructor and Description |
---|
SymbolicAssociation(Services services,
IProgramVariable programVariable,
ISymbolicObject target,
Term condition,
IModelSettings settings)
Constructor.
|
SymbolicAssociation(Services services,
Term arrayIndex,
ISymbolicObject target,
Term condition,
IModelSettings settings)
Constructor.
|
SymbolicAssociation(Services services,
Term arrayIndex,
Term arrayStartIndex,
Term arrayEndIndex,
ISymbolicObject target,
Term condition,
IModelSettings settings)
Constructor.
|
SymbolicEquivalenceClass(Services services,
ImmutableList<Term> terms,
IModelSettings settings)
Constructor.
|
SymbolicEquivalenceClass(Services services,
IModelSettings settings)
Constructor.
|
SymbolicObject(Services services,
Term name,
IModelSettings settings)
Constructor.
|
SymbolicValue(Services services,
IProgramVariable programVariable,
Term value,
Term condition,
IModelSettings settings)
Constructor.
|
SymbolicValue(Services services,
Term arrayIndex,
Term value,
Term condition,
IModelSettings settings)
Constructor.
|
SymbolicValue(Services services,
Term arrayIndex,
Term arrayStartIndex,
Term arrayEndIndex,
Term value,
Term condition,
IModelSettings settings)
Constructor.
|
Modifier and Type | Method and Description |
---|---|
protected Term |
ProgramMethodPO.buildFrameClause(java.util.List<LocationVariable> modHeaps,
java.util.Map<Term,Term> heapToAtPre,
ProgramVariable selfVar,
ImmutableList<ProgramVariable> paramVars,
Services services)
Builds the frame clause including the modifies clause.
|
protected Term |
ProgramMethodSubsetPO.buildFreePre(ProgramVariable selfVar,
KeYJavaType selfKJT,
ImmutableList<ProgramVariable> paramVars,
java.util.List<LocationVariable> heaps,
Services proofServices)
Builds the "general assumption".
|
protected ImmutableList<StatementBlock> |
ProgramMethodPO.buildOperationBlocks(ImmutableList<LocationVariable> formalParVars,
ProgramVariable selfVar,
ProgramVariable resultVar,
Services services)
Builds the code to execute in different statement blocks.
|
protected ImmutableList<StatementBlock> |
ProgramMethodSubsetPO.buildOperationBlocks(ImmutableList<LocationVariable> formalParVars,
ProgramVariable selfVar,
ProgramVariable resultVar,
Services services)
Builds the code to execute in different statement blocks.
|
protected Term |
ProgramMethodSubsetPO.ensureUninterpretedPredicateExists(ImmutableList<ProgramVariable> paramVars,
ImmutableList<LocationVariable> formalParamVars,
ProgramVariable exceptionVar,
java.lang.String name,
Services proofServices)
|
protected Term |
ProgramMethodPO.generateMbyAtPreDef(ProgramVariable selfVar,
ImmutableList<ProgramVariable> paramVars,
Services services) |
protected Term |
ProgramMethodPO.getGlobalDefs(LocationVariable heap,
Term heapTerm,
Term selfTerm,
ImmutableList<Term> paramTerms,
Services services) |
protected Term |
ProgramMethodPO.getPost(java.util.List<LocationVariable> modHeaps,
ProgramVariable selfVar,
ImmutableList<ProgramVariable> paramVars,
ProgramVariable resultVar,
ProgramVariable exceptionVar,
java.util.Map<LocationVariable,LocationVariable> atPreVars,
Services services)
Creates the postcondition.
|
protected Term |
ProgramMethodPO.getPre(java.util.List<LocationVariable> modHeaps,
ProgramVariable selfVar,
ImmutableList<ProgramVariable> paramVars,
java.util.Map<LocationVariable,LocationVariable> atPreVars,
Services services)
Creates the precondition.
|
protected Term |
ProgramMethodSubsetPO.getPre(java.util.List<LocationVariable> modHeaps,
ProgramVariable selfVar,
ImmutableList<ProgramVariable> paramVars,
java.util.Map<LocationVariable,LocationVariable> atPreVars,
Services services)
Creates the precondition.
|
protected Term |
TruthValuePOExtension.labelPostTerm(Services services,
Term term)
Labels all predicates in the given
Term and its children with
a FormulaTermLabel . |
Term |
TruthValuePOExtension.modifyPostTerm(InitConfig proofConfig,
Services services,
Term postTerm)
Modifies the post condition.
|
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.
|
protected java.util.List<Triple<Term,java.util.Set<Term>,Node>> |
AbstractSideProofRule.computeResultsAndConditions(Services services,
Goal goal,
ProofEnvironment sideProofEnvironment,
Sequent sequentToProve,
Function newPredicate)
Starts the side proof and extracts the result
Term and conditions. |
protected Function |
AbstractSideProofRule.createResultConstant(Services services,
Sort sort)
Creates a constant which is used in the original
Proof to
store the computed result in form of QueryResult = ... |
protected Function |
AbstractSideProofRule.createResultFunction(Services services,
Sort sort)
Creates the result
Function used in a predicate to compute the result in the side proof. |
protected static SequentFormula |
AbstractSideProofRule.replace(PosInOccurrence pio,
Term newTerm,
Services services)
|
Modifier and Type | Method and Description |
---|---|
protected boolean |
ThinBackwardSlicer.accept(Node node,
Node previousChild,
Services services,
java.util.Set<Location> relevantLocations,
AbstractSlicer.SequentInfo info,
SourceElement activeStatement)
Decides if the given
Node is part of the slice or not. |
protected abstract boolean |
AbstractBackwardSlicer.accept(Node node,
Node previousChild,
Services services,
java.util.Set<Location> relevantLocations,
AbstractSlicer.SequentInfo info,
SourceElement activeStatement)
Decides if the given
Node is part of the slice or not. |
protected void |
AbstractSlicer.analyzeEquality(Services services,
Term equality,
java.util.Map<Location,java.util.SortedSet<Location>> aliases,
ReferencePrefix thisReference)
Analyzes the given equality
Term for aliased locations. |
protected void |
AbstractSlicer.analyzeEquivalenceClasses(Services services,
ImmutableList<ISymbolicEquivalenceClass> sec,
java.util.Map<Location,java.util.SortedSet<Location>> aliases,
ReferencePrefix thisReference)
Analyzes the gievn
ISymbolicEquivalenceClass es. |
protected void |
AbstractSlicer.analyzeHeapUpdate(Term term,
Services services,
HeapLDT heapLDT,
java.util.Map<Location,java.util.SortedSet<Location>> aliases,
ReferencePrefix thisReference)
Recursive utility method used by
#analyzeUpdate(Term, Services, HeapLDT, Map) to analyze a given update. |
protected void |
AbstractSlicer.analyzeSequent(Services services,
Sequent sequent,
java.util.Map<Location,java.util.SortedSet<Location>> aliases,
ReferencePrefix thisReference)
Analyzes the given
Sequent for equalities specified by top level formulas. |
protected void |
AbstractSlicer.analyzeUpdate(Term term,
Services services,
HeapLDT heapLDT,
java.util.Map<Location,java.util.SortedSet<Location>> aliases,
java.util.Map<ProgramVariable,Term> localValues,
ExecutionContext ec,
ReferencePrefix thisReference)
Recursive utility method used by
#analyzeUpdates(ImmutableList, Services, HeapLDT, Map) to analyze a given update. |
protected void |
AbstractSlicer.analyzeUpdates(ImmutableList<Term> updates,
Services services,
HeapLDT heapLDT,
java.util.Map<Location,java.util.SortedSet<Location>> aliases,
java.util.Map<ProgramVariable,Term> localValues,
ExecutionContext ec,
ReferencePrefix thisReference)
Utility method used by
#analyzeSequent(Node) to analyze the given updates. |
protected void |
AbstractSlicer.listModifiedHeapLocations(Term term,
Services services,
HeapLDT heapLDT,
java.util.List<Location> listToFill,
ReferencePrefix thisReference,
java.util.Set<Location> relevantLocations,
Node node)
Recursive utility method used by
#listModifiedLocations(Term, Services, HeapLDT, List, ReferencePrefix) to analyze a given update. |
protected void |
AbstractSlicer.listModifiedLocations(Term term,
Services services,
HeapLDT heapLDT,
java.util.List<Location> listToFill,
ExecutionContext ec,
ReferencePrefix thisReference,
java.util.Set<Location> relevantLocations,
Node node)
|
protected Location |
AbstractSlicer.normalizeAlias(Services services,
Location location,
AbstractSlicer.SequentInfo info)
Returns the representative alias for the given
Location . |
protected Location |
AbstractSlicer.normalizeAlias(Services services,
ReferencePrefix referencePrefix,
AbstractSlicer.SequentInfo info)
Returns the representative alias for the given
ReferencePrefix . |
protected boolean |
AbstractSlicer.performRemoveRelevant(Services services,
Location normalized,
java.util.Set<Location> relevantLocations,
AbstractSlicer.SequentInfo info)
Checks if the given
Location is directly or indirectly
contained (aliased) in the Set of relevant locations. |
protected boolean |
AbstractSlicer.removeRelevant(Services services,
Location location,
java.util.Set<Location> relevantLocations,
AbstractSlicer.SequentInfo info)
Checks if the given
Location is directly or indirectly
contained (aliased) in the Set of relevant locations. |
protected boolean |
AbstractSlicer.removeRelevant(Services services,
ReferencePrefix sourceElement,
java.util.Set<Location> relevantLocations,
AbstractSlicer.SequentInfo info)
Checks if the given
SourceElement is directly or indirectly
contained (aliased) in the Set of relevant locations. |
protected Location |
AbstractSlicer.toLocation(Services services,
ReferencePrefix prefix,
ExecutionContext ec,
ReferencePrefix thisReference)
Converts the given
ReferencePrefix into a Location . |
static Location |
AbstractSlicer.toLocation(Services services,
Term term)
|
protected ImmutableList<Access> |
AbstractSlicer.toLocationRecursive(Services services,
ReferencePrefix prefix,
ExecutionContext ec,
ReferencePrefix thisReference,
ImmutableList<Access> children)
Utility method used by
#toLocation(Services, ReferencePrefix, ReferencePrefix)
to recursively extract the Access instances. |
Term |
Location.toTerm(Services services)
|
static Term |
AbstractSlicer.toTerm(Services services,
Expression expression,
ExecutionContext ec)
Converts the given
Expression into a Term . |
static ImmutableArray<Term> |
AbstractSlicer.toTerm(Services services,
ImmutableArray<Expression> expressions,
ExecutionContext ec)
Converts the given
Expression s into Term s. |
protected void |
AbstractSlicer.updateAliases(Services services,
Location first,
Location second,
java.util.Map<Location,java.util.SortedSet<Location>> aliases,
ReferencePrefix thisReference)
Adds the found alias consisting of first and second
ReferencePrefix to the alias Map . |
protected java.util.Set<Location> |
AbstractBackwardSlicer.updateOutdatedLocations(Services services,
java.util.Set<Location> oldLocationsToUpdate,
java.util.Map<Location,java.util.SortedSet<Location>> newAliases,
java.util.Map<Location,java.util.SortedSet<Location>> oldAliases,
Location outdatedPrefix,
ReferencePrefix thisReference)
Updates the outdated locations.
|
protected void |
AbstractBackwardSlicer.updateRelevantLocations(ProgramElement read,
java.util.Set<Location> relevantLocations,
AbstractSlicer.SequentInfo info,
Services services)
Updates the relevant locations.
|
Modifier and Type | Method and Description |
---|---|
protected void |
CutHeapObjectsTermGenerator.collectEqualityTerms(SequentFormula sf,
java.util.Set<Term> equalityTerms,
java.util.Set<Term> topTerms,
HeapLDT heapLDT,
Services services)
Computes all possible equality terms between objects in the given
SequentFormula . |
Modifier and Type | Method and Description |
---|---|
static void |
SymbolicExecutionSideProofUtil.addNewNamesToNamespace(Services services,
Term term)
|
static boolean |
SymbolicExecutionUtil.canComputeVariables(IExecutionNode<?> node,
Services services)
Checks if it is right now possible to compute the variables of the given
IExecutionNode
via IExecutionNode.getVariables() . |
static java.util.List<Pair<Term,Node>> |
SymbolicExecutionSideProofUtil.computeResults(Services services,
Proof proof,
ProofEnvironment sideProofEnvironment,
Sequent sequentToProve,
TermLabel label,
java.lang.String description,
java.lang.String methodTreatment,
java.lang.String loopTreatment,
java.lang.String queryTreatment,
java.lang.String splittingOption,
boolean addNamesToServices)
Starts the side proof and extracts the result
Term . |
static java.util.List<Triple<Term,java.util.Set<Term>,Node>> |
SymbolicExecutionSideProofUtil.computeResultsAndConditions(Services services,
Proof proof,
ProofEnvironment sideProofEnvironment,
Sequent sequentToProve,
Operator operator,
java.lang.String description,
java.lang.String methodTreatment,
java.lang.String loopTreatment,
java.lang.String queryTreatment,
java.lang.String splittingOption,
boolean addNamesToServices)
Starts the side proof and extracts the result
Term and conditions. |
static boolean |
SymbolicExecutionSideProofUtil.containsIrrelevantThings(Services services,
SequentFormula sf,
java.util.Set<Operator> relevantThings)
Checks if the given
SequentFormula contains irrelevant things
(things which are not contained in the relevantThingsToProve and are no Java types) |
static boolean |
SymbolicExecutionUtil.containsStatement(ProgramElement toSearchIn,
SourceElement toSearch,
Services services)
Checks if the given
ProgramElement contains the given SourceElement . |
static SymbolicExecutionUtil.SiteProofVariableValueInput |
SymbolicExecutionUtil.createExtractReturnVariableValueSequent(Services services,
IExecutionContext context,
Node methodReturnNode,
Node methodCallEmptyNode,
IProgramVariable variable)
Creates a
Sequent which can be used in site proofs to
extract the return value of the given IProgramVariable from the
sequent of the given Node . |
static SymbolicExecutionUtil.SiteProofVariableValueInput |
SymbolicExecutionUtil.createExtractReturnVariableValueSequent(Services services,
TypeReference contextObjectType,
IProgramMethod contextMethod,
ReferencePrefix contextObject,
Node methodReturnNode,
Node methodCallEmptyNode,
IProgramVariable variable)
Creates a
Sequent which can be used in site proofs to
extract the return value of the given IProgramVariable from the
sequent of the given Node . |
static SymbolicExecutionUtil.SiteProofVariableValueInput |
SymbolicExecutionUtil.createExtractTermSequent(Services sideProofServices,
Node node,
PosInOccurrence pio,
Term additionalConditions,
Term term,
boolean keepUpdates)
Creates a
Sequent which can be used in site proofs to
extract the value of the given IProgramVariable from the
sequent of the given Node . |
static SymbolicExecutionUtil.SiteProofVariableValueInput |
SymbolicExecutionUtil.createExtractVariableValueSequent(Services services,
Node node,
PosInOccurrence pio,
Term additionalConditions,
IProgramVariable variable)
Creates a
Sequent which can be used in site proofs to
extract the value of the given IProgramVariable from the
sequent of the given Node . |
static java.util.Set<Operator> |
SymbolicExecutionSideProofUtil.extractRelevantThings(Services services,
Sequent sequentToProve)
|
static java.lang.String |
SymbolicExecutionUtil.formatTerm(Term term,
Services services,
boolean useUnicode,
boolean usePrettyPrinting)
|
static Term |
SymbolicExecutionUtil.getArrayIndex(Services services,
HeapLDT heapLDT,
Term arrayIndexTerm)
Returns the array index defined by the given
Term . |
static ProgramVariable |
SymbolicExecutionUtil.getProgramVariable(Services services,
HeapLDT heapLDT,
Term locationTerm)
Returns the
ProgramVariable defined by the given Term . |
static boolean |
SymbolicExecutionUtil.hasReferenceSort(Services services,
IProgramVariable var)
Checks if the
Sort of the given IProgramVariable is a reference type. |
static boolean |
SymbolicExecutionUtil.hasReferenceSort(Services services,
Sort sort)
Checks if the
Sort is a reference type. |
static boolean |
SymbolicExecutionUtil.hasReferenceSort(Services services,
Term term)
|
static Term |
SymbolicExecutionUtil.improveReadability(Term term,
Services services)
Improves the
Term to increase its readability. |
static Term |
SymbolicExecutionUtil.instantiateTerm(Node node,
Term term,
TacletApp tacletApp,
Services services)
|
static boolean |
SymbolicExecutionUtil.isBoolean(Services services,
Operator op)
Checks if the given
Operator is a boolean. |
static boolean |
SymbolicExecutionUtil.isHeapUpdate(Services services,
Term term)
Checks if the given
Term represents a heap update,
in particular a store or create operation on a heap. |
static boolean |
SymbolicExecutionSideProofUtil.isIrrelevantCondition(Services services,
Sequent initialSequent,
java.util.Set<Operator> relevantThingsInSequentToProve,
SequentFormula sf)
Checks if the given
SequentFormula is a relevant condition. |
static boolean |
SymbolicExecutionUtil.isNotImplicit(Services services,
IProgramMethod pm)
Checks if the given
IProgramMethod is not implicit. |
static boolean |
SymbolicExecutionUtil.isNullSort(Sort sort,
Services services)
|
protected static boolean |
SymbolicExecutionSideProofUtil.isRelevantThing(Services services,
Term term)
Checks if the given
Term describes a relevant thing. |
static boolean |
SymbolicExecutionUtil.isSelect(Services services,
Term term)
Checks if the given
Term is a select on a heap. |
static Term |
SymbolicExecutionUtil.replaceSkolemConstants(Sequent sequent,
Term term,
Services services)
Replaces all skolem constants in the given
Term . |
static SymbolicExecutionUtil.ContractPostOrExcPostExceptionVariableResult |
SymbolicExecutionUtil.searchContractPostOrExcPostExceptionVariable(Node node,
Services services)
Searches the used exception variable in the post or exceptional post branch of an applied
ContractRuleApp on the parent of the given Node . |
static Term |
SymbolicExecutionUtil.sequentToImplication(Sequent sequent,
Services services)
Converts the given
Sequent into an implication. |
Constructor and Description |
---|
ContainsIrrelevantThingsVisitor(Services services,
java.util.Set<Operator> relevantThings)
Constructor.
|
Modifier and Type | Method and Description |
---|---|
static void |
AssumptionGenerator.checkTable(byte[][] referenceTable,
Sort[] instTable,
Sort[] genericTable,
de.uka.ilkd.key.taclettranslation.assumptions.TacletConditions conditions,
Services services)
Checks the referenceTable whether there are rows that are not
allowed.
|
static boolean |
AssumptionGenerator.isAbstractOrInterface(Sort sort,
Services services) |
static boolean |
AssumptionGenerator.isReferenceSort(Sort sort,
Services services) |
Constructor and Description |
---|
AssumptionGenerator(Services services) |
DefaultTacletSetTranslation(Services services,
SMTSettings settings) |
Modifier and Type | Method and Description |
---|---|
java.lang.String |
UserDefinedSymbols.createHeader(Services services) |
java.lang.String |
UserDefinedSymbols.getRuleHeader(Services services) |
Constructor and Description |
---|
ModelGenerator(Goal s,
int target,
Services services) |
Constructor and Description |
---|
ModifiesSetTranslator(Services services,
OracleGenerator gen) |
OracleGenerator(Services services,
ReflectionClassCreator rflCreator,
boolean useRFL) |
OracleInvariantTranslator(Services services) |
Modifier and Type | Method and Description |
---|---|
static Services |
HelperClassForTests.createServices() |
static Services |
HelperClassForTests.createServices(java.io.File keyFile) |
Modifier and Type | Method and Description |
---|---|
static java.util.List<LocationVariable> |
MiscTools.applicableHeapContexts(Modality modality,
Services services)
Returns the applicable heap contexts out of the currently available set
of three contexts: The normal heap, the saved heap (transaction), and the
permission heap.
|
static IProgramMethod |
KeYTypeUtil.findExplicitConstructor(Services services,
IProgramMethod implicitConstructor)
Returns the
IProgramMethod of the explicit constructor for
the given implicit constructor. |
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.
|
static java.lang.String |
KeYTypeUtil.getParentName(Services services,
KeYJavaType type)
Returns the name of the parent package/type or
null if it has no one. |
static Term |
MiscTools.getSelfTerm(MethodFrame mf,
Services services)
Returns the receiver term of the passed method frame, or null if the frame belongs to a
static method.
|
static java.util.Optional<LoopSpecification> |
MiscTools.getSpecForTermWithLoopStmt(Term loopTerm,
Services services)
Returns the
LoopSpecification for the program in the given term,
the active statement of which has to be a loop statement. |
static KeYJavaType |
KeYTypeUtil.getType(Services services,
java.lang.String fullName)
Returns the
KeYJavaType fore the given name. |
static boolean |
KeYTypeUtil.isInnerType(Services services,
KeYJavaType type)
Checks if the given type is an inner or anonymous type.
|
static boolean |
MiscTools.isPermissions(Services services) |
static boolean |
KeYTypeUtil.isType(Services services,
java.lang.String fullName)
Checks if the given full name is a type in KeY.
|
static IProgramMethod |
HelperClassForTests.searchProgramMethod(Services services,
java.lang.String containerTypeName,
java.lang.String methodFullName)
Searches a
IProgramMethod in the given Services . |
Constructor and Description |
---|
InfFlowProgVarRenamer(Term[] terms,
java.util.Map<Term,Term> preInitialisedReplaceMap,
java.lang.String postfix,
Goal goalForVariableRegistration,
Services services) |
InfFlowProgVarRenamer(Term[] terms,
java.lang.String postfix,
Goal goalForVariableRegistration,
Services services) |
Modifier and Type | Method and Description |
---|---|
static Term |
MergeRuleUtils.allClosure(Term term,
Services services)
Universally closes all logical and location variables in the given term.
|
static void |
MergeRuleUtils.assertEquivalent(Term term1,
Term term2,
Services services,
int timeout)
Tries to prove the equivalence of term1 and term2 and throws a
RuntimeException if the proof fails. |
static Term |
MergeRuleUtils.createSimplifiedDisjunctivePathCondition(Term cond1,
Term cond2,
Services services,
int simplificationTimeout)
Creates a path condition that is equivalent to the disjunction of the two
supplied formulae, but possibly simpler.
|
static boolean |
MergeRuleUtils.equalsModBranchUniqueRenaming(SourceElement se1,
SourceElement se2,
Node node,
Services services)
An equals method that, before the comparison, replaces all program
locations in the supplied arguments by their branch-unique versions.
|
static Term |
MergeRuleUtils.exClosure(Term term,
Services services)
Existentially closes all logical and location variables in the given
term.
|
static MergeRuleUtils.Option<Pair<Term,Term>> |
MergeRuleUtils.getDistinguishingFormula(java.util.ArrayList<Term> conjElemsPathCond1,
java.util.ArrayList<Term> conjElemsPathCond2,
Services services) |
static MergeRuleUtils.Option<Pair<Term,Term>> |
MergeRuleUtils.getDistinguishingFormula(Term pathCondition1,
Term pathCondition2,
Services services)
Computes a formula that implies pathCondition1 and, if pathCondition1 and
pathCondition2 are contradicting, does not imply pathCondition2.
|
static LocationVariable |
MergeRuleUtils.getFreshLocVariableForPrefix(java.lang.String prefix,
Sort sort,
Services services)
Computes and registers a fresh location variable with the given prefix in
its name of the given sort.
|
static LogicVariable |
MergeRuleUtils.getFreshVariableForPrefix(java.lang.String prefix,
Sort sort,
Services services)
Computes and registers a fresh variable with the given prefix in its name
of the given sort.
|
static ImmutableSet<LocationVariable> |
MergeRuleUtils.getLocationVariables(Term term,
Services services)
Returns all program variables in the given term.
|
static java.util.HashSet<LocationVariable> |
MergeRuleUtils.getLocationVariablesHashSet(Sequent sequent,
Services services)
Returns all program variables in the given sequent.
|
static java.util.HashSet<LocationVariable> |
MergeRuleUtils.getLocationVariablesHashSet(Term term,
Services services)
Returns all program variables in the given term.
|
static Function |
MergeRuleUtils.getNewSkolemConstantForPrefix(java.lang.String prefix,
Sort sort,
Services services)
Computes and registers a new Skolem constant with the given prefix in its
name of the given sort.
|
static Pair<SymbolicExecutionState,SymbolicExecutionState> |
MergeRuleUtils.handleNameClashes(SymbolicExecutionState mergeState,
SymbolicExecutionState mergePartnerState,
Services services)
Due to the introduction of local namespaces, we run into trouble when
applying state merging in the presence of locally introduced symbols.
|
static boolean |
MergeRuleUtils.isProvable(Sequent toProve,
Services services,
int timeout)
Tries to prove the given formula without splitting and returns whether
the prove could be closed.
|
static boolean |
MergeRuleUtils.isProvable(Term toProve,
Services services,
int timeout)
Tries to prove the given formula without splitting and returns whether
the prove could be closed.
|
static boolean |
MergeRuleUtils.isProvableWithSplitting(Sequent toProve,
Services services,
int timeout)
Tries to prove the given formula with splitting and returns whether the
prove could be closed.
|
static boolean |
MergeRuleUtils.isProvableWithSplitting(Term toProve,
Services services,
int timeout)
Tries to prove the given formula with splitting and returns whether the
prove could be closed.
|
static Pair<Sort,Name> |
MergeRuleUtils.parsePlaceholder(java.lang.String input,
boolean registerInNamespaces,
Services services)
Parses a declaration of the type "<SORT> <NAME>", where
<SORT> must be a sort known to the proof and <NAME> must be a
fresh name.
|
static Pair<Sort,Name> |
MergeRuleUtils.parsePlaceholder(java.lang.String input,
Services services)
Parses a declaration of the type "<SORT> <NAME>", where
<SORT> must be a sort known to the proof and <NAME> must be a
fresh name.
|
static AbstractionPredicate |
MergeRuleUtils.parsePredicate(java.lang.String input,
java.util.ArrayList<Pair<Sort,Name>> registeredPlaceholders,
NamespaceSet localNamespaces,
Services services)
Parses an abstraction predicate.
|
static boolean |
MergeRuleUtils.pathConditionsAreDistinguishable(Term pathCondition1,
Term pathCondition2,
Services services)
Checks if two given path conditions are distinguishable.
|
static SymbolicExecutionState |
MergeRuleUtils.sequentToSEPair(Node node,
PosInOccurrence pio,
Services services)
Converts a sequent (given by goal & pos in occurrence) to an SE state
(U,C).
|
static SymbolicExecutionStateWithProgCnt |
MergeRuleUtils.sequentToSETriple(Node node,
PosInOccurrence pio,
Services services)
Converts a sequent (given by goal & pos in occurrence) to an SE state
(U,C,p).
|
static Term |
MergeRuleUtils.substConstantsByFreshVars(Term term,
java.util.HashMap<Function,LogicVariable> replMap,
Services services)
Substitutes all constants in the given term by fresh variables.
|
static Term |
MergeRuleUtils.substConstantsByFreshVars(Term term,
java.util.HashSet<Function> restrictTo,
java.util.HashMap<Function,LogicVariable> replMap,
Services services)
Substitutes all constants in the given term that are contained in the set
restrictTo by fresh variables.
|
static Term |
MergeRuleUtils.translateToFormula(Services services,
java.lang.String toTranslate)
Translates a String into a formula or to null if not applicable.
|
Constructor and Description |
---|
ProofExplorationService(Proof proof,
Services services) |
Constructor and Description |
---|
LogPrinter(Services services) |
Copyright © 2003-2019 The KeY-Project.