Constructor and Description |
---|
SearchNode(SequentFormula[] pattern,
int succAntPos,
ImmutableList<IfFormulaInstantiation> antec,
ImmutableList<IfFormulaInstantiation> succ) |
SearchNode(SequentFormula[] pattern,
int succAntPos,
ImmutableList<IfFormulaInstantiation> antec,
ImmutableList<IfFormulaInstantiation> succ) |
Modifier and Type | Method and Description |
---|---|
ImmutableList<BuiltInRule> |
AbstractProofControl.getBuiltInRule(Goal focusedGoal,
PosInOccurrence pos) |
ImmutableList<BuiltInRule> |
ProofControl.getBuiltInRule(Goal focusedGoal,
PosInOccurrence pos)
collects all built-in rules that are applicable at the given sequent
position 'pos'.
|
ImmutableList<TacletApp> |
AbstractProofControl.getFindTaclet(Goal focusedGoal,
PosInOccurrence pos) |
ImmutableList<TacletApp> |
ProofControl.getFindTaclet(Goal focusedGoal,
PosInOccurrence pos)
collects all applicable FindTaclets of the current goal (called by the
SequentViewer)
|
ImmutableList<TacletApp> |
AbstractProofControl.getNoFindTaclet(Goal focusedGoal) |
ImmutableList<TacletApp> |
ProofControl.getNoFindTaclet(Goal focusedGoal)
collects all applicable NoFindTaclets of the current goal (called by the
SequentViewer)
|
ImmutableList<TacletApp> |
AbstractProofControl.getRewriteTaclet(Goal focusedGoal,
PosInOccurrence pos) |
ImmutableList<TacletApp> |
ProofControl.getRewriteTaclet(Goal focusedGoal,
PosInOccurrence pos)
collects all applicable RewriteTaclets of the current goal (called by the
SequentViewer)
|
Modifier and Type | Method and Description |
---|---|
void |
AbstractProofControl.startAndWaitForAutoMode(Proof proof,
ImmutableList<Goal> goals)
Starts the auto mode for the given proof which must be contained
in this user interface and blocks the current thread until it
has finished.
|
void |
ProofControl.startAndWaitForAutoMode(Proof proof,
ImmutableList<Goal> goals)
Starts the auto mode for the given proof which must be contained
in this user interface and blocks the current thread until it
has finished.
|
void |
AbstractProofControl.startAutoMode(Proof proof,
ImmutableList<Goal> goals)
|
void |
ProofControl.startAutoMode(Proof proof,
ImmutableList<Goal> goals)
|
void |
DefaultProofControl.startAutoMode(Proof proof,
ImmutableList<Goal> goals,
ProverTaskListener ptl) |
protected abstract void |
AbstractProofControl.startAutoMode(Proof proof,
ImmutableList<Goal> goals,
ProverTaskListener ptl) |
Modifier and Type | Method and Description |
---|---|
static IfFormulaInstantiation[] |
TacletAssumesModel.createIfInsts(ImmutableList<IfFormulaInstantiation> candidates) |
Constructor and Description |
---|
TacletAssumesModel(Term ifFma,
ImmutableList<IfFormulaInstantiation> candidates,
TacletApp app,
Goal goal,
Services services,
NamespaceSet nss,
AbbrevMap scm) |
Modifier and Type | Method and Description |
---|---|
ImmutableList<MergePartner> |
MergePartnerSelectionDialog.getChosenCandidates() |
Constructor and Description |
---|
MergePartnerSelectionDialog(Goal mergeGoal,
PosInOccurrence pio,
ImmutableList<MergePartner> candidates,
Services services)
Creates a new merge partner selection dialog.
|
Modifier and Type | Method and Description |
---|---|
static ImmutableList<TacletApp> |
CurrentGoalViewMenu.removeRewrites(ImmutableList<TacletApp> list)
removes RewriteTaclet from list
|
static ImmutableList<TacletApp> |
CurrentGoalViewMenu.sort(ImmutableList<TacletApp> finds,
CurrentGoalViewMenu.TacletAppComparator comp)
This method is also used by the KeYIDE has to be static and public.
|
Modifier and Type | Method and Description |
---|---|
static ImmutableList<TacletApp> |
CurrentGoalViewMenu.removeRewrites(ImmutableList<TacletApp> list)
removes RewriteTaclet from list
|
static ImmutableList<TacletApp> |
CurrentGoalViewMenu.sort(ImmutableList<TacletApp> finds,
CurrentGoalViewMenu.TacletAppComparator comp)
This method is also used by the KeYIDE has to be static and public.
|
Constructor and Description |
---|
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
|
Modifier and Type | Method and Description |
---|---|
ProofMacroFinishedInfo |
StartAuxiliaryLoopComputationMacro.applyTo(UserInterfaceControl uic,
Proof proof,
ImmutableList<Goal> goals,
PosInOccurrence posInOcc,
ProverTaskListener listener) |
ProofMacroFinishedInfo |
FinishAuxiliaryLoopComputationMacro.applyTo(UserInterfaceControl uic,
Proof proof,
ImmutableList<Goal> goals,
PosInOccurrence posInOcc,
ProverTaskListener listener) |
ProofMacroFinishedInfo |
StartAuxiliaryBlockComputationMacro.applyTo(UserInterfaceControl uic,
Proof proof,
ImmutableList<Goal> goals,
PosInOccurrence posInOcc,
ProverTaskListener listener) |
ProofMacroFinishedInfo |
FinishAuxiliaryBlockComputationMacro.applyTo(UserInterfaceControl uic,
Proof proof,
ImmutableList<Goal> goals,
PosInOccurrence posInOcc,
ProverTaskListener listener) |
ProofMacroFinishedInfo |
StartAuxiliaryMethodComputationMacro.applyTo(UserInterfaceControl uic,
Proof proof,
ImmutableList<Goal> goals,
PosInOccurrence posInOcc,
ProverTaskListener listener) |
ProofMacroFinishedInfo |
ExhaustiveProofMacro.applyTo(UserInterfaceControl uic,
Proof proof,
ImmutableList<Goal> goals,
PosInOccurrence posInOcc,
ProverTaskListener listener) |
ProofMacroFinishedInfo |
FinishAuxiliaryMethodComputationMacro.applyTo(UserInterfaceControl uic,
Proof proof,
ImmutableList<Goal> goals,
PosInOccurrence posInOcc,
ProverTaskListener listener) |
boolean |
StartAuxiliaryLoopComputationMacro.canApplyTo(Proof proof,
ImmutableList<Goal> goals,
PosInOccurrence posInOcc) |
boolean |
SelfcompositionStateExpansionMacro.canApplyTo(Proof proof,
ImmutableList<Goal> goals,
PosInOccurrence posInOcc)
Can this macro be applied on the given goals?
This method should not make any changes but check if the macro can be
applied or not on the given goals.
|
boolean |
FinishAuxiliaryLoopComputationMacro.canApplyTo(Proof proof,
ImmutableList<Goal> goals,
PosInOccurrence posInOcc) |
boolean |
StartAuxiliaryBlockComputationMacro.canApplyTo(Proof proof,
ImmutableList<Goal> goals,
PosInOccurrence posInOcc) |
boolean |
StateExpansionAndInfFlowContractApplicationMacro.canApplyTo(Proof proof,
ImmutableList<Goal> goals,
PosInOccurrence posInOcc)
Can this macro be applied on the given goals?
This method should not make any changes but check if the macro can be
applied or not on the given goals.
|
boolean |
FullUseInformationFlowContractMacro.canApplyTo(Proof proof,
ImmutableList<Goal> goals,
PosInOccurrence posInOcc)
Can this macro be applied on the given goals?
This method should not make any changes but check if the macro can be
applied or not on the given goals.
|
boolean |
FullInformationFlowAutoPilotMacro.canApplyTo(Proof proof,
ImmutableList<Goal> goals,
PosInOccurrence posInOcc)
Can this macro be applied on the given goals?
This method should not make any changes but check if the macro can be
applied or not on the given goals.
|
boolean |
FinishAuxiliaryBlockComputationMacro.canApplyTo(Proof proof,
ImmutableList<Goal> goals,
PosInOccurrence posInOcc) |
boolean |
StartAuxiliaryMethodComputationMacro.canApplyTo(Proof proof,
ImmutableList<Goal> goals,
PosInOccurrence posInOcc) |
boolean |
ExhaustiveProofMacro.canApplyTo(Proof proof,
ImmutableList<Goal> goals,
PosInOccurrence posInOcc) |
boolean |
FinishAuxiliaryMethodComputationMacro.canApplyTo(Proof proof,
ImmutableList<Goal> goals,
PosInOccurrence posInOcc) |
Modifier and Type | Method and Description |
---|---|
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.
|
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.
|
Modifier and Type | Field and Description |
---|---|
ImmutableList<Term> |
StateVars.localVars |
ImmutableList<Term> |
StateVars.paddedTermList |
ImmutableList<Term> |
StateVars.termList |
Constructor and Description |
---|
StateVars(Term self,
ImmutableList<Term> localVars,
Term heap) |
StateVars(Term self,
ImmutableList<Term> localVars,
Term result,
Term exception,
Term heap) |
StateVars(Term self,
ImmutableList<Term> localVars,
Term result,
Term exception,
Term heap,
Term mbyAtPre) |
StateVars(Term self,
Term guard,
ImmutableList<Term> localVars,
Term heap) |
StateVars(Term self,
Term guard,
ImmutableList<Term> localVars,
Term result,
Term exception,
Term heap) |
StateVars(Term self,
Term guard,
ImmutableList<Term> localVars,
Term result,
Term exception,
Term heap,
Term mbyAtPre) |
Modifier and Type | Field and Description |
---|---|
static Properties.Property<ImmutableList<Term>> |
InfFlowContractAppTacletExecutor.INF_FLOW_CONTRACT_APPL_PROPERTY
Strategy property which saves the list of formulas which where added
by information flow contract applications.
|
Modifier and Type | Method and Description |
---|---|
ImmutableList<KeYJavaType> |
JavaInfo.createSignature(ImmutableArray<? extends Expression> arguments)
retrieves the signature according to the given expressions
|
protected ImmutableList<Field> |
CreateArrayMethodBuilder.filterField(FieldDeclaration field)
extracts all fields out of fielddeclaration
|
protected ImmutableList<Field> |
CreateArrayMethodBuilder.filterField(ImmutableArray<MemberDeclaration> list)
extracts all field specifications out of the given list.
|
protected ImmutableList<Field> |
CreateArrayMethodBuilder.filterImplicitFields(ImmutableList<Field> list)
extracts all implicit field specifications out of the given list
|
ImmutableList<KeYJavaType> |
KeYProgModelInfo.findImplementations(Type ct,
java.lang.String name,
ImmutableList<KeYJavaType> signature) |
ImmutableList<ProgramVariable> |
JavaInfo.getAllAttributes(java.lang.String programName,
KeYJavaType type) |
ImmutableList<ProgramVariable> |
JavaInfo.getAllAttributes(java.lang.String programName,
KeYJavaType type,
boolean traverseSubtypes)
returns a list of all attributes with the given program name
declared in one of type's sub- or supertype including
its own attributes
Attention:
The type must not denote the null type
|
ImmutableList<Field> |
JavaInfo.getAllFields(TypeDeclaration classDecl)
retrieves all attributes locally declared in class cl
(inclusive the implicit attributes)
The returned list is in source code order.
|
ImmutableList<Field> |
KeYProgModelInfo.getAllFieldsLocallyDeclaredIn(KeYJavaType ct)
returns the fields defined within the given class type.
|
ImmutableList<Method> |
JavaInfo.getAllMethods(KeYJavaType kjt)
returns all methods from the given Type
|
ImmutableList<Method> |
KeYProgModelInfo.getAllMethods(KeYJavaType kjt)
Returns all visible methods that are defined in this
class type or any of its supertypes.
|
ImmutableList<IProgramMethod> |
JavaInfo.getAllProgramMethods(KeYJavaType kjt)
returns all methods from the given Type as IProgramMethods
|
ImmutableList<IProgramMethod> |
KeYProgModelInfo.getAllProgramMethods(KeYJavaType kjt)
Returns all visible methods that are defined in this
class type or any of its supertypes.
|
ImmutableList<ProgramMethod> |
JavaInfo.getAllProgramMethodsLocallyDeclared(KeYJavaType kjt)
returns all methods declared in the given Type as IProgramMethods
|
ImmutableList<ProgramMethod> |
KeYProgModelInfo.getAllProgramMethodsLocallyDeclared(KeYJavaType ct)
Returns the ProgramMethods locally defined within the given
class type.
|
ImmutableList<KeYJavaType> |
JavaInfo.getAllSubtypes(KeYJavaType type)
returns all proper subtypes of a given type
|
ImmutableList<KeYJavaType> |
KeYProgModelInfo.getAllSubtypes(KeYJavaType ct)
Returns all proper subtypes of the given class type
|
ImmutableList<KeYJavaType> |
JavaInfo.getAllSupertypes(KeYJavaType type)
returns all supertypes of a given type
|
ImmutableList<KeYJavaType> |
KeYProgModelInfo.getAllSupertypes(KeYJavaType ct)
Returns all known supertypes of the given class type with the type itself
as first element.
|
ImmutableList<Field> |
KeYProgModelInfo.getAllVisibleFields(KeYJavaType ct)
returns all in ct visible fields
declared in ct or one of its supertypes
in topological order starting with the fields of
the given type
If the type is represented in source code, the returned list
matches the syntactic order.
|
ImmutableList<KeYJavaType> |
JavaInfo.getCommonSubtypes(KeYJavaType k1,
KeYJavaType k2)
returns the list of all common subtypes of types k1 and k2
(inclusive one of them if they are equal or subtypes themselves)
attention: Null is not a jav atype only a logic sort, i.e.
|
ImmutableList<IProgramMethod> |
JavaInfo.getConstructors(KeYJavaType kjt) |
ImmutableList<IProgramMethod> |
KeYProgModelInfo.getConstructors(KeYJavaType ct)
Returns the constructors locally defined within the given
class type.
|
ImmutableList<KeYJavaType> |
JavaInfo.getDirectSuperTypes(KeYJavaType type)
returns all direct supertypes (local declared types in extends and
implements) if extends is not given explict java.lang.Object is added
(it is not added for interfaces)
|
ImmutableList<Field> |
JavaInfo.getImplicitFields(ClassDeclaration cl)
retrieves all implicit attributes locally declared in the given class
The returned list is in source code order.
|
ImmutableList<Method> |
JavaInfo.getMethods(KeYJavaType kjt)
returns all locally declared methods from the given Type
|
ImmutableList<Method> |
KeYProgModelInfo.getMethods(KeYJavaType ct)
Returns the methods locally defined within the given
class type.
|
ImmutableList<Method> |
KeYProgModelInfo.getMethods(KeYJavaType ct,
java.lang.String m,
ImmutableList<Type> signature,
KeYJavaType context)
Returns the list of most specific methods with the given
name that are defined in the given type or in a supertype
where they are visible for the given type, and have a signature
that is compatible to the given one.
|
ImmutableList<LDT> |
TypeConverter.getModels() |
Modifier and Type | Method and Description |
---|---|
protected java.util.List<Statement> |
CreateArrayMethodBuilder.createArray(ImmutableList<Field> fields)
creates the statements which take the next object out of the list of
available objects
|
protected de.uka.ilkd.key.java.Context |
Recoder2KeY.createContext(ImmutableList<ProgramVariable> pvs)
create a new context with a temporary name and make a list of variables
visible from within.
|
protected de.uka.ilkd.key.java.Context |
Recoder2KeY.createContext(ImmutableList<ProgramVariable> vars,
CrossReferenceSourceInfo csi)
create a new Context with a temporary name and make a list of variables
visible from within.
|
protected ImmutableList<Field> |
CreateArrayMethodBuilder.filterImplicitFields(ImmutableList<Field> list)
extracts all implicit field specifications out of the given list
|
protected ProgramVariable |
CreateArrayMethodBuilder.find(java.lang.String name,
ImmutableList<Field> fields)
retrieves a field with the given name out of the list
|
ImmutableList<KeYJavaType> |
KeYProgModelInfo.findImplementations(Type ct,
java.lang.String name,
ImmutableList<KeYJavaType> signature) |
IProgramMethod |
JavaInfo.getConstructor(KeYJavaType kjt,
ImmutableList<KeYJavaType> signature) |
IProgramMethod |
KeYProgModelInfo.getConstructor(KeYJavaType ct,
ImmutableList<KeYJavaType> signature)
retrieves the most specific constructor declared in the given type with
respect to the given signature
|
protected StatementBlock |
CreateArrayMethodBuilder.getCreateArrayHelperBody(ProgramVariable length,
ImmutableList<Field> fields,
boolean createTransient,
ProgramVariable transientType)
creates the body of method
<createArrayHelper(int
paramLength)>
therefore it first adds the statements responsible to take the correct
one out of the list, then the arrays length attribute is set followed by
a call to <prepare>() setting the arrays fields on
their default value. |
IProgramMethod |
CreateArrayMethodBuilder.getCreateArrayHelperMethod(TypeReference arrayTypeReference,
ProgramVariable length,
ImmutableList<Field> fields)
create the method declaration of the
<createArrayHelper> method |
IProgramMethod |
CreateArrayMethodBuilder.getCreateArrayMethod(TypeReference arrayTypeReference,
IProgramMethod prepare,
ImmutableList<Field> fields)
creates the implicit method
<createArray> it
fulfills a similar purpose as <createObject> in
addition it sets the arrays length and calls the prepare method |
ImmutableList<Method> |
KeYProgModelInfo.getMethods(KeYJavaType ct,
java.lang.String m,
ImmutableList<Type> signature,
KeYJavaType context)
Returns the list of most specific methods with the given
name that are defined in the given type or in a supertype
where they are visible for the given type, and have a signature
that is compatible to the given one.
|
IProgramMethod |
CreateArrayMethodBuilder.getPrepareArrayMethod(TypeRef arrayRef,
ProgramVariable length,
Expression defaultValue,
ImmutableList<Field> fields)
returns the prepare method for arrays initialising all array fields with
their default value
|
IProgramMethod |
JavaInfo.getProgramMethod(KeYJavaType classType,
java.lang.String methodName,
ImmutableList<? extends Type> signature,
KeYJavaType context)
returns the program methods defined in the given KeYJavaType with name
m and the list of types as signature of the method
|
IProgramMethod |
KeYProgModelInfo.getProgramMethod(KeYJavaType ct,
java.lang.String m,
ImmutableList<? extends Type> signature,
KeYJavaType context)
Returns the IProgramMethods with the given name that is defined
in the given type or in a supertype where it is visible for the
given type, and has a signature that is compatible to the given one.
|
IProgramMethod |
JavaInfo.getToplevelPM(KeYJavaType kjt,
java.lang.String methodName,
ImmutableList<KeYJavaType> sig) |
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.
|
ImmutableList<KeYJavaType> |
NullType.getSupertypes()
Returns the array of locally declared supertypes of this class type.
|
ImmutableList<KeYJavaType> |
ClassType.getSupertypes()
Returns the array of locally declared supertypes of 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
|
ImmutableList<KeYJavaType> |
InterfaceDeclaration.getSupertypes()
returns the local declared supertypes
|
ImmutableList<KeYJavaType> |
ArrayDeclaration.getSupertypes()
returns the local declared supertypes
|
abstract ImmutableList<KeYJavaType> |
TypeDeclaration.getSupertypes()
returns the local declared supertypes
|
ImmutableList<KeYJavaType> |
ClassDeclaration.getSupertypes()
returns the local declared supertypes
|
ImmutableList<KeYJavaType> |
SuperArrayDeclaration.getSupertypes()
returns the local declared supertypes
|
ImmutableList<ClassType> |
TypeDeclaration.getTypes(Services services)
TO BE IMPLEMENTED
|
Modifier and Type | Field and Description |
---|---|
static ImmutableList<java.lang.String> |
JMLTransformer.javaMods |
Modifier and Type | Method and Description |
---|---|
static ImmutableList<PositionedString> |
JMLTransformer.getWarningsOfLastInstance() |
Modifier and Type | Method and Description |
---|---|
ImmutableList<KeYJavaType> |
MethodReference.getMethodSignature(Services services,
ExecutionContext ec)
determines the arguments types and constructs a signature of the current
method
|
Modifier and Type | Method and Description |
---|---|
IProgramMethod |
MethodReference.method(Services services,
KeYJavaType classType,
ImmutableList<KeYJavaType> signature,
KeYJavaType context) |
Modifier and Type | Method and Description |
---|---|
ImmutableList<ProgramElement> |
JavaASTCollector.getNodes()
returns the found nodes of the specified type
|
ImmutableList<SchemaVariable> |
ProgramSVCollector.getSchemaVariables() |
Constructor and Description |
---|
ProgramSVCollector(ProgramElement root,
ImmutableList<SchemaVariable> vars)
create the ProgramSVCollector
|
ProgramSVCollector(ProgramElement root,
ImmutableList<SchemaVariable> vars,
SVInstantiations svInst)
create the ProgramSVCollector
|
Modifier and Type | Method and Description |
---|---|
ImmutableList<LocationVariable> |
HeapLDT.getAllHeaps() |
Modifier and Type | Method and Description |
---|---|
ImmutableList<SequentFormula> |
SequentChangeInfo.addedFormulas()
The formulas added to the sequent are returned as a concatenated list of
the formulas added to each semisequent.
|
ImmutableList<SequentFormula> |
SemisequentChangeInfo.addedFormulas()
returns the list of all added constrained formulas
|
ImmutableList<SequentFormula> |
SequentChangeInfo.addedFormulas(boolean antec)
The formulas added to one of the semisequents are returned.
|
ImmutableList<Term> |
TermBuilder.apply(Term update,
ImmutableList<Term> targets) |
ImmutableList<Term> |
TermBuilder.applyElementary(Term heap,
java.lang.Iterable<Term> targets) |
ImmutableList<SequentFormula> |
Sequent.asList()
Returns a list containing every
SequentFormula in this sequent. |
ImmutableList<SequentFormula> |
Semisequent.asList() |
ImmutableList<SequentFormula> |
SemisequentChangeInfo.getFormulaList()
returns the list of constrained formula of the new semisequent
|
ImmutableList<IProgramMethod> |
MethodStackInfo.getMethodStack()
returns the method call stack
|
ImmutableList<Sort> |
TermBuilder.getSorts(java.lang.Iterable<Term> terms)
|
ImmutableList<FormulaChangeInfo> |
SequentChangeInfo.modifiedFormulas()
The formulas modified within the sequent are returned as a
concatenated list of the formulas modified within each each
semisequent.
|
ImmutableList<FormulaChangeInfo> |
SemisequentChangeInfo.modifiedFormulas()
returns the list of all modification positions
|
ImmutableList<FormulaChangeInfo> |
SequentChangeInfo.modifiedFormulas(boolean antec)
The formulas modified within one of the semisequents are
returned.
|
ImmutableList<ProgramVariable> |
TermBuilder.paramVars(IObserverFunction obs,
boolean makeNamesUnique)
Creates program variables for the parameters.
|
ImmutableList<ProgramVariable> |
TermBuilder.paramVars(java.lang.String postfix,
IObserverFunction obs,
boolean makeNamesUnique)
Creates program variables for the parameters.
|
ImmutableList<SequentFormula> |
SequentChangeInfo.rejectedFormulas()
Returns the formulas that have been rejected when trying to add as being redundant.
|
ImmutableList<SequentFormula> |
SemisequentChangeInfo.rejectedFormulas()
returns a list of formulas that have been tried to add to
the semisequent but got rejected as they were redundant
|
ImmutableList<SequentFormula> |
SequentChangeInfo.rejectedFormulas(boolean antec)
Returns the formulas that have been rejected when trying to add as being redundant.
|
ImmutableList<SequentFormula> |
SequentChangeInfo.removedFormulas()
The formulas removed from the sequent are returned as a
concatenated list of the formulas removed from each semisequent.
|
ImmutableList<SequentFormula> |
SemisequentChangeInfo.removedFormulas()
returns the list of all removed constrained formulas
|
ImmutableList<SequentFormula> |
SequentChangeInfo.removedFormulas(boolean antec)
The formulas removed from one of the semisequents are returned.
|
ImmutableList<Term> |
TermBuilder.var(java.lang.Iterable<ProgramVariable> vs) |
ImmutableList<Term> |
TermBuilder.var(ProgramVariable... vs) |
ImmutableList<Term> |
TermBuilder.wd(java.lang.Iterable<Term> l) |
Modifier and Type | Method and Description |
---|---|
static Pair<ImmutableList<Term>,Term> |
TermBuilder.goBelowUpdates2(Term term)
Removes leading updates from the passed term.
|
Modifier and Type | Method and Description |
---|---|
SequentChangeInfo |
Sequent.addFormula(ImmutableList<SequentFormula> insertions,
boolean antec,
boolean first)
adds list of formulas to the antecedent (or succedent) of the sequent.
|
SequentChangeInfo |
Sequent.addFormula(ImmutableList<SequentFormula> insertions,
PosInOccurrence p)
adds the formulas of list insertions to the sequent starting at position p.
|
ImmutableList<Term> |
TermBuilder.apply(Term update,
ImmutableList<Term> targets) |
Term |
TermBuilder.applyParallel(ImmutableList<Term> updates,
Term target) |
Term |
TermBuilder.applySequential(ImmutableList<Term> updates,
Term target) |
Term |
TermBuilder.applyUpdatePairsSequential(ImmutableList<SVInstantiations.UpdateLabelPair> updates,
Term target) |
SequentChangeInfo |
Sequent.changeFormula(ImmutableList<SequentFormula> replacements,
PosInOccurrence p)
replaces the formula at position p with the head of the given list and adds
the remaining list elements to the sequent (NOTICE:Sequent determines index
using identity (==) not equality.)
|
protected ProgramElementName |
VariableNamer.getNameProposalForSchemaVariable(java.lang.String basename,
SchemaVariable sv,
PosInOccurrence posOfFind,
PosInProgram posOfDeclaration,
ImmutableList<java.lang.String> previousProposals)
proposes a unique name for the instantiation of a schema variable
(like getProposal(), but somewhat less nicely)
|
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) |
Term |
TermBuilder.ifEx(ImmutableList<QuantifiableVariable> qvs,
Term cond,
Term _then,
Term _else)
Construct a term with the \ifEx operator.
|
SemisequentChangeInfo |
Semisequent.insert(int idx,
ImmutableList<SequentFormula> insertionList)
inserts the elements of the list at the specified index
performing redundancy checks
|
SemisequentChangeInfo |
Semisequent.insertFirst(ImmutableList<SequentFormula> insertions)
inserts element at index 0 performing redundancy
checks, this may result in returning same semisequent if
inserting would create redundancies
|
SemisequentChangeInfo |
Semisequent.insertLast(ImmutableList<SequentFormula> insertions)
inserts the formulas of the list at the end of the semisequent
performing redundancy checks, this may result in returning same
semisequent if inserting would create redundancies
|
Term |
TermBuilder.max(ImmutableList<? extends QuantifiableVariable> qvs,
Term range,
Term t,
TermServices services)
minimum operator
|
Term |
TermBuilder.min(ImmutableList<? extends QuantifiableVariable> qvs,
Term range,
Term t,
TermServices services)
minimum operator
|
Term |
TermBuilder.parallel(ImmutableList<Term> updates) |
Term |
TermBuilder.prod(ImmutableList<QuantifiableVariable> qvs,
Term range,
Term t,
TermServices services)
General (unbounded) product
|
SemisequentChangeInfo |
Semisequent.replace(int idx,
ImmutableList<SequentFormula> replacements)
replaces the formula at position
idx by the given list of formulas |
SemisequentChangeInfo |
Semisequent.replace(PosInOccurrence pos,
ImmutableList<SequentFormula> replacements)
replaces the element at place idx with the first element of the
given list and adds the rest of the list to the semisequent
behind the replaced formula
|
Term |
TermBuilder.seq(ImmutableList<Term> terms) |
Term |
TermBuilder.sequential(ImmutableList<Term> updates) |
void |
SemisequentChangeInfo.setFormulaList(ImmutableList<SequentFormula> list)
sets the list of constrained formula containing all formulas of
the semisequent after the operation
|
Term |
TermBuilder.sum(ImmutableList<QuantifiableVariable> qvs,
Term range,
Term t)
General (unbounded) sum
|
protected java.lang.Iterable<ProgramElementName> |
VariableNamer.wrapGlobals(ImmutableList<? extends Named> globals)
creates a Globals object for use with other internal methods
|
Constructor and Description |
---|
SemisequentChangeInfo(ImmutableList<SequentFormula> formulas) |
Modifier and Type | Method and Description |
---|---|
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.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.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 . |
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 |
---|---|
ImmutableList<LocationVariable> |
ProgramMethod.collectParameters() |
ImmutableList<LocationVariable> |
IProgramMethod.collectParameters() |
ImmutableList<LocationVariable> |
ProgramSV.collectParameters() |
Modifier and Type | Method and Description |
---|---|
ImmutableList<Goal> |
ProofMacroFinishedInfo.getGoals() |
Modifier and Type | Method and Description |
---|---|
ProofMacroFinishedInfo |
FinishSymbolicExecutionUntilMergePointMacro.applyTo(UserInterfaceControl uic,
Proof proof,
ImmutableList<Goal> goals,
PosInOccurrence posInOcc,
ProverTaskListener listener) |
ProofMacroFinishedInfo |
SequentialOnLastGoalProofMacro.applyTo(UserInterfaceControl uic,
Proof proof,
ImmutableList<Goal> goals,
PosInOccurrence posInOcc,
ProverTaskListener listener)
Apply this macro on the given goals.
|
ProofMacroFinishedInfo |
SequentialProofMacro.applyTo(UserInterfaceControl uic,
Proof proof,
ImmutableList<Goal> goals,
PosInOccurrence posInOcc,
ProverTaskListener listener)
Apply this macro on the given goals.
|
ProofMacroFinishedInfo |
ProofMacro.applyTo(UserInterfaceControl uic,
Proof proof,
ImmutableList<Goal> goals,
PosInOccurrence posInOcc,
ProverTaskListener listener)
Apply this macro on the given goals.
|
ProofMacroFinishedInfo |
AlternativeMacro.applyTo(UserInterfaceControl uic,
Proof proof,
ImmutableList<Goal> goals,
PosInOccurrence posInOcc,
ProverTaskListener listener)
Apply this macro on the given goals.
|
ProofMacroFinishedInfo |
TryCloseMacro.applyTo(UserInterfaceControl uic,
Proof proof,
ImmutableList<Goal> goals,
PosInOccurrence posInOcc,
ProverTaskListener listener) |
ProofMacroFinishedInfo |
StrategyProofMacro.applyTo(UserInterfaceControl uic,
Proof proof,
ImmutableList<Goal> goals,
PosInOccurrence posInOcc,
ProverTaskListener listener) |
ProofMacroFinishedInfo |
DoWhileFinallyMacro.applyTo(UserInterfaceControl uic,
Proof proof,
ImmutableList<Goal> goals,
PosInOccurrence posInOcc,
ProverTaskListener listener) |
ProofMacroFinishedInfo |
AbstractBlastingMacro.applyTo(UserInterfaceControl uic,
Proof proof,
ImmutableList<Goal> goals,
PosInOccurrence posInOcc,
ProverTaskListener listener) |
ProofMacroFinishedInfo |
SkipMacro.applyTo(UserInterfaceControl uic,
Proof proof,
ImmutableList<Goal> goals,
PosInOccurrence posInOcc,
ProverTaskListener listener) |
boolean |
WellDefinednessMacro.canApplyTo(Proof proof,
ImmutableList<Goal> goals,
PosInOccurrence posInOcc) |
boolean |
SequentialProofMacro.canApplyTo(Proof proof,
ImmutableList<Goal> goals,
PosInOccurrence posInOcc)
Can this macro be applied on the given goals?
This method should not make any changes but check if the macro can be
applied or not on the given goals.
|
boolean |
ProofMacro.canApplyTo(Proof proof,
ImmutableList<Goal> goals,
PosInOccurrence posInOcc)
Can this macro be applied on the given goals?
This method should not make any changes but check if the macro can be
applied or not on the given goals.
|
boolean |
AlternativeMacro.canApplyTo(Proof proof,
ImmutableList<Goal> goals,
PosInOccurrence posInOcc)
Can this macro be applied on the given goals?
This method should not make any changes but check if the macro can be
applied or not on the given goals.
|
boolean |
TryCloseMacro.canApplyTo(Proof proof,
ImmutableList<Goal> goals,
PosInOccurrence posInOcc) |
boolean |
StrategyProofMacro.canApplyTo(Proof proof,
ImmutableList<Goal> goals,
PosInOccurrence posInOcc)
Can this macro be applied on the given goals?
This method should not make any changes but check if the macro can be
applied or not on the given goals.
|
boolean |
DoWhileFinallyMacro.canApplyTo(Proof proof,
ImmutableList<Goal> goals,
PosInOccurrence posInOcc) |
boolean |
SkipMacro.canApplyTo(Proof proof,
ImmutableList<Goal> goals,
PosInOccurrence posInOcc) |
Constructor and Description |
---|
ProofMacroFinishedInfo(ProofMacro macro,
ImmutableList<Goal> goals) |
Modifier and Type | Method and Description |
---|---|
protected static Goal |
EngineState.getGoal(ImmutableList<Goal> openGoals,
Node node) |
Modifier and Type | Method and Description |
---|---|
ImmutableList<Taclet> |
TacletPBuilder.visitTacletlist(KeYParser.TacletlistContext ctx) |
Modifier and Type | Method and Description |
---|---|
ImmutableList<SequentPrintFilterEntry> |
SequentPrintFilter.getFilteredAntec()
Get the formulas of the filtered antecedent and the constraints to use for
instantiating metavariables when printing
|
ImmutableList<SequentPrintFilterEntry> |
IdentitySequentPrintFilter.getFilteredAntec()
Get the formulas of the filtered antecedent and the constraints to use for
instantiating metavariables when printing
|
ImmutableList<SequentPrintFilterEntry> |
ShowSelectedSequentPrintFilter.getFilteredAntec() |
ImmutableList<SequentPrintFilterEntry> |
SequentPrintFilter.getFilteredSucc()
Get the formulas of the filtered succcedent and the constraints to use for
instantiating metavariables when printing
|
ImmutableList<SequentPrintFilterEntry> |
IdentitySequentPrintFilter.getFilteredSucc()
Get the formulas of the filtered succcedent and the constraints to use for
instantiating metavariables when printing
|
ImmutableList<SequentPrintFilterEntry> |
ShowSelectedSequentPrintFilter.getFilteredSucc() |
protected ImmutableList<java.lang.Integer> |
PositionTable.pathForIndex(int index)
Returns the path to the `lowest' position table that includes
index in its range. |
ImmutableList<java.lang.Integer> |
InitialPositionTable.pathForPosition(PosInOccurrence pio,
SequentPrintFilter filter)
Returns the path for a given PosInOccurrence.
|
Modifier and Type | Method and Description |
---|---|
protected PosInSequent |
PositionTable.getSequentPIS(ImmutableList<java.lang.Integer> posList,
SequentPrintFilter filter)
Returns a PosInSequent for a given position list, but without filling in
the bounds.
|
protected void |
LogicPrinter.printRules(ImmutableList<Taclet> rules) |
void |
LogicPrinter.printSemisequent(ImmutableList<SequentPrintFilterEntry> formulas) |
Range |
InitialPositionTable.rangeForPath(ImmutableList<java.lang.Integer> path)
Returns the character range for the subtable indicated
by the given integer list.
|
Range |
PositionTable.rangeForPath(ImmutableList<java.lang.Integer> path,
int length) |
Modifier and Type | Field and Description |
---|---|
protected ImmutableList<NoPosTacletApp> |
TacletIndex.noFindList
contains NoFind-Taclets
|
Modifier and Type | Field and Description |
---|---|
protected java.util.HashMap<java.lang.Object,ImmutableList<NoPosTacletApp>> |
TacletIndex.antecList
contains antecedent Taclets
|
protected java.util.HashMap<java.lang.Object,ImmutableList<NoPosTacletApp>> |
TacletIndex.rwList
contains rewrite Taclets
|
protected java.util.HashMap<java.lang.Object,ImmutableList<NoPosTacletApp>> |
TacletIndex.succList
contains succedent Taclets
|
Modifier and Type | Method and Description |
---|---|
ImmutableList<Goal> |
Proof.allGoals()
Returns the list of all, open and closed, goals.
|
ImmutableList<RuleApp> |
Goal.appliedRuleApps()
returns set of rules applied at this branch
|
ImmutableList<Goal> |
Goal.apply(RuleApp ruleApp) |
ImmutableList<Goal> |
Proof.closedGoals()
Returns the list of closed goals, needed to make pruning in closed branches
possible.
|
static ImmutableList<NoPosTacletApp> |
TermTacletAppIndex.filter(RuleFilter p_filter,
ImmutableList<NoPosTacletApp> taclets) |
ImmutableList<NoPosTacletApp> |
TacletIndex.getAntecedentTaclet(PosInOccurrence pos,
RuleFilter filter,
Services services)
get all Taclets for the antecedent.
|
ImmutableList<IBuiltInRuleApp> |
BuiltInRuleAppIndex.getBuiltInRule(Goal goal,
PosInOccurrence pos)
returns a list of built-in rules application applicable
for the given goal and position
|
ImmutableList<IBuiltInRuleApp> |
RuleAppIndex.getBuiltInRules(Goal g,
PosInOccurrence pos)
returns a list of built-in rule applications applicable
for the given goal, user defined constraint and position
|
ImmutableList<Goal> |
Proof.getClosedSubtreeGoals(Node node)
Returns a list of all (closed) goals of the closed subtree pending from this node.
|
ImmutableList<NoPosTacletApp> |
TacletAppIndex.getFindTaclet(PosInOccurrence pos,
TacletFilter filter,
TermServices services)
collects all FindTaclets with instantiations and position
|
ImmutableList<NoPosTacletApp> |
RuleAppIndex.getFindTaclet(TacletFilter filter,
PosInOccurrence pos,
TermServices services)
collects all FindTacletInstantiations for the given
heuristics and position
|
ImmutableList<Goal> |
ProofTreeEvent.getGoals() |
ImmutableList<IProgramVariable> |
Node.getLocalProgVars()
Returns the set of created program variables known in this node.
|
ImmutableList<FormulaChangeInfo> |
FormulaTagManager.getModifications(FormulaTag p_tag) |
ImmutableList<Goal> |
ProofEvent.getNewGoals()
returns the list of new goals (empty if a goal was closed) in case of a rule
application otherwise null
|
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
|
ImmutableList<NoPosTacletApp> |
TacletIndex.getPartialInstantiatedApps()
returns a list with all partial instantiated no pos taclet apps
|
ImmutableList<Name> |
NameRecorder.getProposals() |
ImmutableList<RenamingTable> |
Node.getRenamingTable() |
ImmutableList<NoPosTacletApp> |
TacletIndex.getRewriteTaclet(PosInOccurrence pos,
RuleFilter filter,
Services services)
get all Rewrite-Taclets.
|
ImmutableList<NoPosTacletApp> |
TacletAppIndex.getRewriteTaclet(PosInOccurrence pos,
TacletFilter filter,
TermServices services)
collects all RewriteTacletInstantiations in a subterm of the
constrainedFormula described by a PosInOccurrence.
|
ImmutableList<NoPosTacletApp> |
RuleAppIndex.getRewriteTaclet(TacletFilter filter,
PosInOccurrence pos,
TermServices services)
collects all RewriteTacletInstantiations for the given
heuristics in a subterm of the constraintformula described by a
PosInOccurrence
|
ImmutableList<Goal> |
Proof.getSubtreeEnabledGoals(Node node)
get the list of goals of the subtree starting with node which are enabled.
|
ImmutableList<Goal> |
Proof.getSubtreeGoals(Node node)
returns the list of goals of the subtree starting with node.
|
ImmutableList<NoPosTacletApp> |
TacletIndex.getSuccedentTaclet(PosInOccurrence pos,
RuleFilter filter,
Services services)
get all Taclets for the succedent.
|
ImmutableList<NoPosTacletApp> |
TermTacletAppIndex.getTacletAppAt(PosInOccurrence pos,
RuleFilter p_filter) |
ImmutableList<NoPosTacletApp> |
SemisequentTacletAppIndex.getTacletAppAt(PosInOccurrence pos,
RuleFilter filter) |
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
|
ImmutableList<Goal> |
Proof.openEnabledGoals()
return the list of open and enabled goals
|
ImmutableList<Goal> |
Proof.openGoals()
Returns the list of open goals.
|
ImmutableList<Node> |
Proof.pruneProof(Node cuttingPoint)
Prunes the subtree beneath the node
cuttingPoint , i.e. |
ImmutableList<Node> |
Proof.pruneProof(Node cuttingPoint,
boolean fireChanges) |
ImmutableList<Term> |
OpReplacer.replace(ImmutableList<Term> terms)
Replaces in a list of terms.
|
static ImmutableList<Term> |
OpReplacer.replace(Term toReplace,
Term with,
ImmutableList<Term> in,
TermFactory tf)
Replace a sub-term.
|
static ImmutableList<Term> |
OpReplacer.replace(Term toReplace,
Term with,
ImmutableList<Term> in,
TermFactory tf,
Proof proof)
Replace a sub-term.
|
ImmutableList<InfFlowSpec> |
OpReplacer.replaceInfFlowSpec(ImmutableList<InfFlowSpec> terms)
Replaces in a list of triples of lists of terms.
|
ImmutableList<BuiltInRule> |
BuiltInRuleIndex.rules()
returns all available rules
|
ImmutableList<Goal> |
Goal.split(int n)
creates n new nodes as children of the
referenced node and new
n goals that have references to these new nodes.
|
Modifier and Type | Method and Description |
---|---|
void |
Proof.add(ImmutableList<Goal> goals)
adds a list with new goals to the list of open goals
|
static ImmutableList<NoPosTacletApp> |
TermTacletAppIndex.filter(RuleFilter p_filter,
ImmutableList<NoPosTacletApp> taclets) |
protected void |
Goal.fireGoalReplaced(Goal goal,
Node parent,
ImmutableList<Goal> newGoals) |
protected void |
Proof.fireProofGoalsAdded(ImmutableList<Goal> goals)
fires the event that new goals have been added to the list of
goals
|
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) |
void |
GoalListener.goalReplaced(Goal source,
Node parent,
ImmutableList<Goal> newGoals)
Informs the listener that the given goal
source
has been replaced by the goals newGoals (note that
source may be an element of
newGoals ). |
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 |
Proof.replace(Goal oldGoal,
ImmutableList<Goal> newGoals)
removes the given goal and adds the new goals in list
|
ImmutableList<Term> |
OpReplacer.replace(ImmutableList<Term> terms)
Replaces in a list of terms.
|
static ImmutableList<Term> |
OpReplacer.replace(Term toReplace,
Term with,
ImmutableList<Term> in,
TermFactory tf)
Replace a sub-term.
|
static ImmutableList<Term> |
OpReplacer.replace(Term toReplace,
Term with,
ImmutableList<Term> in,
TermFactory tf,
Proof proof)
Replace a sub-term.
|
ImmutableList<InfFlowSpec> |
OpReplacer.replaceInfFlowSpec(ImmutableList<InfFlowSpec> terms)
Replaces in a list of triples of lists of terms.
|
void |
NewRuleListener.rulesAdded(ImmutableList<? extends RuleApp> rule,
PosInOccurrence pos)
Called when a collection of new RuleApps is added
|
void |
NullNewRuleListener.rulesAdded(ImmutableList<? extends RuleApp> rule,
PosInOccurrence pos) |
void |
NameRecorder.setProposals(ImmutableList<Name> proposals) |
void |
Node.setRenamings(ImmutableList<RenamingTable> list) |
Constructor and Description |
---|
BuiltInRuleIndex(ImmutableList<BuiltInRule> rules)
creates a new index with the given built-in-rules
|
PrefixTermTacletAppIndexCacheImpl(ImmutableList<QuantifiableVariable> prefix,
java.util.Map<PrefixTermTacletAppIndexCacheImpl.CacheKey,TermTacletAppIndex> cache) |
ProofEvent(Proof source,
RuleAppInfo rai,
ImmutableList<Goal> newGoals)
creates a proof event for a change triggered by a rule applications
|
ProofTreeEvent(Proof source,
ImmutableList<Goal> goals)
Create ProofTreeEvent for the event that affects the goals
given in the list.
|
TacletIndex(java.util.HashMap<java.lang.Object,ImmutableList<NoPosTacletApp>> rwList,
java.util.HashMap<java.lang.Object,ImmutableList<NoPosTacletApp>> antecList,
java.util.HashMap<java.lang.Object,ImmutableList<NoPosTacletApp>> succList,
ImmutableList<NoPosTacletApp> noFindList,
java.util.HashSet<NoPosTacletApp> partialInstantiatedRuleApps) |
Constructor and Description |
---|
TacletIndex(java.util.HashMap<java.lang.Object,ImmutableList<NoPosTacletApp>> rwList,
java.util.HashMap<java.lang.Object,ImmutableList<NoPosTacletApp>> antecList,
java.util.HashMap<java.lang.Object,ImmutableList<NoPosTacletApp>> succList,
ImmutableList<NoPosTacletApp> noFindList,
java.util.HashSet<NoPosTacletApp> partialInstantiatedRuleApps) |
TacletIndex(java.util.HashMap<java.lang.Object,ImmutableList<NoPosTacletApp>> rwList,
java.util.HashMap<java.lang.Object,ImmutableList<NoPosTacletApp>> antecList,
java.util.HashMap<java.lang.Object,ImmutableList<NoPosTacletApp>> succList,
ImmutableList<NoPosTacletApp> noFindList,
java.util.HashSet<NoPosTacletApp> partialInstantiatedRuleApps) |
TacletIndex(java.util.HashMap<java.lang.Object,ImmutableList<NoPosTacletApp>> rwList,
java.util.HashMap<java.lang.Object,ImmutableList<NoPosTacletApp>> antecList,
java.util.HashMap<java.lang.Object,ImmutableList<NoPosTacletApp>> succList,
ImmutableList<NoPosTacletApp> noFindList,
java.util.HashSet<NoPosTacletApp> partialInstantiatedRuleApps) |
Modifier and Type | Field and Description |
---|---|
static ImmutableList<IProofReferencesAnalyst> |
ProofReferenceUtil.DEFAULT_ANALYSTS
The default
IProofReferencesAnalyst s. |
Modifier and Type | Method and Description |
---|---|
static java.util.LinkedHashSet<IProofReference<?>> |
ProofReferenceUtil.computeProofReferences(Node node,
Services services,
ImmutableList<IProofReferencesAnalyst> analysts)
Computes the
IProofReference of the given Node . |
static java.util.LinkedHashSet<IProofReference<?>> |
ProofReferenceUtil.computeProofReferences(Proof proof,
ImmutableList<IProofReferencesAnalyst> analysts)
|
Modifier and Type | Method and Description |
---|---|
ImmutableList<NodeGoalPair> |
DelayedCut.getGoalsAfterUncovering() |
ImmutableList<Node> |
DelayedCut.getSubtrees() |
Constructor and Description |
---|
DelayedCut(Proof proof,
Node node,
Term formula,
ImmutableList<Node> subtrees,
int sideOfDecisionPredicate,
RuleApp firstAppliedRuleApp) |
Modifier and Type | Field and Description |
---|---|
ImmutableList<Term> |
ProofObligationVars.formalParams
The formal parameters of a method.
|
ImmutableList<ProgramVariable> |
WellDefinednessPO.Variables.params |
Modifier and Type | Method and Description |
---|---|
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.
|
ImmutableList<BuiltInRule> |
InitConfig.builtInRules()
returns the built-in rules of this initial configuration
|
protected ImmutableList<TermLabelManager.TermLabelConfiguration> |
JavaProfile.computeTermLabelConfiguration()
Computes the
TermLabelManager.TermLabelConfiguration to use in this Profile . |
protected abstract ImmutableList<TermLabelManager.TermLabelConfiguration> |
AbstractProfile.computeTermLabelConfiguration()
Computes the
TermLabelManager.TermLabelConfiguration to use in this Profile . |
static ImmutableList<POExtension> |
ProofInitServiceUtil.getOperationPOExtension(ProofOblInput po)
Returns the
POExtension which supports the given ProofOblInput . |
ImmutableList<BuiltInRule> |
RuleCollection.getStandardBuiltInRules()
returns a list of all built in rules to be used
|
ImmutableList<Taclet> |
InitConfig.getTaclets() |
protected ImmutableList<BuiltInRule> |
JavaProfile.initBuiltInRules() |
protected ImmutableList<BuiltInRule> |
AbstractProfile.initBuiltInRules() |
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 . |
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 JavaBlock |
AbstractOperationPO.buildJavaBlock(ImmutableList<LocationVariable> formalParVars,
ProgramVariable selfVar,
ProgramVariable resultVar,
ProgramVariable exceptionVar,
boolean transaction,
ImmutableList<StatementBlock> sb)
Creates the try catch block to execute.
|
protected JavaBlock |
AbstractOperationPO.buildJavaBlock(ImmutableList<LocationVariable> formalParVars,
ProgramVariable selfVar,
ProgramVariable resultVar,
ProgramVariable exceptionVar,
boolean transaction,
ImmutableList<StatementBlock> sb)
Creates the try catch block to execute.
|
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.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.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 |
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.
|
protected Term |
FunctionalOperationContractPO.buildUpdate(ImmutableList<ProgramVariable> paramVars,
ImmutableList<LocationVariable> formalParamVars,
java.util.Map<LocationVariable,LocationVariable> atPreVars,
Services services)
Builds the initial updates.
|
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 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 |
AbstractOperationPO.generateParamsOK(ImmutableList<ProgramVariable> paramVars)
Generates the general assumption that all parameter arguments are valid.
|
protected Term |
AbstractOperationPO.generateParamsOK2(ImmutableList<Term> paramVars)
Generates the general assumption that all parameter arguments are valid.
|
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 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(ImmutableList<ProgramVariable> pvs,
Services services) |
void |
InitConfig.setTaclets(ImmutableList<Taclet> tacs) |
Constructor and Description |
---|
ProofObligationVars(StateVars pre,
StateVars post,
Term exceptionParameter,
ImmutableList<Term> formalParams,
Services services) |
ProofObligationVars(StateVars pre,
StateVars post,
Term exceptionParameter,
ImmutableList<Term> formalParams,
TermBuilder tb) |
RuleCollection(RuleSource standardTaclets,
ImmutableList<BuiltInRule> standardBuiltInRules) |
Variables(ProgramVariable self,
ProgramVariable result,
ProgramVariable exception,
java.util.Map<LocationVariable,ProgramVariable> atPres,
ImmutableList<ProgramVariable> params,
LocationVariable heap,
Term anonHeap) |
Modifier and Type | Method and Description |
---|---|
java.lang.String |
OutputStreamProofSaver.builtinRuleIfInsts(Node node,
ImmutableList<PosInOccurrence> ifInsts) |
java.lang.String |
OutputStreamProofSaver.ifFormulaInsts(Node node,
ImmutableList<IfFormulaInstantiation> l) |
Modifier and Type | Method and Description |
---|---|
ImmutableList<Pair<java.lang.Integer,PosInTerm>> |
BuiltInAppIntermediate.getBuiltInIfInsts() |
ImmutableList<java.lang.String> |
TacletAppIntermediate.getIfDirectFormulaList() |
ImmutableList<java.lang.String> |
TacletAppIntermediate.getIfSeqFormulaList() |
ImmutableList<Name> |
BuiltInAppIntermediate.getNewNames() |
ImmutableList<Name> |
TacletAppIntermediate.getNewNames() |
abstract ImmutableList<Name> |
AppIntermediate.getNewNames() |
Constructor and Description |
---|
BuiltInAppIntermediate(java.lang.String ruleName,
Pair<java.lang.Integer,PosInTerm> pos,
java.lang.String contract,
ImmutableList<Pair<java.lang.Integer,PosInTerm>> builtInIfInsts,
ImmutableList<Name> newNames) |
BuiltInAppIntermediate(java.lang.String ruleName,
Pair<java.lang.Integer,PosInTerm> pos,
java.lang.String contract,
ImmutableList<Pair<java.lang.Integer,PosInTerm>> builtInIfInsts,
ImmutableList<Name> newNames) |
MergeAppIntermediate(java.lang.String ruleName,
Pair<java.lang.Integer,PosInTerm> pos,
int id,
java.lang.String joinProc,
int nrPartners,
ImmutableList<Name> newNames,
java.lang.String distinguishingFormula,
java.lang.Class<? extends AbstractPredicateAbstractionLattice> predAbstrLatticeType,
java.lang.String abstractionPredicates,
java.lang.String userChoices)
Constructs a new join rule.
|
MergePartnerAppIntermediate(java.lang.String ruleName,
Pair<java.lang.Integer,PosInTerm> pos,
int mergeNodeId,
ImmutableList<Name> newNames)
Constructs a new close-merge-partner intermediate application.
|
TacletAppIntermediate(java.lang.String tacletName,
Pair<java.lang.Integer,PosInTerm> posInfo,
java.util.LinkedList<java.lang.String> insts,
ImmutableList<java.lang.String> ifSeqFormulaList,
ImmutableList<java.lang.String> ifDirectFormulaList,
ImmutableList<Name> newNames)
Constructs a new intermediate taclet application.
|
TacletAppIntermediate(java.lang.String tacletName,
Pair<java.lang.Integer,PosInTerm> posInfo,
java.util.LinkedList<java.lang.String> insts,
ImmutableList<java.lang.String> ifSeqFormulaList,
ImmutableList<java.lang.String> ifDirectFormulaList,
ImmutableList<Name> newNames)
Constructs a new intermediate taclet application.
|
TacletAppIntermediate(java.lang.String tacletName,
Pair<java.lang.Integer,PosInTerm> posInfo,
java.util.LinkedList<java.lang.String> insts,
ImmutableList<java.lang.String> ifSeqFormulaList,
ImmutableList<java.lang.String> ifDirectFormulaList,
ImmutableList<Name> newNames)
Constructs a new intermediate taclet application.
|
Modifier and Type | Method and Description |
---|---|
void |
JoinProcessor.Listener.endOfJoining(ImmutableList<Goal> goals) |
Modifier and Type | Field and Description |
---|---|
ImmutableList<SequentChangeInfo> |
NodeChangesHolder.scis |
Modifier and Type | Method and Description |
---|---|
void |
NodeChangeJournal.goalReplaced(Goal source,
Node parent,
ImmutableList<Goal> newGoals)
Informs the listener that the given goal
source
has been replaced by the goals newGoals (note that
source may be an element of
newGoals ). |
Constructor and Description |
---|
NodeReplacement(Node p_node,
Node p_parent,
ImmutableList<SequentChangeInfo> p_changes) |
Constructor and Description |
---|
IHTacletFilter(boolean interactive,
ImmutableList<RuleSet> heuristics) |
Modifier and Type | Method and Description |
---|---|
void |
GoalChooser.init(Proof p_proof,
ImmutableList<Goal> p_goals)
Initialise this DefaultGoalChooser for use with a given Proof and a list of goals.
|
ApplyStrategyInfo |
ProverCore.start(Proof proof,
ImmutableList<Goal> goals)
starts a proof search for a set of goals using the given strategy settings
instead the ones configures in the proof
|
ApplyStrategyInfo |
ProverCore.start(Proof proof,
ImmutableList<Goal> goals,
int maxSteps,
long timeout,
boolean stopAtFirstNonCloseableGoal)
This entry point to the proof may provide inconsistent data.
|
ApplyStrategyInfo |
ProverCore.start(Proof proof,
ImmutableList<Goal> goals,
StrategySettings stratSet)
starts a proof search for a set of goals using the given strategy settings
instead the ones configures in the proof
|
void |
GoalChooser.updateGoalList(Node node,
ImmutableList<Goal> newGoals)
The given node has become an internal node of the proof tree, and the
children of the node are the given goals
|
Modifier and Type | Field and Description |
---|---|
protected ImmutableList<Goal> |
DefaultGoalChooser.goalList
list of goals on which the strategy should be applied
|
protected ImmutableList<Goal> |
DefaultGoalChooser.nextGoals
part of goalList that should be worked on next
|
protected ImmutableList<Goal> |
DefaultGoalChooser.selectedList
Subset of the goals to which currently taclets are applied.
|
Modifier and Type | Method and Description |
---|---|
protected ImmutableList<Goal> |
DefaultGoalChooser.insertNewGoals(ImmutableList<Goal> newGoals,
ImmutableList<Goal> prevGoalList) |
protected ImmutableList<Goal> |
DepthFirstGoalChooser.insertNewGoals(ImmutableList<Goal> newGoals,
ImmutableList<Goal> prevGoalList) |
protected static ImmutableList<Goal> |
DefaultGoalChooser.rotateList(ImmutableList<Goal> p_list) |
Modifier and Type | Method and Description |
---|---|
void |
DefaultGoalChooser.init(Proof p_proof,
ImmutableList<Goal> p_goals) |
protected ImmutableList<Goal> |
DefaultGoalChooser.insertNewGoals(ImmutableList<Goal> newGoals,
ImmutableList<Goal> prevGoalList) |
protected ImmutableList<Goal> |
DefaultGoalChooser.insertNewGoals(ImmutableList<Goal> newGoals,
ImmutableList<Goal> prevGoalList) |
protected ImmutableList<Goal> |
DepthFirstGoalChooser.insertNewGoals(ImmutableList<Goal> newGoals,
ImmutableList<Goal> prevGoalList) |
protected ImmutableList<Goal> |
DepthFirstGoalChooser.insertNewGoals(ImmutableList<Goal> newGoals,
ImmutableList<Goal> prevGoalList) |
protected static ImmutableList<Goal> |
DefaultGoalChooser.rotateList(ImmutableList<Goal> p_list) |
protected void |
DefaultGoalChooser.setupGoals(ImmutableList<Goal> p_goals) |
ApplyStrategyInfo |
ApplyStrategy.start(Proof proof,
ImmutableList<Goal> goals) |
ApplyStrategyInfo |
ApplyStrategy.start(Proof proof,
ImmutableList<Goal> goals,
int maxSteps,
long timeout,
boolean stopAtFirstNonCloseableGoal) |
ApplyStrategyInfo |
ApplyStrategy.start(Proof proof,
ImmutableList<Goal> goals,
StrategySettings stratSet) |
void |
DefaultGoalChooser.updateGoalList(Node node,
ImmutableList<Goal> newGoals) |
protected void |
DefaultGoalChooser.updateGoalListHelp(Node node,
ImmutableList<Goal> newGoals) |
protected void |
DepthFirstGoalChooser.updateGoalListHelp(Node node,
ImmutableList<Goal> newGoals) |
Modifier and Type | Field and Description |
---|---|
ImmutableList<Term> |
UseOperationContractRule.Instantiation.actualParams
The actual parameter terms.
|
ImmutableList<AbstractLoopInvariantRule.AnonUpdateData> |
AbstractLoopInvariantRule.AdditionalHeapTerms.anonUpdateData |
ImmutableList<AbstractLoopInvariantRule.AnonUpdateData> |
AbstractLoopInvariantRule.LoopInvariantInformation.anonUpdateData
Anonymizing updates for all heaps.
|
ImmutableList<Goal> |
AbstractLoopInvariantRule.LoopInvariantInformation.goals
The goals created by the invariant rules application; those are
filled with content by the concrete loop invariant rules.
|
protected ImmutableList<IfFormulaInstantiation> |
TacletApp.ifInstantiations
chosen instantiations for the if sequent formulas
|
protected ImmutableList<PosInOccurrence> |
AbstractBuiltInRuleApp.ifInsts |
protected ImmutableList<RuleSet> |
Taclet.ruleSets
list of rulesets (formerly known as heuristics) the taclet belongs to
|
protected ImmutableList<SchemaVariable> |
TacletSchemaVariableCollector.varList
collects all found variables
|
Modifier and Type | Method and Description |
---|---|
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 ImmutableList<Term> |
AbstractBlockContractRule.buildLocalOutsAtPost(ImmutableList<Term> varTerms,
Services services) |
protected static ImmutableList<Term> |
AbstractBlockContractRule.buildLocalOutsAtPre(ImmutableList<Term> varTerms,
Services services) |
protected ImmutableList<SchemaVariable> |
TacletSchemaVariableCollector.collectSVInProgram(JavaBlock jb,
ImmutableList<SchemaVariable> vars)
collects all SchemVariables that occur in the JavaBlock
|
static ImmutableList<Term> |
UseOperationContractRule.computeParams(Term baseHeapTerm,
java.util.Map<LocationVariable,Term> atPres,
LocationVariable baseHeap,
UseOperationContractRule.Instantiation inst,
TermFactory tf)
Returns the correct parameter terms.
|
static ImmutableList<IfFormulaInstantiation> |
IfFormulaInstSeq.createList(Sequent p_s,
boolean antec,
Services services) |
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".
|
ImmutableList<IfFormulaInstantiation> |
IfFormulaInstantiationCache.get(boolean antec,
Semisequent s) |
ImmutableList<Term> |
Trigger.getAvoidConditions() |
ImmutableList<IfFormulaInstantiation> |
IfMatchResult.getFormulas() |
ImmutableList<MatchConditions> |
IfMatchResult.getMatchConditions() |
ImmutableList<RuleSet> |
Taclet.getRuleSets() |
ImmutableList<VariableCondition> |
Taclet.getVariableConditions() |
ImmutableList<VariableCondition> |
TacletApplPart.getVariableConditions()
returns the list of additional generic conditions on
instantiations of schema variables.
|
ImmutableList<TacletGoalTemplate> |
Taclet.goalTemplates()
returns an iterator over the goal descriptions.
|
ImmutableList<IfFormulaInstantiation> |
TacletApp.ifFormulaInstantiations() |
ImmutableList<PosInOccurrence> |
IBuiltInRuleApp.ifInsts() |
ImmutableList<PosInOccurrence> |
AbstractBuiltInRuleApp.ifInsts() |
ImmutableList<NewVarcond> |
Taclet.varsNew()
returns an iterator over the variables that are new in the Taclet.
|
ImmutableList<NewVarcond> |
TacletApplPart.varsNew()
returns the list of variables that are new in a Taclet
|
ImmutableList<NewDependingOn> |
Taclet.varsNewDependingOn() |
ImmutableList<NewDependingOn> |
TacletApplPart.varsNewDependingOn()
returns the list of variable pairs that represent the
"new depending on" relation of a Taclet
|
ImmutableList<NotFreeIn> |
Taclet.varsNotFreeIn()
returns an iterator over the variable pairs that indicate that are
new in the Taclet.
|
ImmutableList<NotFreeIn> |
TacletApplPart.varsNotFreeIn()
returns the list of variable pairs that represent the
NotFreeIn relation of a Taclet
|
Modifier and Type | Method and Description |
---|---|
boolean |
Taclet.admissible(boolean interactive,
ImmutableList<RuleSet> p_ruleSets) |
boolean |
TacletApp.admissible(boolean interactive,
ImmutableList<RuleSet> ruleSets) |
protected boolean |
Taclet.admissibleAutomatic(ImmutableList<RuleSet> admissibleRuleSets) |
protected boolean |
Taclet.admissibleInteractive(ImmutableList<RuleSet> notAdmissibleRuleSets) |
protected static Term |
AbstractBlockContractRule.buildInfFlowPostAssumption(ProofObligationVars instVars,
ImmutableList<Term> localOuts,
ImmutableList<Term> localOutsAtPost,
Term baseHeap,
Term applPredTerm,
TermBuilder tb) |
protected static Term |
AbstractBlockContractRule.buildInfFlowPostAssumption(ProofObligationVars instVars,
ImmutableList<Term> localOuts,
ImmutableList<Term> localOutsAtPost,
Term baseHeap,
Term applPredTerm,
TermBuilder tb) |
protected static Term |
AbstractBlockContractRule.buildInfFlowPreAssumption(ProofObligationVars instVars,
ImmutableList<Term> localOuts,
ImmutableList<Term> localOutsAtPre,
Term baseHeap,
TermBuilder tb) |
protected static Term |
AbstractBlockContractRule.buildInfFlowPreAssumption(ProofObligationVars instVars,
ImmutableList<Term> localOuts,
ImmutableList<Term> localOutsAtPre,
Term baseHeap,
TermBuilder tb) |
protected static ImmutableList<Term> |
AbstractBlockContractRule.buildLocalOutsAtPost(ImmutableList<Term> varTerms,
Services services) |
protected static ImmutableList<Term> |
AbstractBlockContractRule.buildLocalOutsAtPre(ImmutableList<Term> varTerms,
Services services) |
protected ImmutableList<SchemaVariable> |
TacletSchemaVariableCollector.collectSVInProgram(JavaBlock jb,
ImmutableList<SchemaVariable> vars)
collects all SchemVariables that occur in the JavaBlock
|
static NoPosTacletApp |
NoPosTacletApp.createNoPosTacletApp(Taclet taclet,
SVInstantiations instantiations,
ImmutableList<IfFormulaInstantiation> ifInstantiations,
Services services) |
static PosTacletApp |
PosTacletApp.createPosTacletApp(FindTaclet taclet,
SVInstantiations instantiations,
ImmutableList<IfFormulaInstantiation> ifInstantiations,
PosInOccurrence pos,
Services services) |
protected static boolean |
TacletApp.ifInstsCorrectSize(Taclet p_taclet,
ImmutableList<IfFormulaInstantiation> p_list) |
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.
|
void |
IfFormulaInstantiationCache.put(boolean antec,
Semisequent s,
ImmutableList<IfFormulaInstantiation> value) |
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.
|
LoopInvariantBuiltInRuleApp |
LoopInvariantBuiltInRuleApp.setIfInsts(ImmutableList<PosInOccurrence> ifInsts) |
IBuiltInRuleApp |
IBuiltInRuleApp.setIfInsts(ImmutableList<PosInOccurrence> ifInsts) |
abstract IBuiltInRuleApp |
AbstractBuiltInRuleApp.setIfInsts(ImmutableList<PosInOccurrence> ifInsts) |
DefaultBuiltInRuleApp |
DefaultBuiltInRuleApp.setIfInsts(ImmutableList<PosInOccurrence> ifInsts) |
IBuiltInRuleApp |
LoopApplyHeadBuiltInRuleApp.setIfInsts(ImmutableList<PosInOccurrence> ifInsts) |
LoopContractExternalBuiltInRuleApp |
LoopContractExternalBuiltInRuleApp.setIfInsts(ImmutableList<PosInOccurrence> ifInstantiations) |
UseDependencyContractApp |
UseDependencyContractApp.setIfInsts(ImmutableList<PosInOccurrence> ifInsts) |
BlockContractInternalBuiltInRuleApp |
BlockContractInternalBuiltInRuleApp.setIfInsts(ImmutableList<PosInOccurrence> ifInstantiations) |
ContractRuleApp |
ContractRuleApp.setIfInsts(ImmutableList<PosInOccurrence> ifInsts) |
BlockContractExternalBuiltInRuleApp |
BlockContractExternalBuiltInRuleApp.setIfInsts(ImmutableList<PosInOccurrence> ifInstantiations) |
LoopContractInternalBuiltInRuleApp |
LoopContractInternalBuiltInRuleApp.setIfInsts(ImmutableList<PosInOccurrence> ifInstantiations) |
void |
AbstractBuiltInRuleApp.setMutable(ImmutableList<PosInOccurrence> ifInsts)
HACK: but strategies do not work otherwise in the moment; I need to have a closer look on what is going on there
This restores the behaviour as it was before my previous commit for the moment
|
Constructor and Description |
---|
AbstractAuxiliaryContractBuiltInRuleApp(BuiltInRule rule,
PosInOccurrence occurrence,
ImmutableList<PosInOccurrence> ifInstantiations) |
AbstractBlockContractBuiltInRuleApp(BuiltInRule rule,
PosInOccurrence occurrence,
ImmutableList<PosInOccurrence> ifInstantiations) |
AbstractBuiltInRuleApp(BuiltInRule rule,
PosInOccurrence pio,
ImmutableList<PosInOccurrence> ifInsts) |
AbstractContractRuleApp(BuiltInRule rule,
PosInOccurrence pio,
ImmutableList<PosInOccurrence> ifInsts,
Contract contract) |
AbstractLoopContractBuiltInRuleApp(BuiltInRule rule,
PosInOccurrence occurrence,
ImmutableList<PosInOccurrence> ifInstantiations) |
AdditionalHeapTerms(Term anonUpdate,
Term wellFormedAnon,
Term frameCondition,
Term reachableState,
ImmutableList<AbstractLoopInvariantRule.AnonUpdateData> anonUpdateData) |
AntecTaclet(Name name,
TacletApplPart applPart,
ImmutableList<TacletGoalTemplate> goalTemplates,
ImmutableList<RuleSet> heuristics,
TacletAttributes attrs,
Term find,
boolean ignoreTopLevelUpdates,
ImmutableMap<SchemaVariable,TacletPrefix> prefixMap,
ImmutableSet<Choice> choices,
ImmutableSet<TacletAnnotation> tacletAnnotations)
creates a Schematic Theory Specific Rule (Taclet) with the given
parameters.
|
AntecTaclet(Name name,
TacletApplPart applPart,
ImmutableList<TacletGoalTemplate> goalTemplates,
ImmutableList<RuleSet> heuristics,
TacletAttributes attrs,
Term find,
boolean ignoreTopLevelUpdates,
ImmutableMap<SchemaVariable,TacletPrefix> prefixMap,
ImmutableSet<Choice> choices,
ImmutableSet<TacletAnnotation> tacletAnnotations)
creates a Schematic Theory Specific Rule (Taclet) with the given
parameters.
|
BlockContractExternalBuiltInRuleApp(BuiltInRule rule,
PosInOccurrence occurrence,
ImmutableList<PosInOccurrence> ifInstantiations,
JavaStatement statement,
BlockContract contract,
java.util.List<LocationVariable> heaps) |
BlockContractInternalBuiltInRuleApp(BuiltInRule rule,
PosInOccurrence occurrence,
ImmutableList<PosInOccurrence> ifInstantiations,
JavaStatement statement,
BlockContract contract,
java.util.List<LocationVariable> heaps) |
DefaultBuiltInRuleApp(BuiltInRule builtInRule,
PosInOccurrence pio,
ImmutableList<PosInOccurrence> ifInsts) |
FindTaclet(Name name,
TacletApplPart applPart,
ImmutableList<TacletGoalTemplate> goalTemplates,
ImmutableList<RuleSet> ruleSets,
TacletAttributes attrs,
Term find,
ImmutableMap<SchemaVariable,TacletPrefix> prefixMap,
ImmutableSet<Choice> choices,
boolean surviveSymbExec,
ImmutableSet<TacletAnnotation> tacletAnnotations)
creates a FindTaclet
|
FindTaclet(Name name,
TacletApplPart applPart,
ImmutableList<TacletGoalTemplate> goalTemplates,
ImmutableList<RuleSet> ruleSets,
TacletAttributes attrs,
Term find,
ImmutableMap<SchemaVariable,TacletPrefix> prefixMap,
ImmutableSet<Choice> choices,
boolean surviveSymbExec,
ImmutableSet<TacletAnnotation> tacletAnnotations)
creates a FindTaclet
|
FindTaclet(Name name,
TacletApplPart applPart,
ImmutableList<TacletGoalTemplate> goalTemplates,
ImmutableList<RuleSet> ruleSets,
TacletAttributes attrs,
Term find,
ImmutableMap<SchemaVariable,TacletPrefix> prefixMap,
ImmutableSet<Choice> choices,
ImmutableSet<TacletAnnotation> tacletAnnotations)
creates a FindTaclet
|
FindTaclet(Name name,
TacletApplPart applPart,
ImmutableList<TacletGoalTemplate> goalTemplates,
ImmutableList<RuleSet> ruleSets,
TacletAttributes attrs,
Term find,
ImmutableMap<SchemaVariable,TacletPrefix> prefixMap,
ImmutableSet<Choice> choices,
ImmutableSet<TacletAnnotation> tacletAnnotations)
creates a FindTaclet
|
IfMatchResult(ImmutableList<IfFormulaInstantiation> p_candidates,
ImmutableList<MatchConditions> p_mcCandidates)
PRECONDITION: p_candidates.size () == p_mcCandidates.size ()
|
IfMatchResult(ImmutableList<IfFormulaInstantiation> p_candidates,
ImmutableList<MatchConditions> p_mcCandidates)
PRECONDITION: p_candidates.size () == p_mcCandidates.size ()
|
Instantiation(Term u,
Term progPost,
Modality mod,
Expression actualResult,
Term actualSelf,
KeYJavaType staticType,
MethodOrConstructorReference mr,
IProgramMethod pm,
ImmutableList<Term> actualParams,
boolean transaction)
Creates a new instantiation for the contract rule and the given variables.
|
LoopContractExternalBuiltInRuleApp(BuiltInRule rule,
PosInOccurrence occurrence,
ImmutableList<PosInOccurrence> ifInstantiations,
JavaStatement statement,
LoopContract contract,
java.util.List<LocationVariable> heaps) |
LoopContractInternalBuiltInRuleApp(BuiltInRule rule,
PosInOccurrence occurrence,
ImmutableList<PosInOccurrence> ifInstantiations,
JavaStatement statement,
LoopContract contract,
java.util.List<LocationVariable> heaps) |
LoopInvariantBuiltInRuleApp(BuiltInRule rule,
PosInOccurrence pio,
ImmutableList<PosInOccurrence> ifInsts,
LoopSpecification inv,
java.util.List<LocationVariable> heapContext,
TermServices services) |
LoopInvariantInformation(Goal goal,
Services services,
AbstractLoopInvariantRule.Instantiation inst,
LoopInvariantBuiltInRuleApp ruleApp,
ImmutableList<Goal> goals,
TermLabelState termLabelState,
Term invTerm,
Term variantPO,
Term reachableState,
Term anonUpdate,
Term wellFormedAnon,
Term uAnonInv,
Term frameCondition,
Term[] uBeforeLoopDefAnonVariant,
ImmutableList<AbstractLoopInvariantRule.AnonUpdateData> anonUpdateData)
Creates a new
AbstractLoopInvariantRule.LoopInvariantInformation object. |
LoopInvariantInformation(Goal goal,
Services services,
AbstractLoopInvariantRule.Instantiation inst,
LoopInvariantBuiltInRuleApp ruleApp,
ImmutableList<Goal> goals,
TermLabelState termLabelState,
Term invTerm,
Term variantPO,
Term reachableState,
Term anonUpdate,
Term wellFormedAnon,
Term uAnonInv,
Term frameCondition,
Term[] uBeforeLoopDefAnonVariant,
ImmutableList<AbstractLoopInvariantRule.AnonUpdateData> anonUpdateData)
Creates a new
AbstractLoopInvariantRule.LoopInvariantInformation object. |
NoFindTaclet(Name name,
TacletApplPart applPart,
ImmutableList<TacletGoalTemplate> goalTemplates,
ImmutableList<RuleSet> ruleSets,
TacletAttributes attrs,
ImmutableMap<SchemaVariable,TacletPrefix> prefixMap,
ImmutableSet<Choice> choices,
ImmutableSet<TacletAnnotation> tacletAnnotations)
creates a Schematic Theory Specific Rule (Taclet) with the given
parameters.
|
NoFindTaclet(Name name,
TacletApplPart applPart,
ImmutableList<TacletGoalTemplate> goalTemplates,
ImmutableList<RuleSet> ruleSets,
TacletAttributes attrs,
ImmutableMap<SchemaVariable,TacletPrefix> prefixMap,
ImmutableSet<Choice> choices,
ImmutableSet<TacletAnnotation> tacletAnnotations)
creates a Schematic Theory Specific Rule (Taclet) with the given
parameters.
|
RewriteTaclet(Name name,
TacletApplPart applPart,
ImmutableList<TacletGoalTemplate> goalTemplates,
ImmutableList<RuleSet> ruleSets,
TacletAttributes attrs,
Term find,
ImmutableMap<SchemaVariable,TacletPrefix> prefixMap,
int p_applicationRestriction,
ImmutableSet<Choice> choices,
boolean surviveSymbExec,
ImmutableSet<TacletAnnotation> tacletAnnotations) |
RewriteTaclet(Name name,
TacletApplPart applPart,
ImmutableList<TacletGoalTemplate> goalTemplates,
ImmutableList<RuleSet> ruleSets,
TacletAttributes attrs,
Term find,
ImmutableMap<SchemaVariable,TacletPrefix> prefixMap,
int p_applicationRestriction,
ImmutableSet<Choice> choices,
boolean surviveSymbExec,
ImmutableSet<TacletAnnotation> tacletAnnotations) |
RewriteTaclet(Name name,
TacletApplPart applPart,
ImmutableList<TacletGoalTemplate> goalTemplates,
ImmutableList<RuleSet> ruleSets,
TacletAttributes attrs,
Term find,
ImmutableMap<SchemaVariable,TacletPrefix> prefixMap,
int p_applicationRestriction,
ImmutableSet<Choice> choices,
ImmutableSet<TacletAnnotation> tacletAnnotations)
creates a Schematic Theory Specific Rule (Taclet) with the given
parameters that represents a rewrite rule.
|
RewriteTaclet(Name name,
TacletApplPart applPart,
ImmutableList<TacletGoalTemplate> goalTemplates,
ImmutableList<RuleSet> ruleSets,
TacletAttributes attrs,
Term find,
ImmutableMap<SchemaVariable,TacletPrefix> prefixMap,
int p_applicationRestriction,
ImmutableSet<Choice> choices,
ImmutableSet<TacletAnnotation> tacletAnnotations)
creates a Schematic Theory Specific Rule (Taclet) with the given
parameters that represents a rewrite rule.
|
SuccTaclet(Name name,
TacletApplPart applPart,
ImmutableList<TacletGoalTemplate> goalTemplates,
ImmutableList<RuleSet> heuristics,
TacletAttributes attrs,
Term find,
boolean ignoreTopLevelUpdates,
ImmutableMap<SchemaVariable,TacletPrefix> prefixMap,
ImmutableSet<Choice> choices,
ImmutableSet<TacletAnnotation> tacletAnnotations)
creates a Schematic Theory Specific Rule (Taclet) with the given
parameters that works on the succedent.
|
SuccTaclet(Name name,
TacletApplPart applPart,
ImmutableList<TacletGoalTemplate> goalTemplates,
ImmutableList<RuleSet> heuristics,
TacletAttributes attrs,
Term find,
boolean ignoreTopLevelUpdates,
ImmutableMap<SchemaVariable,TacletPrefix> prefixMap,
ImmutableSet<Choice> choices,
ImmutableSet<TacletAnnotation> tacletAnnotations)
creates a Schematic Theory Specific Rule (Taclet) with the given
parameters that works on the succedent.
|
Taclet(Name name,
TacletApplPart applPart,
ImmutableList<TacletGoalTemplate> goalTemplates,
ImmutableList<RuleSet> ruleSets,
TacletAttributes attrs,
ImmutableMap<SchemaVariable,TacletPrefix> prefixMap,
ImmutableSet<Choice> choices,
boolean surviveSmbExec,
ImmutableSet<TacletAnnotation> tacletAnnotations)
creates a Taclet (originally known as Schematic Theory Specific Rules)
|
Taclet(Name name,
TacletApplPart applPart,
ImmutableList<TacletGoalTemplate> goalTemplates,
ImmutableList<RuleSet> ruleSets,
TacletAttributes attrs,
ImmutableMap<SchemaVariable,TacletPrefix> prefixMap,
ImmutableSet<Choice> choices,
boolean surviveSmbExec,
ImmutableSet<TacletAnnotation> tacletAnnotations)
creates a Taclet (originally known as Schematic Theory Specific Rules)
|
Taclet(Name name,
TacletApplPart applPart,
ImmutableList<TacletGoalTemplate> goalTemplates,
ImmutableList<RuleSet> ruleSets,
TacletAttributes attrs,
ImmutableMap<SchemaVariable,TacletPrefix> prefixMap,
ImmutableSet<Choice> choices,
ImmutableSet<TacletAnnotation> tacletAnnotations)
creates a Schematic Theory Specific Rule (Taclet) with the given
parameters.
|
Taclet(Name name,
TacletApplPart applPart,
ImmutableList<TacletGoalTemplate> goalTemplates,
ImmutableList<RuleSet> ruleSets,
TacletAttributes attrs,
ImmutableMap<SchemaVariable,TacletPrefix> prefixMap,
ImmutableSet<Choice> choices,
ImmutableSet<TacletAnnotation> tacletAnnotations)
creates a Schematic Theory Specific Rule (Taclet) with the given
parameters.
|
TacletApplPart(Sequent ifseq,
ImmutableList<NewVarcond> varsNew,
ImmutableList<NotFreeIn> varsNotFreeIn,
ImmutableList<NewDependingOn> varsNewDependingOn,
ImmutableList<VariableCondition> variableConditions)
constructs a new TacletApplPart object with the given Sequent,
a list of variables that are new, a list of variable pairs that
represent the NotFreeIn relation and a list of additional
generic variable conditions.
|
TacletApplPart(Sequent ifseq,
ImmutableList<NewVarcond> varsNew,
ImmutableList<NotFreeIn> varsNotFreeIn,
ImmutableList<NewDependingOn> varsNewDependingOn,
ImmutableList<VariableCondition> variableConditions)
constructs a new TacletApplPart object with the given Sequent,
a list of variables that are new, a list of variable pairs that
represent the NotFreeIn relation and a list of additional
generic variable conditions.
|
TacletApplPart(Sequent ifseq,
ImmutableList<NewVarcond> varsNew,
ImmutableList<NotFreeIn> varsNotFreeIn,
ImmutableList<NewDependingOn> varsNewDependingOn,
ImmutableList<VariableCondition> variableConditions)
constructs a new TacletApplPart object with the given Sequent,
a list of variables that are new, a list of variable pairs that
represent the NotFreeIn relation and a list of additional
generic variable conditions.
|
TacletApplPart(Sequent ifseq,
ImmutableList<NewVarcond> varsNew,
ImmutableList<NotFreeIn> varsNotFreeIn,
ImmutableList<NewDependingOn> varsNewDependingOn,
ImmutableList<VariableCondition> variableConditions)
constructs a new TacletApplPart object with the given Sequent,
a list of variables that are new, a list of variable pairs that
represent the NotFreeIn relation and a list of additional
generic variable conditions.
|
Trigger(SchemaVariable triggerVar,
Term trigger,
ImmutableList<Term> avoidConditions) |
UseDependencyContractApp(BuiltInRule rule,
PosInOccurrence pio,
ImmutableList<PosInOccurrence> ifInsts,
Contract contract,
PosInOccurrence step) |
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 |
---|---|
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 ImmutableList<SequentChangeInfo> |
TacletExecutor.checkIfGoals(Goal p_goal,
ImmutableList<IfFormulaInstantiation> p_list,
MatchConditions p_matchCond,
int p_numberOfNewGoals)
Search for formulas within p_list that have to be proved by an
explicit assumes-goal, i.e.
|
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
|
Modifier and Type | Method and Description |
---|---|
protected void |
TacletExecutor.applyAddrule(ImmutableList<Taclet> rules,
Goal goal,
Services services,
MatchConditions matchCond)
adds the given rules (i.e.
|
protected ImmutableList<SequentChangeInfo> |
TacletExecutor.checkIfGoals(Goal p_goal,
ImmutableList<IfFormulaInstantiation> p_list,
MatchConditions p_matchCond,
int p_numberOfNewGoals)
Search for formulas within p_list that have to be proved by an
explicit assumes-goal, i.e.
|
Modifier and Type | Method and Description |
---|---|
ImmutableList<GenericSortCondition> |
SVInstantiations.getGenericSortConditions() |
ImmutableList<SVInstantiations.UpdateLabelPair> |
SVInstantiations.getUpdateContext()
returns the update context
|
ImmutableList<GenericSortCondition> |
GenericSortInstantiations.toConditions()
Create a list of conditions establishing the instantiations
stored by this object (not saying anything about further
generic sorts)
|
Modifier and Type | Method and Description |
---|---|
SVInstantiations |
SVInstantiations.addUpdateList(ImmutableList<SVInstantiations.UpdateLabelPair> updates) |
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(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.
|
void |
GenericSortException.setConditions(ImmutableList<GenericSortCondition> pConditions) |
Constructor and Description |
---|
GenericSortException(java.lang.String description,
ImmutableList<GenericSortCondition> pConditions) |
Modifier and Type | Method and Description |
---|---|
ImmutableList<Name> |
OriginTermLabelRefactoring.getSupportedRuleNames() |
ImmutableList<Name> |
RuleSpecificTask.getSupportedRuleNames()
Returns the supported rule
Name s or null or an empty
list if all rules are supported. |
ImmutableList<Name> |
FormulaTermLabelUpdate.getSupportedRuleNames()
Returns the supported rule
Name s or null or an empty
list if all rules are supported. |
ImmutableList<Name> |
LoopBodyTermLabelUpdate.getSupportedRuleNames()
Returns the supported rule
Name s or null or an empty
list if all rules are supported. |
ImmutableList<Name> |
FormulaTermLabelRefactoring.getSupportedRuleNames()
Returns the supported rule
Name s or null or an empty
list if all rules are supported. |
ImmutableList<Name> |
BlockContractValidityTermLabelUpdate.getSupportedRuleNames()
Returns the supported rule
Name s or null or an empty
list if all rules are supported. |
ImmutableList<Name> |
SymbolicExecutionTermLabelUpdate.getSupportedRuleNames()
Returns the supported rule
Name s or null or an empty
list if all rules are supported. |
ImmutableList<Name> |
RemoveInCheckBranchesTermLabelRefactoring.getSupportedRuleNames()
Returns the supported rule
Name s or null or an empty
list if all rules are supported. |
ImmutableList<Name> |
LoopInvariantNormalBehaviorTermLabelUpdate.getSupportedRuleNames()
Returns the supported rule
Name s or null or an empty
list if all rules are supported. |
Modifier and Type | Method and Description |
---|---|
IfMatchResult |
LegacyTacletMatcher.matchIf(ImmutableList<IfFormulaInstantiation> p_toMatch,
Term p_template,
MatchConditions p_matchCond,
Services p_services)
(non-Javadoc)
|
Modifier and Type | Method and Description |
---|---|
IfMatchResult |
VMTacletMatcher.matchIf(ImmutableList<IfFormulaInstantiation> p_toMatch,
Term p_template,
MatchConditions p_matchCond,
Services p_services)
(non-Javadoc)
|
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) |
static ImmutableList<MergePartner> |
MergeRule.findPotentialMergePartners(Goal goal,
PosInOccurrence pio)
Finds all suitable merge partners
|
ImmutableList<MergePartner> |
MergeRuleBuiltInRuleApp.getMergePartners() |
ImmutableList<SymbolicExecutionState> |
MergeRuleBuiltInRuleApp.getMergePartnerStates() |
static ImmutableList<MergeProcedure> |
MergeProcedure.getMergeProcedures()
Returns all registered merge procedures.
|
Modifier and Type | Method and Description |
---|---|
IBuiltInRuleApp |
CloseAfterMergeRuleBuiltInRuleApp.setIfInsts(ImmutableList<PosInOccurrence> ifInsts) |
IBuiltInRuleApp |
MergeRuleBuiltInRuleApp.setIfInsts(ImmutableList<PosInOccurrence> ifInsts) |
void |
MergeRuleBuiltInRuleApp.setMergePartners(ImmutableList<MergePartner> mergePartners) |
Modifier and Type | Method and Description |
---|---|
ImmutableList<SchemaVariable> |
WhileInvariantTransformer.neededInstantiations(ProgramElement originalLoop,
SVInstantiations svInst)
returns the schemavariables that are needed to transform the given loop.
|
ImmutableList<SchemaVariable> |
UnwindLoop.neededInstantiations(SVInstantiations svInst)
return a list of the SV that are relevant to this UnwindLoop
|
ImmutableList<SchemaVariable> |
ForToWhile.neededInstantiations(SVInstantiations svInst)
return a list of the SV that are relevant to this UnwindLoop
|
ImmutableList<SchemaVariable> |
ProgramTransformer.neededInstantiations(SVInstantiations svInst)
get a list of schema variables that are needed by this entity when
working given a SV instantiation set.
|
ImmutableList<SchemaVariable> |
ProgramTransformer.needs()
get a list of schema variables that are needed by this entity when
working given a SV instantiation set.
|
Modifier and Type | Method and Description |
---|---|
protected Statement |
MethodCall.makeIfCascade(ImmutableList<KeYJavaType> imps,
Services services)
TODO
|
Modifier and Type | Method and Description |
---|---|
ImmutableList<Monomial> |
Polynomial.getParts() |
ImmutableList<Term> |
Monomial.getParts() |
Modifier and Type | Field and Description |
---|---|
protected ImmutableList<TacletGoalTemplate> |
TacletBuilder.goals |
protected ImmutableList<RuleSet> |
TacletBuilder.ruleSets |
protected ImmutableList<VariableCondition> |
TacletBuilder.variableConditions
List of additional generic conditions on the instantiations of
schema variables.
|
protected ImmutableList<NewVarcond> |
TacletBuilder.varsNew |
protected ImmutableList<NewDependingOn> |
TacletBuilder.varsNewDependingOn |
protected ImmutableList<NotFreeIn> |
TacletBuilder.varsNotFreeIn |
Modifier and Type | Method and Description |
---|---|
ImmutableList<TacletGoalTemplate> |
TacletBuilder.goalTemplates() |
ImmutableList<Taclet> |
TacletGoalTemplate.rules()
the goal of a Taclet may introduce new rules.
|
Modifier and Type | Method and Description |
---|---|
void |
TacletBuilder.addVarsNew(ImmutableList<NewVarcond> list)
adds a list of new variables to the variable conditions of
the Taclet: v is new for all v's in the given list
|
void |
TacletBuilder.addVarsNotFreeIn(ImmutableList<NotFreeIn> list)
adds a list of NotFreeIn variable pairs to the variable
conditions of
the Taclet: v0 is not free in v1 for all entries (v0,v1) in the given list.
|
Taclet |
TacletGenerator.generateAxiomTaclet(Name tacletName,
Term originalAxiom,
ImmutableList<ProgramVariable> programVars,
KeYJavaType kjt,
RuleSet ruleSet,
TermServices services)
Returns a no-find taclet to the passed axiom.
|
ImmutableSet<Taclet> |
TacletGenerator.generateContractAxiomTaclets(Name name,
Term originalPre,
Term originalPost,
Term originalMby,
KeYJavaType kjt,
IObserverFunction target,
java.util.List<? extends ProgramVariable> heaps,
ProgramVariable originalSelfVar,
ProgramVariable originalResultVar,
java.util.Map<LocationVariable,ProgramVariable> atPreVars,
ImmutableList<ProgramVariable> originalParamVars,
ImmutableSet<Pair<Sort,IObserverFunction>> toLimit,
boolean satisfiabilityGuard,
TermServices services) |
ImmutableSet<Taclet> |
TacletGenerator.generateFunctionalRepresentsTaclets(Name name,
Term originalPreTerm,
Term originalRepresentsTerm,
KeYJavaType kjt,
IObserverFunction target,
java.util.List<? extends ProgramVariable> heaps,
ProgramVariable self,
ImmutableList<ProgramVariable> paramVars,
java.util.Map<LocationVariable,ProgramVariable> atPreVars,
ImmutableSet<Pair<Sort,IObserverFunction>> toLimit,
boolean satisfiability,
Services services) |
Taclet |
TacletGenerator.generateRelationalRepresentsTaclet(Name tacletName,
Term originalAxiom,
KeYJavaType kjt,
IObserverFunction target,
java.util.List<? extends ProgramVariable> heaps,
ProgramVariable self,
ImmutableList<ProgramVariable> paramVars,
java.util.Map<LocationVariable,ProgramVariable> atPreVars,
boolean satisfiabilityGuard,
TermServices services) |
Taclet |
TacletGenerator.generateRewriteTaclet(Name tacletName,
Term originalFind,
Term originalAxiom,
ImmutableList<ProgramVariable> programVars,
RuleSet ruleSet,
TermServices services) |
void |
TacletBuilder.setRuleSets(ImmutableList<RuleSet> rs) |
void |
TacletBuilder.setTacletGoalTemplates(ImmutableList<TacletGoalTemplate> g) |
Constructor and Description |
---|
AntecSuccTacletGoalTemplate(Sequent addedSeq,
ImmutableList<Taclet> addedRules,
Sequent replacewith) |
AntecSuccTacletGoalTemplate(Sequent addedSeq,
ImmutableList<Taclet> addedRules,
Sequent replacewith,
ImmutableSet<SchemaVariable> pvs)
creates new Goaldescription
|
RewriteTacletGoalTemplate(Sequent addedSeq,
ImmutableList<Taclet> addedRules,
Term replacewith) |
RewriteTacletGoalTemplate(Sequent addedSeq,
ImmutableList<Taclet> addedRules,
Term replacewith,
ImmutableSet<SchemaVariable> pvs)
creates new Goaldescription
|
TacletGoalTemplate(Sequent addedSeq,
ImmutableList<Taclet> addedRules)
creates new Goaldescription
same effect as
new TacletGoalTemplate(addedSeq,
addedRules,
SetAsListOf. |
TacletGoalTemplate(Sequent addedSeq,
ImmutableList<Taclet> addedRules,
ImmutableSet<SchemaVariable> addedProgVars)
creates new Goaldescription
|
Modifier and Type | Method and Description |
---|---|
ImmutableList<Goal> |
RuleAppSMT.SMTRule.apply(Goal goal,
Services services,
RuleApp ruleApp) |
Modifier and Type | Method and Description |
---|---|
RuleAppSMT |
RuleAppSMT.setIfInsts(ImmutableList<PosInOccurrence> ifInsts) |
Modifier and Type | Field and Description |
---|---|
protected ImmutableList<InfFlowSpec> |
AbstractAuxiliaryContractImpl.infFlowSpecs |
ImmutableList<ProgramVariable> |
Contract.OriginalVariables.params |
ImmutableList<Term> |
WellDefinednessCheck.POTerms.rest |
Modifier and Type | Method and Description |
---|---|
ImmutableList<InfFlowSpec> |
AbstractAuxiliaryContractImpl.getInfFlowSpecs() |
ImmutableList<InfFlowSpec> |
InformationFlowContractImpl.getInfFlowSpecs() |
ImmutableList<InfFlowSpec> |
InformationFlowContract.getInfFlowSpecs()
Returns the set of views.
|
ImmutableList<InfFlowSpec> |
AuxiliaryContract.getInfFlowSpecs() |
ImmutableList<InfFlowSpec> |
LoopSpecification.getInfFlowSpecs(LocationVariable heap)
Returns the information flow specification clause.
|
ImmutableList<InfFlowSpec> |
LoopSpecImpl.getInfFlowSpecs(LocationVariable heap) |
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) |
ImmutableList<Term> |
FunctionalOperationContractImpl.getParams() |
ImmutableList<Term> |
InformationFlowContractImpl.getParams() |
ImmutableList<Term> |
InformationFlowContract.getParams()
Get the parameter-variables which is used in this contract.
|
ImmutableList<Term> |
FunctionalOperationContract.getParams() |
ImmutableList<PositionedString> |
SpecExtractor.getWarnings()
Returns all warnings generated so far in the translation process.
|
Modifier and Type | Method and Description |
---|---|
java.util.Map<LocationVariable,ImmutableList<InfFlowSpec>> |
LoopSpecification.getInternalInfFlowSpec() |
java.util.Map<LocationVariable,ImmutableList<InfFlowSpec>> |
LoopSpecImpl.getInternalInfFlowSpec() |
Modifier and Type | Method and Description |
---|---|
Contract.OriginalVariables |
Contract.OriginalVariables.add(ImmutableList<ProgramVariable> newParams)
Adds a list of parameters and deletes the prior ones (if any).
|
FunctionalOperationContract |
ContractFactory.addPost(FunctionalOperationContract old,
Term addedPost,
ProgramVariable selfVar,
ProgramVariable resultVar,
ProgramVariable excVar,
ImmutableList<ProgramVariable> paramVars,
java.util.Map<LocationVariable,LocationVariable> atPreVars)
Returns another contract like this one, except that the passed term has been added as a
postcondition (regardless of termination case).
|
FunctionalOperationContract |
ContractFactory.addPre(FunctionalOperationContract old,
Term addedPre,
ProgramVariable selfVar,
ImmutableList<ProgramVariable> paramVars,
java.util.Map<LocationVariable,LocationVariable> atPreVars)
Returns another contract like this one, except that the passed term has been added as a
precondition.
|
protected abstract T |
AbstractAuxiliaryContractImpl.Creator.build(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) |
protected BlockContract |
BlockContractImpl.Creator.build(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) |
protected LoopContract |
LoopContractImpl.Creator.build(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) |
LoopSpecification |
LoopSpecification.create(LoopStatement loop,
IProgramMethod pm,
KeYJavaType kjt,
java.util.Map<LocationVariable,Term> invariants,
java.util.Map<LocationVariable,Term> freeInvariants,
java.util.Map<LocationVariable,Term> modifies,
java.util.Map<LocationVariable,ImmutableList<InfFlowSpec>> infFlowSpecs,
Term variant,
Term selfTerm,
ImmutableList<Term> localIns,
ImmutableList<Term> localOuts,
java.util.Map<LocationVariable,Term> atPres)
Create and return a new loop specification element from the existing one
where the arguments given are replaced.
|
LoopSpecification |
LoopSpecification.create(LoopStatement loop,
IProgramMethod pm,
KeYJavaType kjt,
java.util.Map<LocationVariable,Term> invariants,
java.util.Map<LocationVariable,Term> freeInvariants,
java.util.Map<LocationVariable,Term> modifies,
java.util.Map<LocationVariable,ImmutableList<InfFlowSpec>> infFlowSpecs,
Term variant,
Term selfTerm,
ImmutableList<Term> localIns,
ImmutableList<Term> localOuts,
java.util.Map<LocationVariable,Term> atPres)
Create and return a new loop specification element from the existing one
where the arguments given are replaced.
|
LoopSpecification |
LoopSpecImpl.create(LoopStatement loop,
IProgramMethod pm,
KeYJavaType kjt,
java.util.Map<LocationVariable,Term> invariants,
java.util.Map<LocationVariable,Term> freeInvariants,
java.util.Map<LocationVariable,Term> modifies,
java.util.Map<LocationVariable,ImmutableList<InfFlowSpec>> infFlowSpecs,
Term variant,
Term selfTerm,
ImmutableList<Term> localIns,
ImmutableList<Term> localOuts,
java.util.Map<LocationVariable,Term> atPres) |
LoopSpecification |
LoopSpecImpl.create(LoopStatement loop,
IProgramMethod pm,
KeYJavaType kjt,
java.util.Map<LocationVariable,Term> invariants,
java.util.Map<LocationVariable,Term> freeInvariants,
java.util.Map<LocationVariable,Term> modifies,
java.util.Map<LocationVariable,ImmutableList<InfFlowSpec>> infFlowSpecs,
Term variant,
Term selfTerm,
ImmutableList<Term> localIns,
ImmutableList<Term> localOuts,
java.util.Map<LocationVariable,Term> atPres) |
LoopSpecification |
LoopSpecification.create(LoopStatement loop,
java.util.Map<LocationVariable,Term> invariants,
java.util.Map<LocationVariable,Term> freeInvariants,
java.util.Map<LocationVariable,Term> modifies,
java.util.Map<LocationVariable,ImmutableList<InfFlowSpec>> infFlowSpecs,
Term variant,
Term selfTerm,
ImmutableList<Term> localIns,
ImmutableList<Term> localOuts,
java.util.Map<LocationVariable,Term> atPres)
Create and return a new loop specification element from the existing one
where the arguments given are replaced.
|
LoopSpecification |
LoopSpecification.create(LoopStatement loop,
java.util.Map<LocationVariable,Term> invariants,
java.util.Map<LocationVariable,Term> freeInvariants,
java.util.Map<LocationVariable,Term> modifies,
java.util.Map<LocationVariable,ImmutableList<InfFlowSpec>> infFlowSpecs,
Term variant,
Term selfTerm,
ImmutableList<Term> localIns,
ImmutableList<Term> localOuts,
java.util.Map<LocationVariable,Term> atPres)
Create and return a new loop specification element from the existing one
where the arguments given are replaced.
|
LoopSpecification |
LoopSpecImpl.create(LoopStatement loop,
java.util.Map<LocationVariable,Term> invariants,
java.util.Map<LocationVariable,Term> freeInvariants,
java.util.Map<LocationVariable,Term> modifies,
java.util.Map<LocationVariable,ImmutableList<InfFlowSpec>> infFlowSpecs,
Term variant,
Term selfTerm,
ImmutableList<Term> localIns,
ImmutableList<Term> localOuts,
java.util.Map<LocationVariable,Term> atPres) |
LoopSpecification |
LoopSpecImpl.create(LoopStatement loop,
java.util.Map<LocationVariable,Term> invariants,
java.util.Map<LocationVariable,Term> freeInvariants,
java.util.Map<LocationVariable,Term> modifies,
java.util.Map<LocationVariable,ImmutableList<InfFlowSpec>> infFlowSpecs,
Term variant,
Term selfTerm,
ImmutableList<Term> localIns,
ImmutableList<Term> localOuts,
java.util.Map<LocationVariable,Term> atPres) |
InformationFlowContract |
ContractFactory.createInformationFlowContract(KeYJavaType forClass,
IProgramMethod pm,
KeYJavaType specifiedIn,
Modality modality,
Term requires,
Term requiresFree,
Term measuredBy,
Term modifies,
boolean hasMod,
ProgramVariableCollection progVars,
Term accessible,
ImmutableList<InfFlowSpec> infFlowSpecs,
boolean toBeSaved) |
DependencyContract |
ContractFactory.dep(KeYJavaType containerType,
IObserverFunction pm,
KeYJavaType specifiedIn,
java.util.Map<LocationVariable,Term> requires,
Term measuredBy,
java.util.Map<ProgramVariable,Term> accessibles,
ProgramVariable selfVar,
ImmutableList<ProgramVariable> paramVars,
java.util.Map<LocationVariable,? extends ProgramVariable> atPreVars,
Term globalDefs) |
DependencyContract |
ContractFactory.dep(java.lang.String string,
KeYJavaType containerType,
IObserverFunction pm,
KeYJavaType specifiedIn,
java.util.Map<LocationVariable,Term> requires,
Term measuredBy,
java.util.Map<ProgramVariable,Term> accessibles,
ProgramVariable selfVar,
ImmutableList<ProgramVariable> paramVars,
java.util.Map<LocationVariable,? extends ProgramVariable> atPreVars,
Term globalDefs) |
ImmutableSet<MergeContract> |
SpecExtractor.extractMergeContracts(IProgramMethod method,
MergePointStatement mps,
ImmutableList<ProgramVariable> methodParams)
Returns the
MergeContract s for the given
MergePointStatement . |
FunctionalOperationContract |
ContractFactory.func(java.lang.String baseName,
KeYJavaType kjt,
IProgramMethod pm,
Modality modality,
java.util.Map<LocationVariable,Term> pres,
java.util.Map<LocationVariable,Term> freePres,
Term mby,
java.util.Map<LocationVariable,Term> posts,
java.util.Map<LocationVariable,Term> freePosts,
java.util.Map<LocationVariable,Term> axioms,
java.util.Map<LocationVariable,Term> mods,
java.util.Map<ProgramVariable,Term> accs,
java.util.Map<LocationVariable,java.lang.Boolean> hasMod,
ProgramVariable selfVar,
ImmutableList<ProgramVariable> paramVars,
ProgramVariable resultVar,
ProgramVariable excVar,
java.util.Map<LocationVariable,LocationVariable> atPreVars,
boolean toBeSaved)
Creates a new functional operation contract.
|
Term |
FunctionalOperationContractImpl.getAnyMod(Term mod,
ProgramVariable selfVar,
ImmutableList<ProgramVariable> paramVars,
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 |
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 |
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 |
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) |
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 |
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 |
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 |
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 |
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.
|
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.
|
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) |
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) |
LoopContract |
LoopContract.update(LoopStatement newLoop,
java.util.Map<LocationVariable,Term> newPreconditions,
java.util.Map<LocationVariable,Term> newFreePreconditions,
java.util.Map<LocationVariable,Term> newPostconditions,
java.util.Map<LocationVariable,Term> newFreePostconditions,
java.util.Map<LocationVariable,Term> newModifiesClauses,
ImmutableList<InfFlowSpec> newinfFlowSpecs,
AuxiliaryContract.Variables newVariables,
Term newMeasuredBy,
Term newDecreases) |
LoopContract |
LoopContractImpl.update(LoopStatement newLoop,
java.util.Map<LocationVariable,Term> newPreconditions,
java.util.Map<LocationVariable,Term> newFreePreconditions,
java.util.Map<LocationVariable,Term> newPostconditions,
java.util.Map<LocationVariable,Term> newFreePostconditions,
java.util.Map<LocationVariable,Term> newModifiesClauses,
ImmutableList<InfFlowSpec> newinfFlowSpecs,
AuxiliaryContract.Variables newVariables,
Term newMeasuredBy,
Term newDecreases) |
BlockContract |
BlockContractImpl.update(StatementBlock newBlock,
java.util.Map<LocationVariable,Term> newPreconditions,
java.util.Map<LocationVariable,Term> newFreePreconditions,
java.util.Map<LocationVariable,Term> newPostconditions,
java.util.Map<LocationVariable,Term> newFreePostconditions,
java.util.Map<LocationVariable,Term> newModifiesClauses,
ImmutableList<InfFlowSpec> newinfFlowSpecs,
AuxiliaryContract.Variables newVariables,
Term newMeasuredBy) |
BlockContract |
BlockContract.update(StatementBlock newBlock,
java.util.Map<LocationVariable,Term> newPreconditions,
java.util.Map<LocationVariable,Term> newFreePreconditions,
java.util.Map<LocationVariable,Term> newPostconditions,
java.util.Map<LocationVariable,Term> newFreePostconditions,
java.util.Map<LocationVariable,Term> newModifiesClauses,
ImmutableList<InfFlowSpec> newInfFlowSpecs,
AuxiliaryContract.Variables newVariables,
Term newMeasuredBy) |
LoopContract |
LoopContract.update(StatementBlock newBlock,
java.util.Map<LocationVariable,Term> newPreconditions,
java.util.Map<LocationVariable,Term> newFreePreconditions,
java.util.Map<LocationVariable,Term> newPostconditions,
java.util.Map<LocationVariable,Term> newFreePostconditions,
java.util.Map<LocationVariable,Term> newModifiesClauses,
ImmutableList<InfFlowSpec> newinfFlowSpecs,
AuxiliaryContract.Variables newVariables,
Term newMeasuredBy,
Term newDecreases) |
LoopContract |
LoopContractImpl.update(StatementBlock newBlock,
java.util.Map<LocationVariable,Term> newPreconditions,
java.util.Map<LocationVariable,Term> newFreePreconditions,
java.util.Map<LocationVariable,Term> newPostconditions,
java.util.Map<LocationVariable,Term> newFreePostconditions,
java.util.Map<LocationVariable,Term> newModifiesClauses,
ImmutableList<InfFlowSpec> newinfFlowSpecs,
AuxiliaryContract.Variables newVariables,
Term newMeasuredBy,
Term newDecreases) |
Modifier and Type | Method and Description |
---|---|
LoopSpecification |
LoopSpecification.configurate(java.util.Map<LocationVariable,Term> invariants,
java.util.Map<LocationVariable,Term> freeInvariants,
java.util.Map<LocationVariable,Term> modifies,
java.util.Map<LocationVariable,ImmutableList<InfFlowSpec>> infFlowSpecs,
Term variant)
Configure the existing loop specification element with new elements,
i.e., loop invariant clauses, a loop variant, modifies clauses,
information flow specification elements, and a loop variant,
possibly together with (if any) "free" loop invariant clauses.
|
LoopSpecification |
LoopSpecImpl.configurate(java.util.Map<LocationVariable,Term> invariants,
java.util.Map<LocationVariable,Term> freeInvariants,
java.util.Map<LocationVariable,Term> modifies,
java.util.Map<LocationVariable,ImmutableList<InfFlowSpec>> infFlowSpecs,
Term variant) |
LoopSpecification |
LoopSpecification.create(LoopStatement loop,
IProgramMethod pm,
KeYJavaType kjt,
java.util.Map<LocationVariable,Term> invariants,
java.util.Map<LocationVariable,Term> freeInvariants,
java.util.Map<LocationVariable,Term> modifies,
java.util.Map<LocationVariable,ImmutableList<InfFlowSpec>> infFlowSpecs,
Term variant,
Term selfTerm,
ImmutableList<Term> localIns,
ImmutableList<Term> localOuts,
java.util.Map<LocationVariable,Term> atPres)
Create and return a new loop specification element from the existing one
where the arguments given are replaced.
|
LoopSpecification |
LoopSpecImpl.create(LoopStatement loop,
IProgramMethod pm,
KeYJavaType kjt,
java.util.Map<LocationVariable,Term> invariants,
java.util.Map<LocationVariable,Term> freeInvariants,
java.util.Map<LocationVariable,Term> modifies,
java.util.Map<LocationVariable,ImmutableList<InfFlowSpec>> infFlowSpecs,
Term variant,
Term selfTerm,
ImmutableList<Term> localIns,
ImmutableList<Term> localOuts,
java.util.Map<LocationVariable,Term> atPres) |
LoopSpecification |
LoopSpecification.create(LoopStatement loop,
java.util.Map<LocationVariable,Term> invariants,
java.util.Map<LocationVariable,Term> freeInvariants,
java.util.Map<LocationVariable,Term> modifies,
java.util.Map<LocationVariable,ImmutableList<InfFlowSpec>> infFlowSpecs,
Term variant,
Term selfTerm,
ImmutableList<Term> localIns,
ImmutableList<Term> localOuts,
java.util.Map<LocationVariable,Term> atPres)
Create and return a new loop specification element from the existing one
where the arguments given are replaced.
|
LoopSpecification |
LoopSpecImpl.create(LoopStatement loop,
java.util.Map<LocationVariable,Term> invariants,
java.util.Map<LocationVariable,Term> freeInvariants,
java.util.Map<LocationVariable,Term> modifies,
java.util.Map<LocationVariable,ImmutableList<InfFlowSpec>> infFlowSpecs,
Term variant,
Term selfTerm,
ImmutableList<Term> localIns,
ImmutableList<Term> localOuts,
java.util.Map<LocationVariable,Term> atPres) |
Constructor and Description |
---|
AbstractAuxiliaryContractImpl(java.lang.String baseName,
StatementBlock block,
java.util.List<Label> labels,
IProgramMethod method,
Modality modality,
java.util.Map<LocationVariable,Term> preconditions,
java.util.Map<LocationVariable,Term> freePreconditions,
Term measuredBy,
java.util.Map<LocationVariable,Term> postconditions,
java.util.Map<LocationVariable,Term> freePostconditions,
java.util.Map<LocationVariable,Term> modifiesClauses,
ImmutableList<InfFlowSpec> infFlowSpecs,
AuxiliaryContract.Variables variables,
boolean transactionApplicable,
java.util.Map<LocationVariable,java.lang.Boolean> hasMod,
ImmutableSet<FunctionalAuxiliaryContract<?>> functionalContracts) |
BlockContractImpl(java.lang.String baseName,
StatementBlock block,
java.util.List<Label> labels,
IProgramMethod method,
Modality modality,
java.util.Map<LocationVariable,Term> preconditions,
java.util.Map<LocationVariable,Term> freePreconditions,
Term measuredBy,
java.util.Map<LocationVariable,Term> postconditions,
java.util.Map<LocationVariable,Term> freePostconditions,
java.util.Map<LocationVariable,Term> modifiesClauses,
ImmutableList<InfFlowSpec> infFlowSpecs,
AuxiliaryContract.Variables variables,
boolean transactionApplicable,
java.util.Map<LocationVariable,java.lang.Boolean> hasMod,
ImmutableSet<FunctionalAuxiliaryContract<?>> functionalContracts) |
ContractAxiom(java.lang.String name,
IObserverFunction target,
KeYJavaType kjt,
VisibilityModifier visibility,
Term pre,
Term post,
Term mby,
java.util.Map<LocationVariable,ProgramVariable> atPreVars,
ProgramVariable selfVar,
ProgramVariable resultVar,
ImmutableList<ProgramVariable> paramVars) |
ContractAxiom(java.lang.String name,
java.lang.String displayName,
IObserverFunction target,
KeYJavaType kjt,
VisibilityModifier visibility,
Term originalPre,
Term originalPost,
Term originalMby,
java.util.Map<LocationVariable,ProgramVariable> atPreVars,
ProgramVariable selfVar,
ProgramVariable resultVar,
ImmutableList<ProgramVariable> paramVars) |
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.
|
InformationFlowContractImpl(java.lang.String baseName,
KeYJavaType forClass,
IProgramMethod pm,
KeYJavaType specifiedIn,
Modality modality,
Term pre,
Term freePre,
Term mby,
Term mod,
boolean hasRealMod,
Term self,
ImmutableList<Term> params,
Term result,
Term exc,
Term heapAtPre,
Term dep,
ImmutableList<InfFlowSpec> infFlowSpecs,
boolean toBeSaved) |
InformationFlowContractImpl(java.lang.String baseName,
KeYJavaType forClass,
IProgramMethod pm,
KeYJavaType specifiedIn,
Modality modality,
Term pre,
Term freePre,
Term mby,
Term mod,
boolean hasRealMod,
Term self,
ImmutableList<Term> params,
Term result,
Term exc,
Term heapAtPre,
Term dep,
ImmutableList<InfFlowSpec> infFlowSpecs,
boolean toBeSaved) |
InformationFlowContractImpl(java.lang.String baseName,
java.lang.String name,
KeYJavaType forClass,
IProgramMethod pm,
KeYJavaType specifiedIn,
Modality modality,
Term pre,
Term freePre,
Term mby,
Term mod,
boolean hasRealMod,
Term self,
ImmutableList<Term> params,
Term result,
Term exc,
Term heapAtPre,
Term dep,
ImmutableList<InfFlowSpec> infFlowSpecs,
boolean toBeSaved,
int id) |
InformationFlowContractImpl(java.lang.String baseName,
java.lang.String name,
KeYJavaType forClass,
IProgramMethod pm,
KeYJavaType specifiedIn,
Modality modality,
Term pre,
Term freePre,
Term mby,
Term mod,
boolean hasRealMod,
Term self,
ImmutableList<Term> params,
Term result,
Term exc,
Term heapAtPre,
Term dep,
ImmutableList<InfFlowSpec> infFlowSpecs,
boolean toBeSaved,
int id) |
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.
|
LoopSpecImpl(LoopStatement loop,
IProgramMethod pm,
KeYJavaType kjt,
java.util.Map<LocationVariable,Term> invariants,
java.util.Map<LocationVariable,Term> freeInvariants,
java.util.Map<LocationVariable,Term> modifies,
java.util.Map<LocationVariable,ImmutableList<InfFlowSpec>> infFlowSpecs,
Term variant,
Term selfTerm,
ImmutableList<Term> localIns,
ImmutableList<Term> localOuts,
java.util.Map<LocationVariable,Term> atPres)
Creates a loop invariant.
|
LoopSpecImpl(LoopStatement loop,
IProgramMethod pm,
KeYJavaType kjt,
java.util.Map<LocationVariable,Term> invariants,
java.util.Map<LocationVariable,Term> freeInvariants,
java.util.Map<LocationVariable,Term> modifies,
java.util.Map<LocationVariable,ImmutableList<InfFlowSpec>> infFlowSpecs,
Term variant,
Term selfTerm,
ImmutableList<Term> localIns,
ImmutableList<Term> localOuts,
java.util.Map<LocationVariable,Term> atPres)
Creates a loop invariant.
|
OriginalVariables(ProgramVariable selfVar,
ProgramVariable resVar,
ProgramVariable excVar,
java.util.Map<? extends LocationVariable,? extends ProgramVariable> atPreVars,
ImmutableList<? extends ProgramVariable> paramVars)
Create new instance of original variables
|
RepresentsAxiom(java.lang.String name,
IObserverFunction target,
KeYJavaType kjt,
VisibilityModifier visibility,
Term pre,
Term rep,
ProgramVariable selfVar,
ImmutableList<ProgramVariable> paramVars,
java.util.Map<LocationVariable,ProgramVariable> atPreVars) |
RepresentsAxiom(java.lang.String name,
java.lang.String displayName,
IObserverFunction target,
KeYJavaType kjt,
VisibilityModifier visibility,
Term pre,
Term rep,
ProgramVariable selfVar,
ImmutableList<ProgramVariable> paramVars,
java.util.Map<LocationVariable,ProgramVariable> atPreVars) |
Constructor and Description |
---|
LoopSpecImpl(LoopStatement loop,
IProgramMethod pm,
KeYJavaType kjt,
java.util.Map<LocationVariable,Term> invariants,
java.util.Map<LocationVariable,Term> freeInvariants,
java.util.Map<LocationVariable,Term> modifies,
java.util.Map<LocationVariable,ImmutableList<InfFlowSpec>> infFlowSpecs,
Term variant,
Term selfTerm,
ImmutableList<Term> localIns,
ImmutableList<Term> localOuts,
java.util.Map<LocationVariable,Term> atPres)
Creates a loop invariant.
|
Modifier and Type | Method and Description |
---|---|
ImmutableList<PositionedString> |
JMLSpecExtractor.getWarnings() |
Modifier and Type | Method and Description |
---|---|
ImmutableSet<MergeContract> |
JMLSpecExtractor.extractMergeContracts(IProgramMethod method,
MergePointStatement mps,
ImmutableList<ProgramVariable> methodParams) |
Modifier and Type | Field and Description |
---|---|
protected ImmutableList<java.lang.String> |
TextualJMLConstruct.mods |
Modifier and Type | Method and Description |
---|---|
java.util.Map<java.lang.String,ImmutableList<LabeledParserRuleContext>> |
TextualJMLLoopSpec.getAssignables() |
java.util.Map<java.lang.String,ImmutableList<LabeledParserRuleContext>> |
TextualJMLLoopSpec.getAssignablesInit() |
java.util.Map<java.lang.String,ImmutableList<LabeledParserRuleContext>> |
TextualJMLLoopSpec.getFreeInvariants() |
java.util.Map<java.lang.String,ImmutableList<LabeledParserRuleContext>> |
TextualJMLLoopSpec.getInvariants() |
Modifier and Type | Method and Description |
---|---|
protected void |
TextualJMLConstruct.addGeneric(java.util.Map<java.lang.String,ImmutableList<LabeledParserRuleContext>> item,
LabeledParserRuleContext ps)
Deprecated.
|
Modifier and Type | Field and Description |
---|---|
ImmutableList<Term> |
JMLSpecFactory.ContractClauses.abbreviations |
ImmutableList<InfFlowSpec> |
JMLSpecFactory.ContractClauses.infFlowSpecs |
ImmutableList<ProgramVariable> |
ProgramVariableCollection.paramVars
The list of method parameters if the textual specification case is a method contract.
|
Modifier and Type | Method and Description |
---|---|
protected ImmutableList<ProgramVariable> |
JMLSpecFactory.collectLocalVariablesVisibleTo(Statement statement,
IProgramMethod method) |
Modifier and Type | Method and Description |
---|---|
ImmutableSet<MergeContract> |
JMLSpecFactory.createJMLMergeContracts(IProgramMethod method,
MergePointStatement mps,
TextualJMLMergePointDecl mergePointDecl,
ImmutableList<ProgramVariable> methodParams) |
Constructor and Description |
---|
ProgramVariableCollection(ProgramVariable selfVar,
ImmutableList<ProgramVariable> paramVars,
ProgramVariable resultVar,
ProgramVariable excVar,
java.util.Map<LocationVariable,LocationVariable> atPreVars,
java.util.Map<LocationVariable,Term> atPres)
Create a collection containing the specified variables.
|
ProgramVariableCollection(ProgramVariable selfVar,
ImmutableList<ProgramVariable> paramVars,
ProgramVariable resultVar,
ProgramVariable excVar,
java.util.Map<LocationVariable,LocationVariable> atPreVars,
java.util.Map<LocationVariable,Term> atPres,
java.util.Map<LocationVariable,LocationVariable> atBeforeVars,
java.util.Map<LocationVariable,Term> atBefores)
Create a collection containing the specified variables.
|
Modifier and Type | Method and Description |
---|---|
ImmutableList<PositionedString> |
JmlIO.getWarnings()
returns the gathered interpretation warnings, e.g., deprecated constructs.
|
ImmutableList<Term> |
JmlTermFactory.infflowspeclist(ImmutableList<Term> result) |
ImmutableList<TextualJMLConstruct> |
JmlIO.parseClassLevel(JmlLexer lexer)
Parses a JML constructs on class level, e.g., invariants and methods contracts, and returns a parse tree.
|
ImmutableList<TextualJMLConstruct> |
JmlIO.parseClassLevel(java.lang.String content)
Parses a JML constructs on class level, e.g., invariants and methods contracts, and returns a parse tree.
|
ImmutableList<TextualJMLConstruct> |
JmlIO.parseClassLevel(java.lang.String concatenatedComment,
java.lang.String fileName,
Position pos)
Parse and interpret class level comments.
|
ImmutableList<TextualJMLConstruct> |
JmlIO.parseMethodLevel(PositionedString positionedString)
Parses a JML constructs which occurs inside methods (mostly JML statements) and returns a parse tree.
|
ImmutableList<TextualJMLConstruct> |
JmlIO.parseMethodLevel(java.lang.String concatenatedComment,
java.lang.String fileName,
Position position)
Parse and interpret the given string as a method level construct.
|
Modifier and Type | Method and Description |
---|---|
SLExpression |
JmlTermFactory.createUnionF(boolean nullable,
Pair<KeYJavaType,ImmutableList<LogicVariable>> declVars,
Term expr,
Term guard) |
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.
|
Modifier and Type | Method and Description |
---|---|
ImmutableList<SLExpression> |
SLParameters.getParameters() |
ImmutableList<KeYJavaType> |
SLParameters.getSignature(Services services)
returns the type signature of the parameter list
|
Modifier and Type | Method and Description |
---|---|
void |
SLResolverManager.putIntoTopLocalVariablesNamespace(ImmutableList<? extends ProgramVariable> pvs)
Puts a list of local variables into the topmost namespace on the stack.
|
void |
SLResolverManager.putIntoTopLocalVariablesNamespace(ImmutableList<LogicVariable> pvs,
KeYJavaType kjt)
Puts a list of local variables into the topmost namespace on the stack.
|
Constructor and Description |
---|
SLParameters(ImmutableList<SLExpression> parameters) |
Modifier and Type | Method and Description |
---|---|
static ImmutableList<RuleAppContainer> |
RuleAppContainer.createAppContainers(ImmutableList<? extends RuleApp> rules,
PosInOccurrence pos,
Goal goal)
Create containers for RuleApps.
|
ImmutableList<RuleAppContainer> |
TacletAppContainer.createFurtherApps(Goal p_goal)
Create a list of new RuleAppContainers that are to be
considered for application.
|
abstract ImmutableList<RuleAppContainer> |
RuleAppContainer.createFurtherApps(Goal p_goal)
Create a list of new RuleAppContainers that are to be
considered for application.
|
ImmutableList<RuleAppContainer> |
BuiltInRuleAppContainer.createFurtherApps(Goal goal) |
protected static ImmutableList<RuleAppContainer> |
TacletAppContainer.createInitialAppContainers(ImmutableList<NoPosTacletApp> p_app,
PosInOccurrence p_pio,
Goal p_goal) |
ImmutableList<IfFormulaInstantiation> |
IfInstantiationCachePool.IfInstantiationCache.get(boolean antec,
java.lang.Long key) |
ImmutableList<NoPosTacletApp> |
IfInstantiator.getResults() |
Modifier and Type | Method and Description |
---|---|
static ImmutableList<RuleAppContainer> |
RuleAppContainer.createAppContainers(ImmutableList<? extends RuleApp> rules,
PosInOccurrence pos,
Goal goal)
Create containers for RuleApps.
|
protected static ImmutableList<RuleAppContainer> |
TacletAppContainer.createInitialAppContainers(ImmutableList<NoPosTacletApp> p_app,
PosInOccurrence p_pio,
Goal p_goal) |
void |
IfInstantiationCachePool.IfInstantiationCache.put(boolean antec,
java.lang.Long key,
ImmutableList<IfFormulaInstantiation> value) |
void |
FocussedBreakpointRuleApplicationManager.rulesAdded(ImmutableList<? extends RuleApp> rules,
PosInOccurrence pos) |
void |
FocussedRuleApplicationManager.rulesAdded(ImmutableList<? extends RuleApp> rules,
PosInOccurrence pos) |
void |
QueueRuleApplicationManager.rulesAdded(ImmutableList<? extends RuleApp> rules,
PosInOccurrence pos)
Implementation of the method from
NewRuleListener . |
Modifier and Type | Method and Description |
---|---|
protected ImmutableList<Term> |
AbstractMonomialSmallerThanFeature.collectAtoms(Term t) |
ImmutableList<Term> |
SmallerThanFeature.Collector.getResult() |
Modifier and Type | Method and Description |
---|---|
protected boolean |
NonDuplicateAppFeature.containsRuleApp(ImmutableList<RuleApp> list,
TacletApp rapp,
PosInOccurrence pio) |
protected boolean |
SmallerThanFeature.lessThan(ImmutableList<Term> list1,
ImmutableList<Term> list2,
PosInOccurrence focus,
Goal currentGoal) |
protected boolean |
SmallerThanFeature.lessThan(ImmutableList<Term> list1,
ImmutableList<Term> list2,
PosInOccurrence focus,
Goal currentGoal) |
Modifier and Type | Method and Description |
---|---|
protected ImmutableList<Term> |
AbstractUpdateExtractor.computeOriginalUpdates(PosInOccurrence pio,
boolean currentLayout)
Computes the original updates.
|
protected ImmutableList<Term> |
SymbolicLayoutExtractor.extractInitialUpdates()
Computes the initial updates to consider.
|
protected ImmutableList<Node> |
SymbolicExecutionTreeBuilder.findMethodCallStack(java.util.Map<Node,ImmutableList<Node>> methodCallStack,
Node node) |
ImmutableList<ISymbolicAssociation> |
SymbolicLayoutReader.AbstractKeYlessAssociationValueContainer.getAssociations()
Returns the contained associations.
|
ImmutableList<IExecutionNode<?>> |
ExecutionNodeReader.AbstractKeYlessExecutionBlockStartNode.getBlockCompletions()
Returns the up to now discovered
IExecutionNode s. |
ImmutableList<IExecutionBlockStartNode<?>> |
ExecutionNodeReader.AbstractKeYlessExecutionNode.getCompletedBlocks()
Returns all code blocks completed by this
IExecutionBlockStartNode . |
ImmutableList<Term> |
ExecutionNodeReader.KeYlessOperationContract.getContractParams()
Returns the parameters of the called method for which a
Contract is applied. |
ImmutableList<ISymbolicEquivalenceClass> |
SymbolicLayoutReader.KeYlessLayout.getEquivalenceClasses()
Returns the equivalence classes.
|
ImmutableList<ISymbolicEquivalenceClass> |
SymbolicLayoutExtractor.getEquivalenceClasses(int layoutIndex)
Returns the equivalence class of the memory layout defined by the index.
|
ImmutableList<IExecutionLink> |
ExecutionNodeReader.AbstractKeYlessExecutionNode.getIncomingLinks()
Returns all available incoming links.
|
ImmutableList<ISymbolicEquivalenceClass> |
ExecutionNodeReader.AbstractKeYlessExecutionNode.getLayoutsEquivalenceClasses(int configurationIndex)
Returns the equivalence classes of the memory layout with the given index.
|
ImmutableList<IExecutionBaseMethodReturn<?>> |
ExecutionNodeReader.KeYlessMethodCall.getMethodReturns()
Returns the up to now discovered
IExecutionBaseMethodReturn s. |
ImmutableList<ISymbolicObject> |
SymbolicLayoutReader.KeYlessLayout.getObjects()
Returns all available symbolic objects.
|
ImmutableList<IExecutionLink> |
ExecutionNodeReader.AbstractKeYlessExecutionNode.getOutgoingLinks()
Returns all available outgoing links.
|
ImmutableList<Goal> |
AbstractUpdateExtractor.NodeGoal.getStartingGoals()
Returns the
Goal s at which backward iteration has started. |
ImmutableList<IExecutionTermination> |
ExecutionNodeReader.KeYlessStart.getTerminations()
Returns the up to now discovered
IExecutionTermination s. |
ImmutableList<Term> |
SymbolicLayoutReader.KeYlessEquivalenceClass.getTerms()
Returns the terms which represents the same
ISymbolicObject . |
ImmutableList<java.lang.String> |
SymbolicLayoutReader.KeYlessEquivalenceClass.getTermStrings()
Returns the terms which represents the same
ISymbolicObject as human readable String . |
ImmutableList<ISymbolicValue> |
SymbolicLayoutReader.AbstractKeYlessAssociationValueContainer.getValues()
Returns the contained values.
|
protected ImmutableList<ISymbolicEquivalenceClass> |
SymbolicLayoutExtractor.lazyComputeEquivalenceClasses(ImmutableSet<Term> appliedCuts)
Computes the equivalence classes from the given applied cut rules
lazily when
SymbolicLayoutExtractor.getEquivalenceClasses(int) is called the first time. |
Modifier and Type | Method and Description |
---|---|
protected java.util.Map<SymbolicExecutionTreeBuilder.JavaPair,ImmutableList<IExecutionNode<?>>> |
SymbolicExecutionTreeBuilder.findAfterBlockMap(java.util.Map<Node,java.util.Map<SymbolicExecutionTreeBuilder.JavaPair,ImmutableList<IExecutionNode<?>>>> afterBlockMaps,
Node node)
Searches the relevant after block
Map in the given once for the given Node . |
protected java.util.Map<Node,java.util.Map<SymbolicExecutionTreeBuilder.JavaPair,ImmutableList<IExecutionNode<?>>>> |
SymbolicExecutionTreeBuilder.getAfterBlockMaps(int id)
Returns the after block map used for the given ID.
|
protected java.util.Map<Node,java.util.Map<SymbolicExecutionTreeBuilder.JavaPair,ImmutableList<IExecutionNode<?>>>> |
SymbolicExecutionTreeBuilder.getAfterBlockMaps(SymbolicExecutionTermLabel label)
Returns the after block map.
|
protected java.util.Map<Node,ImmutableList<Node>> |
SymbolicExecutionTreeBuilder.getMethodCallStack(int id)
Returns the method call stack used for the given ID.
|
protected java.util.Map<Node,ImmutableList<Node>> |
SymbolicExecutionTreeBuilder.getMethodCallStack(RuleApp ruleApp)
Returns the method call stack.
|
protected java.util.Map<Node,ImmutableList<Node>> |
SymbolicExecutionTreeBuilder.getMethodCallStack(SymbolicExecutionTermLabel label)
Returns the method call stack.
|
protected java.util.Map<SymbolicExecutionTreeBuilder.JavaPair,ImmutableList<IExecutionNode<?>>> |
SymbolicExecutionTreeBuilder.updateAfterBlockMap(Node node,
RuleApp ruleApp)
Updates the after block maps when a symbolic execution tree node is detected.
|
protected Pair<java.lang.Boolean,ImmutableList<Term>> |
ExecutionVariableExtractor.updateAlreadyVisitedObjects(ImmutableList<Term> alreadyVisitedObjects,
Term value)
Updates the already visited objects list if required.
|
Modifier and Type | Method and Description |
---|---|
protected void |
SymbolicLayoutExtractor.applyCutRules(ProofStarter starter,
java.util.Set<Term> symbolicObjects,
ImmutableList<Term> updates)
Applies cut rules to the given side proofs to compute equivalence classes.
|
protected ISymbolicLayout |
SymbolicLayoutExtractor.createLayoutFromExecutionVariableValuePairs(ImmutableList<ISymbolicEquivalenceClass> equivalentClasses,
java.util.Set<AbstractUpdateExtractor.ExecutionVariableValuePair> pairs,
java.lang.String stateName)
Creates an
ISymbolicLayout which shows the objects,
values and associations defined by the given ExecutionVariableValuePair s. |
protected void |
SymbolicLayoutExtractor.createObjectForTerm(java.util.Map<Term,SymbolicObject> objects,
ImmutableList<ISymbolicEquivalenceClass> equivalentClasses,
SymbolicLayout result,
Term objectTerm)
Creates for the object defined by the given
Term an SymbolicObject instance if not already available. |
protected void |
ExecutionVariableExtractor.createValues(IExecutionVariable variable,
java.util.List<AbstractUpdateExtractor.ExecutionVariableValuePair> pairs,
AbstractUpdateExtractor.ExecutionVariableValuePair firstPair,
java.util.Map<de.uka.ilkd.key.symbolic_execution.ExecutionVariableExtractor.ParentDefinition,java.util.Map<de.uka.ilkd.key.symbolic_execution.ExecutionVariableExtractor.LocationDefinition,java.util.List<AbstractUpdateExtractor.ExecutionVariableValuePair>>> contentMap,
java.util.List<IExecutionValue> valueListToFill,
ImmutableList<Term> alreadyVisitedObjects)
Creates the
IExecutionValue s of the given IExecutionVariable . |
protected IExecutionVariable |
ExecutionVariableExtractor.createVariablesValueStructure(java.util.List<AbstractUpdateExtractor.ExecutionVariableValuePair> pairs,
java.util.Map<de.uka.ilkd.key.symbolic_execution.ExecutionVariableExtractor.ParentDefinition,java.util.Map<de.uka.ilkd.key.symbolic_execution.ExecutionVariableExtractor.LocationDefinition,java.util.List<AbstractUpdateExtractor.ExecutionVariableValuePair>>> contentMap,
ExecutionVariableExtractor.ExtractedExecutionValue parentValue,
ImmutableList<Term> alreadyVisitedObjects)
Creates an
IExecutionVariable for the given ExecutionVariableValuePair s. |
protected ISymbolicEquivalenceClass |
SymbolicLayoutExtractor.findEquivalentClass(ImmutableList<ISymbolicEquivalenceClass> equivalentClasses,
Term term)
Searches the
ISymbolicEquivalenceClass from the given one
which contains the given Term . |
protected boolean |
SymbolicExecutionTreeBuilder.isContained(ImmutableList<IExecutionNode<?>> list,
Node node)
Checks if one of the give
IExecutionNode s represents the given Node . |
protected ISymbolicLayout |
SymbolicLayoutExtractor.lazyComputeLayout(ImmutableSet<Term> layout,
java.util.Set<AbstractUpdateExtractor.ExtractLocationParameter> locations,
ImmutableList<ISymbolicEquivalenceClass> equivalentClasses,
java.lang.String stateName,
boolean currentLayout)
Computes a memory layout lazily when it is first time requested via
#getLayout(Map, int, Term, Set, String, boolean) . |
protected Pair<java.lang.Boolean,ImmutableList<Term>> |
ExecutionVariableExtractor.updateAlreadyVisitedObjects(ImmutableList<Term> alreadyVisitedObjects,
Term value)
Updates the already visited objects list if required.
|
protected java.util.Set<AbstractUpdateExtractor.ExtractLocationParameter> |
SymbolicLayoutExtractor.updateLocationsAccordingtoEquivalentClass(java.util.Set<AbstractUpdateExtractor.ExtractLocationParameter> locations,
ImmutableList<ISymbolicEquivalenceClass> equivalentClasses)
Replaces the parent of each
ExtractLocationParameter according
to the ISymbolicEquivalenceClass es, because there is no guarantee
that the strategy evaluates each aliased location to the same symbolic value. |
Modifier and Type | Method and Description |
---|---|
protected java.util.Map<SymbolicExecutionTreeBuilder.JavaPair,ImmutableList<IExecutionNode<?>>> |
SymbolicExecutionTreeBuilder.findAfterBlockMap(java.util.Map<Node,java.util.Map<SymbolicExecutionTreeBuilder.JavaPair,ImmutableList<IExecutionNode<?>>>> afterBlockMaps,
Node node)
Searches the relevant after block
Map in the given once for the given Node . |
protected ImmutableList<Node> |
SymbolicExecutionTreeBuilder.findMethodCallStack(java.util.Map<Node,ImmutableList<Node>> methodCallStack,
Node node) |
Constructor and Description |
---|
JavaPair(java.lang.Integer stackSize,
ImmutableList<SourceElement> elementsOfInterest)
Constructor.
|
KeYlessEquivalenceClass(ImmutableList<java.lang.String> termStrings,
java.lang.String representativeString)
Constructor.
|
NodeGoal(Node currentNode,
ImmutableList<Goal> startingGoals)
A reached child node during backward iteration.
|
Modifier and Type | Method and Description |
---|---|
ImmutableList<IExecutionNode<?>> |
IExecutionBlockStartNode.getBlockCompletions()
Returns the up to now discovered
IExecutionNode s. |
ImmutableList<IExecutionBlockStartNode<?>> |
IExecutionNode.getCompletedBlocks()
Returns all code blocks completed by this
IExecutionBlockStartNode . |
ImmutableList<Term> |
IExecutionOperationContract.getContractParams()
Returns the parameters of the called method for which a
Contract is applied. |
ImmutableList<IExecutionLink> |
IExecutionNode.getIncomingLinks()
Returns all available incoming links.
|
ImmutableList<ISymbolicEquivalenceClass> |
IExecutionNode.getLayoutsEquivalenceClasses(int layoutIndex)
Returns the equivalence classes of the memory layout with the given index.
|
ImmutableList<IExecutionBaseMethodReturn<?>> |
IExecutionMethodCall.getMethodReturns()
Returns the up to now discovered
IExecutionBaseMethodReturn s. |
ImmutableList<IExecutionLink> |
IExecutionNode.getOutgoingLinks()
Returns all available outgoing links.
|
ImmutableList<IExecutionTermination> |
IExecutionStart.getTerminations()
Returns the up to now discovered
IExecutionTermination s. |
Modifier and Type | Method and Description |
---|---|
ImmutableList<IExecutionNode<?>> |
AbstractExecutionBlockStartNode.getBlockCompletions()
Returns the up to now discovered
IExecutionNode s. |
ImmutableList<IExecutionBlockStartNode<?>> |
AbstractExecutionNode.getCompletedBlocks()
Returns all code blocks completed by this
IExecutionBlockStartNode . |
ImmutableList<Term> |
ExecutionOperationContract.getContractParams()
Returns the parameters of the called method for which a
Contract is applied. |
ImmutableList<IExecutionLink> |
AbstractExecutionNode.getIncomingLinks()
Returns all available incoming links.
|
ImmutableList<ISymbolicEquivalenceClass> |
AbstractExecutionNode.getLayoutsEquivalenceClasses(int layoutIndex)
Returns the equivalence classes of the memory layout with the given index.
|
ImmutableList<IExecutionBaseMethodReturn<?>> |
ExecutionMethodCall.getMethodReturns()
Returns the up to now discovered
IExecutionBaseMethodReturn s. |
ImmutableList<IExecutionLink> |
AbstractExecutionNode.getOutgoingLinks()
Returns all available outgoing links.
|
ImmutableList<IExecutionTermination> |
ExecutionStart.getTerminations()
Returns the up to now discovered
IExecutionTermination s. |
Modifier and Type | Method and Description |
---|---|
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. |
Modifier and Type | Method and Description |
---|---|
ImmutableList<ISymbolicAssociation> |
ISymbolicAssociationValueContainer.getAssociations()
Returns the contained associations.
|
ImmutableList<ISymbolicEquivalenceClass> |
ISymbolicLayout.getEquivalenceClasses()
Returns the equivalence classes.
|
ImmutableList<ISymbolicObject> |
ISymbolicLayout.getObjects()
Returns all available symbolic objects.
|
ImmutableList<Term> |
ISymbolicEquivalenceClass.getTerms()
Returns the terms which represents the same
ISymbolicObject . |
ImmutableList<java.lang.String> |
ISymbolicEquivalenceClass.getTermStrings()
Returns the terms which represents the same
ISymbolicObject as human readable String . |
ImmutableList<ISymbolicValue> |
ISymbolicAssociationValueContainer.getValues()
Returns the contained values.
|
Modifier and Type | Method and Description |
---|---|
ImmutableList<ISymbolicAssociation> |
AbstractSymbolicAssociationValueContainer.getAssociations()
Returns the contained associations.
|
ImmutableList<ISymbolicEquivalenceClass> |
SymbolicLayout.getEquivalenceClasses()
Returns the equivalence classes.
|
ImmutableList<ISymbolicObject> |
SymbolicLayout.getObjects()
Returns all available symbolic objects.
|
ImmutableList<Term> |
SymbolicEquivalenceClass.getTerms()
Returns the terms which represents the same
ISymbolicObject . |
ImmutableList<java.lang.String> |
SymbolicEquivalenceClass.getTermStrings()
Returns the terms which represents the same
ISymbolicObject as human readable String . |
ImmutableList<ISymbolicValue> |
AbstractSymbolicAssociationValueContainer.getValues()
Returns the contained values.
|
Constructor and Description |
---|
SymbolicEquivalenceClass(Services services,
ImmutableList<Term> terms,
IModelSettings settings)
Constructor.
|
SymbolicLayout(IModelSettings settings,
ImmutableList<ISymbolicEquivalenceClass> equivalenceClasses)
Constructor.
|
Modifier and Type | Method and Description |
---|---|
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 static ImmutableList<ProgramVariable> |
ProgramMethodSubsetPO.convert(java.util.Collection<LocationVariable> c)
Converts the given
Collection into an ImmutableList . |
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 |
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.
|
Modifier and Type | Method and Description |
---|---|
protected ImmutableList<TermLabelManager.TermLabelConfiguration> |
SimplifyTermProfile.computeTermLabelConfiguration()
Computes the
TermLabelManager.TermLabelConfiguration to use in this Profile . |
protected ImmutableList<TermLabelManager.TermLabelConfiguration> |
SymbolicExecutionJavaProfile.computeTermLabelConfiguration()
Computes the
TermLabelManager.TermLabelConfiguration to use in this Profile . |
static ImmutableList<TermLabelManager.TermLabelConfiguration> |
SymbolicExecutionJavaProfile.getSymbolicExecutionTermLabelConfigurations(boolean predicateEvaluationEnabled)
Returns the additional
TermLabelFactory instances used for symbolic execution. |
protected ImmutableList<BuiltInRule> |
SymbolicExecutionJavaProfile.initBuiltInRules() |
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.
|
Modifier and Type | Method and Description |
---|---|
ImmutableList<Access> |
Location.getAccesses()
Returns the
Access path. |
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. |
Modifier and Type | Method and Description |
---|---|
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 AbstractSlicer.SequentInfo |
AbstractSlicer.analyzeSequent(Node node,
ImmutableList<ISymbolicEquivalenceClass> sec)
Computes the aliases specified by the updates of the current
Node
at the application PosInOccurrence and computes the current this reference. |
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. |
static <T> int |
AbstractSlicer.computeFirstCommonPrefixLength(ImmutableList<ImmutableList<T>> candidates,
ImmutableList<T> toCheck)
Computes the length of a common prefix.
|
static <T> int |
AbstractSlicer.computeFirstCommonPrefixLength(ImmutableList<ImmutableList<T>> candidates,
ImmutableList<T> toCheck)
Computes the length of a common prefix.
|
protected abstract ImmutableArray<Node> |
AbstractSlicer.doSlicing(Node seedNode,
Location seedLocation,
ImmutableList<ISymbolicEquivalenceClass> sec)
Performs the slicing.
|
ImmutableArray<Node> |
AbstractBackwardSlicer.doSlicing(Node seedNode,
Location seedLocation,
ImmutableList<ISymbolicEquivalenceClass> sec)
Performs the slicing.
|
ImmutableArray<Node> |
AbstractSlicer.slice(Node seedNode,
Location seedLocation,
ImmutableList<ISymbolicEquivalenceClass> sec)
Computes the slice.
|
ImmutableArray<Node> |
AbstractSlicer.slice(Node seedNode,
ReferencePrefix seedLocation,
ImmutableList<ISymbolicEquivalenceClass> sec)
Computes the slice.
|
ImmutableArray<Node> |
AbstractSlicer.slice(Node seedNode,
Term term,
ImmutableList<ISymbolicEquivalenceClass> sec)
Computes the slice.
|
static <T> boolean |
AbstractSlicer.startsWith(ImmutableList<T> list,
ImmutableList<T> prefix)
Checks if the given
ImmutableList starts with the given prefix. |
static <T> boolean |
AbstractSlicer.startsWith(ImmutableList<T> list,
ImmutableList<T> prefix)
Checks if the given
ImmutableList starts with the given prefix. |
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. |
Modifier and Type | Method and Description |
---|---|
static <T> int |
AbstractSlicer.computeFirstCommonPrefixLength(ImmutableList<ImmutableList<T>> candidates,
ImmutableList<T> toCheck)
Computes the length of a common prefix.
|
Constructor and Description |
---|
Location(ImmutableList<Access> accesses)
Constructor.
|
Modifier and Type | Method and Description |
---|---|
void |
SymbolicExecutionGoalChooser.init(Proof p_proof,
ImmutableList<Goal> p_goals)
Initialise this DefaultGoalChooser for use with a given Proof and a list of goals.
|
void |
SymbolicExecutionGoalChooser.updateGoalList(Node node,
ImmutableList<Goal> newGoals)
The given node has become an internal node of the proof tree, and the
children of the node are the given goals
|
Modifier and Type | Method and Description |
---|---|
ImmutableList<ProgramVariable> |
AbstractConditionalBreakpoint.getVarsForCondition() |
Modifier and Type | Method and Description |
---|---|
void |
AbstractConditionalBreakpoint.setVarsForCondition(ImmutableList<ProgramVariable> varsForCondition) |
Modifier and Type | Method and Description |
---|---|
static ImmutableList<Term> |
SymbolicExecutionUtil.collectElementaryUpdates(Term term)
Collects the
ElementaryUpdate s in the given Term . |
static ImmutableList<Goal> |
SymbolicExecutionUtil.collectGoalsInSubtree(IExecutionElement executionElement)
Collects all
Goal s in the subtree of the given IExecutionElement . |
static ImmutableList<Goal> |
SymbolicExecutionUtil.collectGoalsInSubtree(Node node)
|
static ImmutableList<Term> |
SymbolicExecutionUtil.computeRootElementaryUpdates(Node root)
Computes the initial
ElementaryUpdate s on the given root Node . |
static ImmutableList<Term> |
SymbolicExecutionUtil.listSemisequentTerms(Semisequent semisequent)
Lists the
Term s contained in the given Semisequent . |
Modifier and Type | Method and Description |
---|---|
Pair<ImmutableList<Term>,Term> |
SymbolicExecutionUtil.ContractPostOrExcPostExceptionVariableResult.getUpdatesAndTerm()
Returns the updates.
|
Modifier and Type | Method and Description |
---|---|
static Sequent |
SymbolicExecutionUtil.createSequentToProveWithNewSuccedent(Node node,
PosInOccurrence pio,
Term additionalAntecedent,
Term newSuccedent,
ImmutableList<Term> updates,
boolean addResultLabel)
|
static Sequent |
SymbolicExecutionUtil.createSequentToProveWithNewSuccedent(Node node,
Term additionalAntecedent,
Term newSuccedent,
ImmutableList<Term> updates,
boolean addResultLabel)
|
Constructor and Description |
---|
ContractPostOrExcPostExceptionVariableResult(Term workingTerm,
Pair<ImmutableList<Term>,Term> updatesAndTerm,
Term exceptionDefinition,
Term exceptionEquality)
Constructor.
|
Modifier and Type | Method and Description |
---|---|
ImmutableList<TacletFormula> |
TacletSetTranslation.getNotTranslated()
Returns all taclet that have not been translated.
|
ImmutableList<TacletFormula> |
DefaultTacletSetTranslation.getNotTranslated() |
ImmutableList<TacletFormula> |
TacletSetTranslation.getTranslation(ImmutableSet<Sort> sorts)
Builds the translation of the taclets given by calling the method
setTacletSet() . |
ImmutableList<TacletFormula> |
DefaultTacletSetTranslation.getTranslation(ImmutableSet<Sort> sorts) |
Modifier and Type | Method and Description |
---|---|
abstract ImmutableList<Taclet> |
TacletLoader.loadTaclets()
get the set of taclets to examine
(either from the system or from a file)
|
ImmutableList<Taclet> |
TacletLoader.TacletFromFileLoader.loadTaclets() |
ImmutableList<Taclet> |
TacletLoader.KeYsTacletsLoader.loadTaclets() |
Modifier and Type | Method and Description |
---|---|
void |
MediatorProofControl.startAutoMode(Proof proof,
ImmutableList<Goal> goals,
ProverTaskListener ptl) |
Modifier and Type | Field and Description |
---|---|
ImmutableList<Term> |
InfFlowSpec.newObjects |
ImmutableList<Term> |
InfFlowSpec.postExpressions |
ImmutableList<Term> |
InfFlowSpec.preExpressions |
Modifier and Type | Method and Description |
---|---|
static ImmutableList<Term> |
MiscTools.filterOutDuplicates(ImmutableList<Term> localIns,
ImmutableList<Term> localOuts) |
static ImmutableList<Term> |
MiscTools.toTermList(java.lang.Iterable<ProgramVariable> list,
TermBuilder tb) |
Modifier and Type | Method and Description |
---|---|
static ImmutableList<Term> |
MiscTools.filterOutDuplicates(ImmutableList<Term> localIns,
ImmutableList<Term> localOuts) |
static ImmutableList<Term> |
MiscTools.filterOutDuplicates(ImmutableList<Term> localIns,
ImmutableList<Term> localOuts) |
ApplyStrategyInfo |
ProofStarter.start(ImmutableList<Goal> goals)
starts proof attempt
|
Constructor and Description |
---|
InfFlowSpec(ImmutableList<Term> preExpressions,
ImmutableList<Term> postExpressions,
ImmutableList<Term> newObjects) |
InfFlowSpec(ImmutableList<Term> preExpressions,
ImmutableList<Term> postExpressions,
ImmutableList<Term> newObjects) |
InfFlowSpec(ImmutableList<Term> preExpressions,
ImmutableList<Term> postExpressions,
ImmutableList<Term> newObjects) |
Modifier and Type | Method and Description |
---|---|
ImmutableList<Term> |
MergeParamsSpec.getPredicates() |
static ImmutableList<SymbolicExecutionState> |
MergeRuleUtils.sequentsToSEPairs(java.lang.Iterable<MergePartner> sequentInfos)
Convenience method for converting a whole list of goal-pio combinations
to symbolic execution states; relies on
MergeRuleUtils.sequentToSETriple(Node, PosInOccurrence, Services) . |
Constructor and Description |
---|
MergeParamsSpec(java.lang.String latticeType,
LocationVariable placeholder,
ImmutableList<Term> predicates) |
Modifier and Type | Class and Description |
---|---|
class |
ImmutableSLList<T>
Simple implementation of a non-destructive (unmodifiable) list.
|
Modifier and Type | Method and Description |
---|---|
ImmutableList<T> |
ImmutableList.append(ImmutableList<T> list)
appends a whole list (non-destructive)
|
ImmutableList<T> |
ImmutableSLList.append(java.lang.Iterable<T> collection) |
ImmutableList<T> |
ImmutableList.append(java.lang.Iterable<T> collection)
appends an iterable collection
|
ImmutableList<T> |
ImmutableList.append(T... array)
appends element at end (non-destructive) (O(n))
|
ImmutableList<T> |
ImmutableList.append(T element)
appends element to the list (non-destructive)
|
static <T> ImmutableList<T> |
Immutables.concatDuplicateFreeLists(ImmutableList<T> l1,
ImmutableList<? extends T> l2) |
static <T> ImmutableList<T> |
Immutables.createListFrom(java.lang.Iterable<T> iterable) |
static <T> ImmutableList<T> |
ImmutableList.fromList(java.util.Collection<T> list)
Creates an ImmutableList from a List.
|
ImmutableList<T> |
ImmutableList.prepend(ImmutableList<T> list)
prepends a whole list (non-destructive)
|
ImmutableList<T> |
ImmutableSLList.prepend(T... array)
prepends array (O(n))
|
ImmutableList<T> |
ImmutableList.prepend(T... array)
prepends array (O(n))
|
ImmutableList<T> |
ImmutableList.prepend(T element)
prepends element to the list (non-destructive)
|
protected ImmutableList<T> |
ImmutableSLList.prepend(T[] array,
int n)
prepends the first
n elements of an array (O(n)) |
ImmutableList<T> |
ImmutableList.prependReverse(ImmutableList<T> collection)
prepends an immutable list in reverse order, i.e.,
[4,5,6].prepend([1,2,3]) will be [3,2,1,4,5,6]
(more efficient than
prepend(ImmutableList) ) |
ImmutableList<T> |
ImmutableSLList.prependReverse(java.lang.Iterable<T> collection) |
ImmutableList<T> |
ImmutableList.prependReverse(java.lang.Iterable<T> collection)
prepends an iterable collection in reverse order, i.e.,
[4,5,6].prepend([1,2,3]) will be [3,2,1,4,5,6]
|
ImmutableList<T> |
ImmutableList.removeAll(T obj)
removes all occurrences of obj
|
static <T> ImmutableList<T> |
Immutables.removeDuplicates(ImmutableList<T> list)
Removes duplicate entries from an immutable list.
|
ImmutableList<T> |
ImmutableList.removeFirst(T obj)
removes first occurrence of obj
|
ImmutableList<T> |
ImmutableSLList.reverse()
Reverses this list (O(N))
|
ImmutableList<T> |
ImmutableList.reverse()
Reverses this list
|
ImmutableList<T> |
ImmutableList.tail() |
ImmutableList<T> |
ImmutableSLList.take(int n)
first
n elements of the list are truncated |
ImmutableList<T> |
ImmutableList.take(int n) |
ImmutableList<S> |
ImmutableArray.toImmutableList()
Convert an
ImmutableArray to an ImmutableList . |
ImmutableList<T> |
DefaultImmutableSet.toImmutableList()
Get the underlying immutable list.
|
Modifier and Type | Method and Description |
---|---|
static <T> java.util.stream.Collector<T,java.util.List<T>,ImmutableList<T>> |
ImmutableList.collector()
Returns a Collector that accumulates the input elements into a new ImmutableList.
|
static <T> java.util.stream.Collector<T,java.util.List<T>,ImmutableList<T>> |
ImmutableSLList.toImmutableList() |
Modifier and Type | Method and Description |
---|---|
ImmutableList<T> |
ImmutableList.append(ImmutableList<T> list)
appends a whole list (non-destructive)
|
static <T> ImmutableList<T> |
Immutables.concatDuplicateFreeLists(ImmutableList<T> l1,
ImmutableList<? extends T> l2) |
static <T> ImmutableList<T> |
Immutables.concatDuplicateFreeLists(ImmutableList<T> l1,
ImmutableList<? extends T> l2) |
static <T> ImmutableSet<T> |
DefaultImmutableSet.fromImmutableList(ImmutableList<T> list)
Create an immutable set from an immutable list.
|
static <T> boolean |
Immutables.isDuplicateFree(ImmutableList<T> list)
Checks whether an immutable list is free of duplicates.
|
ImmutableList<T> |
ImmutableList.prepend(ImmutableList<T> list)
prepends a whole list (non-destructive)
|
ImmutableList<T> |
ImmutableList.prependReverse(ImmutableList<T> collection)
prepends an immutable list in reverse order, i.e.,
[4,5,6].prepend([1,2,3]) will be [3,2,1,4,5,6]
(more efficient than
prepend(ImmutableList) ) |
static <T> ImmutableList<T> |
Immutables.removeDuplicates(ImmutableList<T> list)
Removes duplicate entries from an immutable list.
|
Copyright © 2003-2019 The KeY-Project.