Package | Description |
---|---|
de.uka.ilkd.key.gui.mergerule.predicateabstraction | |
de.uka.ilkd.key.informationflow.po | |
de.uka.ilkd.key.java |
This package contains classes that cover the Java programming language.
|
de.uka.ilkd.key.java.declaration |
Elements of the Java syntax tree representing declarations.
|
de.uka.ilkd.key.java.reference |
Elements of the Java syntax tree representing implicit or explicit (named)
references to other program elements.
|
de.uka.ilkd.key.java.visitor |
contains classes representing visitors traversing the tree
structure of Java programs.
|
de.uka.ilkd.key.logic |
provides a representation for the term and sequent
structure.
|
de.uka.ilkd.key.logic.label | |
de.uka.ilkd.key.logic.op |
contains the operators of
Term s. |
de.uka.ilkd.key.pp |
This package contains pretty-printing functionality used by the GUI and for
saving proofs.
|
de.uka.ilkd.key.proof |
This package contains the core data structures of proofs, nodes, goals, as well
as machinery to deal with these data structures.
|
de.uka.ilkd.key.proof_references.analyst | |
de.uka.ilkd.key.proof.init |
This package contains classes handling prover initialisation.
|
de.uka.ilkd.key.rule |
This package contains classes for implementing rules.
|
de.uka.ilkd.key.rule.merge.procedures | |
de.uka.ilkd.key.rule.metaconstruct |
contains classes representing the meta constructs of
Taclet s. |
de.uka.ilkd.key.rule.tacletbuilder | |
de.uka.ilkd.key.speclang |
This package contains the specification language frontends of KeY.
|
de.uka.ilkd.key.speclang.jml | |
de.uka.ilkd.key.speclang.jml.translation | |
de.uka.ilkd.key.speclang.njml |
This package provides the functionalities of parsing JML comments into KeY constructs.
|
de.uka.ilkd.key.speclang.translation | |
de.uka.ilkd.key.symbolic_execution | |
de.uka.ilkd.key.symbolic_execution.po | |
de.uka.ilkd.key.symbolic_execution.slicing | |
de.uka.ilkd.key.symbolic_execution.strategy.breakpoint | |
de.uka.ilkd.key.symbolic_execution.util | |
de.uka.ilkd.key.util |
This package is a grab bag of miscellaneous useful code fragments.
|
Modifier and Type | Method and Description |
---|---|
ProgramVariable |
AbstractDomainElemChoice.getProgVar() |
Modifier and Type | Method and Description |
---|---|
void |
AbstractDomainElemChoice.setProgVar(ProgramVariable progVar) |
Constructor and Description |
---|
AbstractDomainElemChoice(ProgramVariable progVar,
java.util.Optional<AbstractPredicateAbstractionDomainElement> abstrDomElem) |
Modifier and Type | Method and Description |
---|---|
static ProgramVariable |
InfFlowProofSymbols.searchPV(java.lang.String s,
Services services) |
Modifier and Type | Method and Description |
---|---|
protected Term |
LoopInvExecutionPO.buildFrameClause(java.util.List<LocationVariable> modHeaps,
java.util.Map<Term,Term> heapToAtPre,
ProgramVariable selfVar,
ImmutableList<ProgramVariable> paramVars,
Services services)
Deprecated.
|
protected Term |
InfFlowContractPO.buildFrameClause(java.util.List<LocationVariable> modHeaps,
java.util.Map<Term,Term> heapToAtPre,
ProgramVariable selfVar,
ImmutableList<ProgramVariable> paramVars,
Services services)
Deprecated.
|
protected Term |
BlockExecutionPO.buildFrameClause(java.util.List<LocationVariable> modHeaps,
java.util.Map<Term,Term> heapToAtPre,
ProgramVariable selfVar,
ImmutableList<ProgramVariable> paramVars,
Services services)
Deprecated.
|
protected Term |
SymbolicExecutionPO.buildFrameClause(java.util.List<LocationVariable> modHeaps,
java.util.Map<Term,Term> heapToAtPre,
ProgramVariable selfVar,
ImmutableList<ProgramVariable> paramVars,
Services services)
Deprecated.
|
protected ImmutableList<StatementBlock> |
LoopInvExecutionPO.buildOperationBlocks(ImmutableList<LocationVariable> formalParVars,
ProgramVariable selfVar,
ProgramVariable resultVar,
Services services)
Deprecated.
|
protected ImmutableList<StatementBlock> |
InfFlowContractPO.buildOperationBlocks(ImmutableList<LocationVariable> formalParVars,
ProgramVariable selfVar,
ProgramVariable resultVar,
Services services)
Deprecated.
|
protected ImmutableList<StatementBlock> |
BlockExecutionPO.buildOperationBlocks(ImmutableList<LocationVariable> formalParVars,
ProgramVariable selfVar,
ProgramVariable resultVar,
Services services)
Deprecated.
|
protected ImmutableList<StatementBlock> |
SymbolicExecutionPO.buildOperationBlocks(ImmutableList<LocationVariable> formalParVars,
ProgramVariable selfVar,
ProgramVariable resultVar,
Services services)
Deprecated.
|
protected Term |
LoopInvExecutionPO.generateMbyAtPreDef(ProgramVariable selfVar,
ImmutableList<ProgramVariable> paramVars,
Services services)
Deprecated.
|
protected Term |
InfFlowContractPO.generateMbyAtPreDef(ProgramVariable selfVar,
ImmutableList<ProgramVariable> paramVars,
Services services)
Deprecated.
|
protected Term |
BlockExecutionPO.generateMbyAtPreDef(ProgramVariable selfVar,
ImmutableList<ProgramVariable> paramVars,
Services services)
Deprecated.
|
protected Term |
SymbolicExecutionPO.generateMbyAtPreDef(ProgramVariable selfVar,
ImmutableList<ProgramVariable> paramVars,
Services services)
Deprecated.
|
protected Term |
LoopInvExecutionPO.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 | 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 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.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 | Method and Description |
---|---|
ProgramVariable |
Recoder2KeYConverter.convert(VariableReference vr)
converts a recoder variable reference.
|
protected ProgramVariable |
CreateArrayMethodBuilder.find(java.lang.String name,
ImmutableList<Field> fields)
retrieves a field with the given name out of the list
|
protected ProgramVariable |
CreateArrayMethodBuilder.findInObjectFields(java.lang.String name) |
ProgramVariable |
JavaInfo.getArrayLength()
returns the length attribute for arrays
|
ProgramVariable |
JavaInfo.getAttribute(java.lang.String fullyQualifiedName)
returns the programvariable for the specified attribute.
|
ProgramVariable |
JavaInfo.getAttribute(java.lang.String name,
KeYJavaType classType)
returns the program variable representing the attribute of the given
name declared locally in class classType
|
ProgramVariable |
JavaInfo.getAttribute(java.lang.String attributeName,
Sort s)
returns an attribute named attributeName declared locally
in object type s
|
ProgramVariable |
JavaInfo.getAttribute(java.lang.String programName,
java.lang.String qualifiedClassName)
returns the programvariable for the specified attribute declared in
the specified class
|
ProgramVariable |
JavaInfo.getCanonicalFieldProgramVariable(java.lang.String fieldName,
KeYJavaType kjt) |
ProgramVariable |
JavaInfo.getInvProgramVar()
Returns the special program variable symbol
<inv>
which stands for the class invariant of an object. |
static ProgramVariable |
KeYJavaASTFactory.localVariable(ProgramElementName name,
KeYJavaType kjt)
create a local variable
|
static ProgramVariable |
KeYJavaASTFactory.localVariable(Services services,
java.lang.String name,
KeYJavaType type)
Create a local variable with a unique name.
|
static ProgramVariable |
KeYJavaASTFactory.localVariable(java.lang.String name,
KeYJavaType kjt)
create a local variable
|
ProgramVariable |
JavaInfo.lookupVisibleAttribute(java.lang.String programName,
KeYJavaType classType)
looks up for a field of the given program name
visible in the specified class type belonging to the type
or one of its supertypes
|
Modifier and Type | Method and Description |
---|---|
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
|
Modifier and Type | Method and Description |
---|---|
static CopyAssignment |
KeYJavaASTFactory.assignArrayField(ProgramVariable variable,
ReferencePrefix array,
Expression index)
Create a statement that assigns an array element to a variable.
|
static Expression |
KeYJavaASTFactory.attribute(ReferencePrefix prefix,
ProgramVariable field)
creates an attribute access
prefix.field |
static FieldReference |
KeYJavaASTFactory.fieldReference(ReferencePrefix prefix,
ProgramVariable field)
Create a field access.
|
protected StatementBlock |
CreateArrayMethodBuilder.getCreateArrayBody(TypeReference arrayRef,
ProgramVariable paramLength) |
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.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,
ProgramVariable[] args,
KeYJavaType context)
returns the program method defined in the KeYJavaType of the program
variable clv, with the name m, and the KeYJavaTypes of the given array
of program variables as signatures.
|
static IGuard |
KeYJavaASTFactory.lessThanArrayLengthGuard(JavaInfo model,
ProgramVariable variable,
ReferencePrefix array)
Create a condition that compares a variable and an array length using the
less than operator.
|
static MethodBodyStatement |
KeYJavaASTFactory.methodBody(JavaInfo model,
ProgramVariable result,
ReferencePrefix reference,
KeYJavaType classType,
java.lang.String methodName,
ProgramVariable[] arguments)
Create a method body shortcut.
|
static MethodBodyStatement |
KeYJavaASTFactory.methodBody(JavaInfo model,
ProgramVariable result,
ReferencePrefix reference,
KeYJavaType classType,
java.lang.String methodName,
ProgramVariable[] arguments)
Create a method body shortcut.
|
static MethodBodyStatement |
KeYJavaASTFactory.methodBody(ProgramVariable result,
ReferencePrefix reference,
IProgramMethod method,
Expression[] arguments)
Create a method body shortcut.
|
static MethodBodyStatement |
KeYJavaASTFactory.methodBody(ProgramVariable result,
ReferencePrefix reference,
IProgramMethod method,
ImmutableArray<Expression> arguments)
Create a method body shortcut.
|
static IForUpdates |
KeYJavaASTFactory.postIncrementForUpdates(ProgramVariable variable)
Create a loop update expression that post increments a given variable.
|
void |
PrettyPrinter.printProgramVariable(ProgramVariable x) |
Modifier and Type | Method and Description |
---|---|
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.
|
Modifier and Type | Method and Description |
---|---|
static int |
EnumClassDeclaration.indexOf(ProgramVariable attribute) |
Constructor and Description |
---|
FieldSpecification(ExtList children,
ProgramVariable var,
int dimensions,
Type type)
Field specification.
|
FieldSpecification(ProgramVariable var) |
FieldSpecification(ProgramVariable var,
Expression init,
Type type)
Field specification.
|
FieldSpecification(ProgramVariable var,
int dimensions,
Expression init,
Type type)
Field specification.
|
FieldSpecification(ProgramVariable var,
Type type)
Field specification.
|
ImplicitFieldSpecification(ProgramVariable var)
Implicit Field specification.
|
ImplicitFieldSpecification(ProgramVariable var,
Type type)
Implicit Field specification.
|
Modifier and Type | Field and Description |
---|---|
protected ProgramVariable |
VariableReference.variable |
Modifier and Type | Method and Description |
---|---|
ProgramVariable |
VariableReference.getProgramVariable() |
Constructor and Description |
---|
FieldReference(ProgramVariable pv,
ReferencePrefix prefix) |
FieldReference(ProgramVariable pv,
ReferencePrefix prefix,
PositionInfo pi) |
VariableReference(ProgramVariable variable) |
VariableReference(ProgramVariable variable,
PositionInfo pi) |
Modifier and Type | Field and Description |
---|---|
protected java.util.Map<ProgramVariable,ProgramVariable> |
ProgVarReplaceVisitor.replaceMap
stores the program variables to be replaced as keys and the new program
variables as values
|
protected java.util.Map<ProgramVariable,ProgramVariable> |
ProgVarReplaceVisitor.replaceMap
stores the program variables to be replaced as keys and the new program
variables as values
|
Modifier and Type | Method and Description |
---|---|
static LocationVariable |
ProgVarReplaceVisitor.copy(ProgramVariable pv) |
static LocationVariable |
ProgVarReplaceVisitor.copy(ProgramVariable pv,
java.lang.String postFix) |
void |
ProgVarReplaceVisitor.performActionOnProgramVariable(ProgramVariable pv) |
void |
Visitor.performActionOnProgramVariable(ProgramVariable x) |
void |
JavaASTVisitor.performActionOnProgramVariable(ProgramVariable x) |
Constructor and Description |
---|
OuterBreakContinueAndReturnReplacer(StatementBlock block,
java.lang.Iterable<Label> alwaysInnerLabels,
Label breakOutLabel,
java.util.Map<Label,ProgramVariable> breakFlags,
java.util.Map<Label,ProgramVariable> continueFlags,
ProgramVariable returnFlag,
ProgramVariable returnValue,
ProgramVariable exception,
Services services) |
Constructor and Description |
---|
OuterBreakContinueAndReturnReplacer(StatementBlock block,
java.lang.Iterable<Label> alwaysInnerLabels,
Label breakOutLabel,
java.util.Map<Label,ProgramVariable> breakFlags,
java.util.Map<Label,ProgramVariable> continueFlags,
ProgramVariable returnFlag,
ProgramVariable returnValue,
ProgramVariable exception,
Services services) |
OuterBreakContinueAndReturnReplacer(StatementBlock block,
java.lang.Iterable<Label> alwaysInnerLabels,
Label breakOutLabel,
java.util.Map<Label,ProgramVariable> breakFlags,
java.util.Map<Label,ProgramVariable> continueFlags,
ProgramVariable returnFlag,
ProgramVariable returnValue,
ProgramVariable exception,
Services services) |
ProgVarReplaceVisitor(ProgramElement st,
java.util.Map<ProgramVariable,ProgramVariable> map,
boolean replaceall,
Services services)
creates a visitor that replaces the program variables in the given
statement
|
ProgVarReplaceVisitor(ProgramElement st,
java.util.Map<ProgramVariable,ProgramVariable> map,
boolean replaceall,
Services services)
creates a visitor that replaces the program variables in the given
statement
|
ProgVarReplaceVisitor(ProgramElement st,
java.util.Map<ProgramVariable,ProgramVariable> map,
Services services)
creates a visitor that replaces the program variables in the given
statement by new ones with the same name
|
ProgVarReplaceVisitor(ProgramElement st,
java.util.Map<ProgramVariable,ProgramVariable> map,
Services services)
creates a visitor that replaces the program variables in the given
statement by new ones with the same name
|
Modifier and Type | Field and Description |
---|---|
protected java.util.HashMap<ProgramVariable,ProgramVariable> |
VariableNamer.map |
protected java.util.HashMap<ProgramVariable,ProgramVariable> |
VariableNamer.map |
protected java.util.HashMap<ProgramVariable,ProgramVariable> |
VariableNamer.renamingHistory |
protected java.util.HashMap<ProgramVariable,ProgramVariable> |
VariableNamer.renamingHistory |
Modifier and Type | Method and Description |
---|---|
abstract ProgramVariable |
VariableNamer.rename(ProgramVariable var,
Goal goal,
PosInOccurrence posOfFind)
intended to be called when symbolically executing a variable declaration;
resolves any naming conflicts between the new variable and other global
variables by renaming the new variable and / or other variables
|
ProgramVariable |
InnerVariableNamer.rename(ProgramVariable var,
Goal goal,
PosInOccurrence posOfFind) |
Modifier and Type | Method and Description |
---|---|
java.util.HashMap<ProgramVariable,ProgramVariable> |
VariableNamer.getRenamingMap() |
java.util.HashMap<ProgramVariable,ProgramVariable> |
VariableNamer.getRenamingMap() |
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.
|
Modifier and Type | Method and Description |
---|---|
Term |
TermBuilder.reachableValue(ProgramVariable pv) |
abstract ProgramVariable |
VariableNamer.rename(ProgramVariable var,
Goal goal,
PosInOccurrence posOfFind)
intended to be called when symbolically executing a variable declaration;
resolves any naming conflicts between the new variable and other global
variables by renaming the new variable and / or other variables
|
ProgramVariable |
InnerVariableNamer.rename(ProgramVariable var,
Goal goal,
PosInOccurrence posOfFind) |
ImmutableList<Term> |
TermBuilder.var(ProgramVariable... vs) |
Term |
TermBuilder.var(ProgramVariable v) |
Modifier and Type | Method and Description |
---|---|
ImmutableList<Term> |
TermBuilder.var(java.lang.Iterable<ProgramVariable> vs) |
protected java.lang.Iterable<ProgramElementName> |
VariableNamer.wrapGlobals(ImmutableSet<ProgramVariable> globals)
creates a Globals object for use with other internal methods
|
Modifier and Type | Method and Description |
---|---|
ProgramVariable |
BlockContractValidityTermLabel.getChild(int i)
Retrieves the i-th parameter object of this term label.
|
ProgramVariable |
BlockContractValidityTermLabel.getExceptionVariable()
retrieves the original exception variable as found in the local variable declaration statement
|
Constructor and Description |
---|
BlockContractValidityTermLabel(ProgramVariable exceptionVariable)
Constructor.
|
Modifier and Type | Class and Description |
---|---|
class |
LocationVariable
This class represents proper program variables, which are not program
constants.
|
class |
ProgramConstant
This class represents currently only static final fields initialised with
a compile time constant.
|
Modifier and Type | Method and Description |
---|---|
void |
LogicPrinter.printProgramVariable(ProgramVariable pv)
Pretty-Prints a ProgramVariable in the logic, not in Java blocks.
|
Modifier and Type | Method and Description |
---|---|
void |
Goal.addProgramVariable(ProgramVariable pv) |
Constructor and Description |
---|
ProgVarReplacer(java.util.Map<ProgramVariable,ProgramVariable> map,
Services services)
creates a ProgVarReplacer that replaces program variables as specified
by the map parameter
|
ProgVarReplacer(java.util.Map<ProgramVariable,ProgramVariable> map,
Services services)
creates a ProgVarReplacer that replaces program variables as specified
by the map parameter
|
Modifier and Type | Method and Description |
---|---|
protected void |
ProgramVariableReferencesAnalyst.listReferences(Node node,
ProgramElement pe,
ProgramVariable arrayLength,
java.util.LinkedHashSet<IProofReference<?>> toFill,
boolean includeExpressionContainer)
Extracts the proof references recursive.
|
Modifier and Type | Field and Description |
---|---|
ProgramVariable |
WellDefinednessPO.Variables.exception |
ProgramVariable |
WellDefinednessPO.Variables.heapAtPre |
ProgramVariable |
WellDefinednessPO.Variables.result |
ProgramVariable |
WellDefinednessPO.Variables.self |
Modifier and Type | Field and Description |
---|---|
java.util.Map<LocationVariable,ProgramVariable> |
WellDefinednessPO.Variables.atPres |
ImmutableList<ProgramVariable> |
WellDefinednessPO.Variables.params |
Modifier and Type | Method and Description |
---|---|
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 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.ensureUninterpretedPredicateExists(ImmutableList<ProgramVariable> paramVars,
ImmutableList<LocationVariable> formalParamVars,
ProgramVariable exceptionVar,
java.lang.String name,
Services services)
|
protected abstract Term |
AbstractOperationPO.generateMbyAtPreDef(ProgramVariable selfVar,
ImmutableList<ProgramVariable> paramVars,
Services services) |
protected Term |
FunctionalOperationContractPO.generateMbyAtPreDef(ProgramVariable selfVar,
ImmutableList<ProgramVariable> paramVars,
Services services) |
protected Term |
AbstractPO.generateSelfCreated(java.util.List<LocationVariable> heaps,
IProgramMethod pm,
ProgramVariable selfVar,
Services services)
Generates the general assumption that self is created.
|
protected Term |
AbstractPO.generateSelfExactType(IProgramMethod pm,
ProgramVariable selfVar,
KeYJavaType selfKJT)
Generates the general assumption which defines the type of self.
|
protected Term |
AbstractPO.generateSelfNotNull(IProgramMethod pm,
ProgramVariable selfVar)
Generates the general assumption that self is not null.
|
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 void |
AbstractPO.register(ProgramVariable pv,
Services services) |
Modifier and Type | Method and Description |
---|---|
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 Term |
AbstractOperationPO.buildProgramTerm(ImmutableList<ProgramVariable> paramVars,
ImmutableList<LocationVariable> formalParamVars,
ProgramVariable selfVar,
ProgramVariable resultVar,
ProgramVariable exceptionVar,
java.util.Map<LocationVariable,LocationVariable> atPreVars,
Term postTerm,
ImmutableList<StatementBlock> sb,
Services services)
Creates the
Term which contains the modality including
the complete program to execute. |
protected Term |
AbstractOperationPO.buildUpdate(ImmutableList<ProgramVariable> paramVars,
ImmutableList<LocationVariable> formalParamVars,
java.util.Map<LocationVariable,LocationVariable> atPreVars,
Services services)
Builds the initial updates.
|
protected Term |
FunctionalOperationContractPO.buildUpdate(ImmutableList<ProgramVariable> paramVars,
ImmutableList<LocationVariable> formalParamVars,
java.util.Map<LocationVariable,LocationVariable> atPreVars,
Services services)
Builds the initial updates.
|
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 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 void |
AbstractPO.register(ImmutableList<ProgramVariable> pvs,
Services services) |
Constructor and Description |
---|
Variables(ProgramVariable self,
ProgramVariable result,
ProgramVariable exception,
java.util.Map<LocationVariable,ProgramVariable> atPres,
ImmutableList<ProgramVariable> params,
LocationVariable heap,
Term anonHeap) |
Constructor and Description |
---|
Variables(ProgramVariable self,
ProgramVariable result,
ProgramVariable exception,
java.util.Map<LocationVariable,ProgramVariable> atPres,
ImmutableList<ProgramVariable> params,
LocationVariable heap,
Term anonHeap) |
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 |
---|---|
static ProgramVariable |
UseOperationContractRule.computeResultVar(UseOperationContractRule.Instantiation inst,
TermServices services)
Computes the result variable for this instantiation.
|
protected static ProgramVariable |
AbstractAuxiliaryContractRule.createLocalVariable(java.lang.String nameBase,
KeYJavaType type,
Services services) |
ProgramVariable |
AbstractBlockContractRule.BlockContractHint.getExceptionalVariable() |
Modifier and Type | Method and Description |
---|---|
static AbstractBlockContractRule.BlockContractHint |
AbstractBlockContractRule.BlockContractHint.createValidityBranchHint(ProgramVariable excVar) |
protected static void |
AbstractAuxiliaryContractRule.register(ProgramVariable pv,
Services services)
Adds
pv to the sevices ' program variable namespace. |
protected AbstractBlockContractRule.InfFlowValidityData |
AbstractBlockContractRule.setUpInfFlowValidityGoal(Goal infFlowGoal,
BlockContract contract,
java.util.Map<LocationVariable,Function> anonymisationHeaps,
Services services,
AuxiliaryContract.Variables variables,
ProgramVariable exceptionParameter,
java.util.List<LocationVariable> heaps,
ImmutableSet<ProgramVariable> localInVariables,
ImmutableSet<ProgramVariable> localOutVariables,
BlockContractInternalBuiltInRuleApp application,
AbstractAuxiliaryContractRule.Instantiation instantiation) |
Term |
AuxiliaryContractBuilders.GoalsConfigurator.setUpLoopValidityGoal(Goal goal,
LoopContract contract,
Term context,
Term remember,
Term rememberNext,
java.util.Map<LocationVariable,Function> anonOutHeaps,
java.util.Map<LocationVariable,Term> modifiesClauses,
Term[] assumptions,
Term decreasesCheck,
Term[] postconditions,
Term[] postconditionsNext,
ProgramVariable exceptionParameter,
AuxiliaryContract.Terms terms,
AuxiliaryContract.Variables nextVars) |
Term |
AuxiliaryContractBuilders.GoalsConfigurator.setUpValidityGoal(Goal goal,
Term[] updates,
Term[] assumptions,
Term[] postconditions,
ProgramVariable exceptionParameter,
AuxiliaryContract.Terms terms) |
Modifier and Type | Method and Description |
---|---|
Term |
AuxiliaryContractBuilders.ConditionsAndClausesBuilder.buildReachableCondition(ImmutableSet<ProgramVariable> variables) |
Term |
AuxiliaryContractBuilders.ConditionsAndClausesBuilder.buildReachableInCondition(ImmutableSet<ProgramVariable> localInVariables) |
Term |
AuxiliaryContractBuilders.ConditionsAndClausesBuilder.buildReachableOutCondition(ImmutableSet<ProgramVariable> localOutVariables) |
protected static AbstractLoopInvariantRule.AdditionalHeapTerms |
AbstractLoopInvariantRule.createAdditionalHeapTerms(Services services,
AbstractLoopInvariantRule.Instantiation inst,
java.util.List<LocationVariable> heapContext,
ImmutableSet<ProgramVariable> localOuts,
java.util.Map<LocationVariable,java.util.Map<Term,Term>> heapToBeforeLoop,
java.util.Map<LocationVariable,Term> atPres)
Prepare anon update, wellformed formula, frame condition and reachable
state formula.
|
protected static Term |
AbstractLoopInvariantRule.createBeforeLoopUpdate(Services services,
java.util.List<LocationVariable> heapContext,
ImmutableSet<ProgramVariable> localOuts,
java.util.Map<LocationVariable,java.util.Map<Term,Term>> heapToBeforeLoop)
Creates the "...Before_LOOP" update needed for the variant.
|
protected static Term |
AbstractAuxiliaryContractRule.createLocalAnonUpdate(ImmutableSet<ProgramVariable> localOuts,
Services services) |
protected static Term |
AbstractLoopInvariantRule.createLocalAnonUpdate(ImmutableSet<ProgramVariable> localOuts,
Services services)
Creates an update for the anonymization of all
ProgramVariable s
in localOuts. |
protected AbstractBlockContractRule.InfFlowValidityData |
AbstractBlockContractRule.setUpInfFlowValidityGoal(Goal infFlowGoal,
BlockContract contract,
java.util.Map<LocationVariable,Function> anonymisationHeaps,
Services services,
AuxiliaryContract.Variables variables,
ProgramVariable exceptionParameter,
java.util.List<LocationVariable> heaps,
ImmutableSet<ProgramVariable> localInVariables,
ImmutableSet<ProgramVariable> localOutVariables,
BlockContractInternalBuiltInRuleApp application,
AbstractAuxiliaryContractRule.Instantiation instantiation) |
protected AbstractBlockContractRule.InfFlowValidityData |
AbstractBlockContractRule.setUpInfFlowValidityGoal(Goal infFlowGoal,
BlockContract contract,
java.util.Map<LocationVariable,Function> anonymisationHeaps,
Services services,
AuxiliaryContract.Variables variables,
ProgramVariable exceptionParameter,
java.util.List<LocationVariable> heaps,
ImmutableSet<ProgramVariable> localInVariables,
ImmutableSet<ProgramVariable> localOutVariables,
BlockContractInternalBuiltInRuleApp application,
AbstractAuxiliaryContractRule.Instantiation instantiation) |
Term |
AuxiliaryContractBuilders.GoalsConfigurator.setUpWdGoal(Goal goal,
BlockContract contract,
Term update,
Term anonUpdate,
LocationVariable heap,
Function anonHeap,
ImmutableSet<ProgramVariable> localIns) |
Constructor and Description |
---|
BlockContractHint(java.lang.String description,
ProgramVariable excVar) |
ValidityProgramConstructor(java.lang.Iterable<Label> labels,
StatementBlock block,
AuxiliaryContract.Variables variables,
ProgramVariable exceptionParameter,
Services services) |
ValidityProgramConstructor(java.lang.Iterable<Label> labels,
StatementBlock block,
AuxiliaryContract.Variables variables,
ProgramVariable exceptionParameter,
Services services,
AuxiliaryContract.Variables alreadyDeclared) |
Modifier and Type | Method and Description |
---|---|
abstract java.util.LinkedHashMap<ProgramVariable,AbstractDomainElement> |
MergeWithLatticeAbstraction.getUserChoices() |
java.util.LinkedHashMap<ProgramVariable,AbstractDomainElement> |
MergeWithPredicateAbstraction.getUserChoices() |
Modifier and Type | Method and Description |
---|---|
MergeWithPredicateAbstraction |
MergeWithPredicateAbstractionFactory.instantiate(java.lang.Iterable<AbstractionPredicate> predicates,
java.lang.Class<? extends AbstractPredicateAbstractionLattice> latticeType,
java.util.LinkedHashMap<ProgramVariable,AbstractDomainElement> userChoices)
Creates a complete instance of
MergeWithPredicateAbstraction . |
Constructor and Description |
---|
MergeWithPredicateAbstraction(java.lang.Iterable<AbstractionPredicate> predicates,
java.lang.Class<? extends AbstractPredicateAbstractionLattice> latticeType,
java.util.Map<ProgramVariable,AbstractDomainElement> userChoices)
Creates a new instance of
MergeWithPredicateAbstraction . |
Modifier and Type | Field and Description |
---|---|
protected ProgramVariable |
MethodCall.pvar |
Modifier and Type | Method and Description |
---|---|
static ProgramVariable |
EvaluateArgs.evaluate(Expression e,
java.util.List<? super LocalVariableDeclaration> l,
Services services,
ExecutionContext ec)
TODO Comment.
|
protected ProgramVariable[] |
InitArray.evaluateInitializers(Statement[] p_stmnts,
NewArray p_creationExpression,
Services services)
The variable initializers have to be evaluated and assigned to
temporary variables (the initializers may itself be array
initializers, in which case valid creation expressions are
created by inserting the new-operator)
|
ProgramVariable |
EnhancedForElimination.getIndexVariable() |
ProgramVariable |
EnhancedForElimination.getIteratorVariable() |
ProgramVariable |
EnhancedForElimination.getValuesVariable() |
Modifier and Type | Method and Description |
---|---|
protected void |
InitArray.createArrayAssignments(int p_start,
Statement[] p_statements,
ProgramVariable[] p_initializers,
ReferencePrefix p_array,
NewArray p_creationExpression)
Convert the variable initializers to assignments to the array
elements (the initializers may itself be array initializers, in
which case valid creation expressions are created by inserting
the new-operator)
|
Constructor and Description |
---|
ConstructorCall(ProgramVariable pv,
New n)
Used to programmatically produce this statement.
|
PostWork(ProgramVariable pv)
Used to create this Java statement programmatically.
|
WhileInvariantTransformation(ProgramElement root,
ProgramElementName outerLabel,
ProgramElementName innerLabel,
ProgramVariable cont,
ProgramVariable exc,
ProgramVariable excParam,
ProgramVariable thrownException,
ProgramVariable brk,
ProgramVariable rtrn,
ProgramVariable returnExpr,
java.util.LinkedList<de.uka.ilkd.key.rule.metaconstruct.BreakToBeReplaced> breakList,
Services services)
creates the WhileLoopTransformation for the transformation mode
|
Modifier and Type | Method and Description |
---|---|
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) |
Modifier and Type | Method and Description |
---|---|
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.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.generateContractAxiomTaclets(Name name,
Term originalPre,
Term originalPost,
Term originalMby,
KeYJavaType kjt,
IObserverFunction target,
java.util.List<? extends ProgramVariable> heaps,
ProgramVariable originalSelfVar,
ProgramVariable originalResultVar,
java.util.Map<LocationVariable,ProgramVariable> atPreVars,
ImmutableList<ProgramVariable> originalParamVars,
ImmutableSet<Pair<Sort,IObserverFunction>> toLimit,
boolean satisfiabilityGuard,
TermServices services) |
ImmutableSet<Taclet> |
TacletGenerator.generateFunctionalRepresentsTaclets(Name name,
Term originalPreTerm,
Term originalRepresentsTerm,
KeYJavaType kjt,
IObserverFunction target,
java.util.List<? extends ProgramVariable> heaps,
ProgramVariable self,
ImmutableList<ProgramVariable> paramVars,
java.util.Map<LocationVariable,ProgramVariable> atPreVars,
ImmutableSet<Pair<Sort,IObserverFunction>> toLimit,
boolean satisfiability,
Services services) |
ImmutableSet<Taclet> |
TacletGenerator.generateFunctionalRepresentsTaclets(Name name,
Term originalPreTerm,
Term originalRepresentsTerm,
KeYJavaType kjt,
IObserverFunction target,
java.util.List<? extends ProgramVariable> heaps,
ProgramVariable self,
ImmutableList<ProgramVariable> paramVars,
java.util.Map<LocationVariable,ProgramVariable> atPreVars,
ImmutableSet<Pair<Sort,IObserverFunction>> toLimit,
boolean satisfiability,
Services services) |
ImmutableSet<Taclet> |
TacletGenerator.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.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.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) |
Modifier and Type | Field and Description |
---|---|
ProgramVariable |
Contract.OriginalVariables.exception |
ProgramVariable |
AuxiliaryContract.Variables.exception
Exception variable to set when the block terminates by an uncaught
throw
statement. |
ProgramVariable |
Contract.OriginalVariables.result |
ProgramVariable |
AuxiliaryContract.Variables.result
Result variable to set when the block terminates by a
return statement. |
ProgramVariable |
AuxiliaryContract.Variables.returnFlag
Boolean flag that is set to
true when the block terminates by a return
statement. |
ProgramVariable |
Contract.OriginalVariables.self |
ProgramVariable |
AuxiliaryContract.Variables.self
self |
Modifier and Type | Field and Description |
---|---|
java.util.Map<LocationVariable,ProgramVariable> |
Contract.OriginalVariables.atPres |
java.util.Map<Label,ProgramVariable> |
AuxiliaryContract.Variables.breakFlags
Boolean flags that are set to
true when the block terminates by a
break label; statement with the specified label. |
java.util.Map<Label,ProgramVariable> |
AuxiliaryContract.Variables.continueFlags
Boolean flags that are set to
true when the block terminates by a
continue label; statement with the specified label. |
ImmutableList<ProgramVariable> |
Contract.OriginalVariables.params |
Modifier and Type | Method and Description |
---|---|
ProgramVariable |
LoopContract.getIndexVariable() |
ProgramVariable |
LoopContractImpl.getIndexVariable() |
ProgramVariable |
LoopContract.getValuesVariable() |
ProgramVariable |
LoopContractImpl.getValuesVariable() |
Modifier and Type | Method and Description |
---|---|
protected java.util.Map<ProgramVariable,ProgramVariable> |
AbstractAuxiliaryContractImpl.createReplacementMap(AuxiliaryContract.Variables newVariables,
Services services) |
protected java.util.Map<ProgramVariable,ProgramVariable> |
AbstractAuxiliaryContractImpl.createReplacementMap(AuxiliaryContract.Variables newVariables,
Services services) |
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.
|
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.
|
Modifier and Type | Method and Description |
---|---|
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.
|
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(KeYJavaType kjt,
LocationVariable targetHeap,
Triple<IObserverFunction,Term,Term> dep,
ProgramVariable selfVar) |
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) |
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.
|
SequentFormula |
StatementWellDefinedness.generateSequent(ProgramVariable self,
LocationVariable heap,
Term anonHeap,
ImmutableSet<ProgramVariable> ps,
Term leadingUpdate,
Term localAnonUpdate,
Services services)
This is where the proof sequent is built, however with a smaller set of variables,
due to the nature of the jml statement.
|
SequentFormula |
StatementWellDefinedness.generateSequent(ProgramVariable self,
ProgramVariable exception,
ProgramVariable result,
LocationVariable heap,
ProgramVariable heapAtPre,
Term anonHeap,
ImmutableSet<ProgramVariable> ps,
Term leadingUpdate,
Term localAnonUpdate,
Services services)
This is where the proof sequent is built.
|
Term |
FunctionalAuxiliaryContract.getAccessible(ProgramVariable heap) |
Term |
FunctionalOperationContractImpl.getAccessible(ProgramVariable heap) |
Term |
InformationFlowContractImpl.getAccessible(ProgramVariable heap) |
Term |
DependencyContractImpl.getAccessible(ProgramVariable heap) |
Term |
WellDefinednessCheck.getAccessible(ProgramVariable heap) |
Term |
Contract.getAccessible(ProgramVariable heap) |
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 |
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.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 |
AbstractAuxiliaryContractImpl.getFreePrecondition(LocationVariable heap,
ProgramVariable self,
java.util.Map<LocationVariable,LocationVariable> atPres,
Services services) |
Term |
AuxiliaryContract.getFreePrecondition(LocationVariable heap,
ProgramVariable self,
java.util.Map<LocationVariable,LocationVariable> atPres,
Services services) |
Term |
FunctionalAuxiliaryContract.getMby(ProgramVariable selfVar,
ImmutableList<ProgramVariable> paramVars,
Services services) |
Term |
FunctionalOperationContractImpl.getMby(ProgramVariable selfVar,
ImmutableList<ProgramVariable> paramVars,
Services services) |
Term |
InformationFlowContractImpl.getMby(ProgramVariable selfVar,
ImmutableList<ProgramVariable> paramVars,
Services services)
Deprecated.
|
Term |
DependencyContractImpl.getMby(ProgramVariable selfVar,
ImmutableList<ProgramVariable> paramVars,
Services services) |
Term |
WellDefinednessCheck.getMby(ProgramVariable selfVar,
ImmutableList<ProgramVariable> paramVars,
Services services)
Deprecated.
|
Term |
Contract.getMby(ProgramVariable selfVar,
ImmutableList<ProgramVariable> paramVars,
Services services)
Returns the measured_by clause of the contract.
|
Term |
AbstractAuxiliaryContractImpl.getMby(ProgramVariable selfVar,
Services services) |
Term |
AuxiliaryContract.getMby(ProgramVariable selfVar,
Services services) |
Term |
FunctionalOperationContractImpl.getMod(LocationVariable heap,
ProgramVariable selfVar,
ImmutableList<ProgramVariable> paramVars,
Services services) |
Term |
OperationContract.getMod(LocationVariable heapVar,
ProgramVariable selfVar,
ImmutableList<ProgramVariable> paramVars,
Services services)
Returns the modifies clause of the contract.
|
Term |
AbstractAuxiliaryContractImpl.getModifiesClause(LocationVariable heap,
ProgramVariable self,
Services services) |
Term |
AuxiliaryContract.getModifiesClause(LocationVariable heap,
ProgramVariable self,
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 |
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 |
AbstractAuxiliaryContractImpl.getPrecondition(LocationVariable heap,
ProgramVariable self,
java.util.Map<LocationVariable,LocationVariable> atPres,
Services services) |
Term |
AuxiliaryContract.getPrecondition(LocationVariable heap,
ProgramVariable self,
java.util.Map<LocationVariable,LocationVariable> atPres,
Services services) |
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 |
WellDefinednessCheck.getUpdates(Term mod,
LocationVariable heap,
ProgramVariable heapAtPre,
Term anonHeap,
TermServices services)
Gets the necessary updates applicable to the post-condition
|
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.
|
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(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(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) |
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) |
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,
IProgramMethod pm,
boolean terminates,
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> accessibles,
java.util.Map<LocationVariable,java.lang.Boolean> hasMod,
ProgramVariableCollection pv)
Creates a new functional operation contract.
|
FunctionalOperationContract |
ContractFactory.func(java.lang.String baseName,
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> accessibles,
java.util.Map<LocationVariable,java.lang.Boolean> hasMod,
ProgramVariableCollection progVars,
boolean toBeSaved,
boolean transaction)
Creates a new functional operation contract.
|
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.
|
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.
|
SequentFormula |
StatementWellDefinedness.generateSequent(ProgramVariable self,
LocationVariable heap,
Term anonHeap,
ImmutableSet<ProgramVariable> ps,
Term leadingUpdate,
Term localAnonUpdate,
Services services)
This is where the proof sequent is built, however with a smaller set of variables,
due to the nature of the jml statement.
|
SequentFormula |
StatementWellDefinedness.generateSequent(ProgramVariable self,
ProgramVariable exception,
ProgramVariable result,
LocationVariable heap,
ProgramVariable heapAtPre,
Term anonHeap,
ImmutableSet<ProgramVariable> ps,
Term leadingUpdate,
Term localAnonUpdate,
Services services)
This is where the proof sequent is built.
|
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 |
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 |
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 |
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 |
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 |
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 |
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 |
FunctionalOperationContractImpl.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,
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 |
FunctionalOperationContract.getFreePost(LocationVariable heap,
ProgramVariable selfVar,
ImmutableList<ProgramVariable> paramVars,
ProgramVariable resultVar,
ProgramVariable excVar,
java.util.Map<LocationVariable,? extends ProgramVariable> atPreVars,
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 |
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 |
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 |
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 |
OperationContract.getFreePre(LocationVariable heap,
ProgramVariable selfVar,
ImmutableList<ProgramVariable> paramVars,
java.util.Map<LocationVariable,? extends ProgramVariable> atPreVars,
Services services) |
Term |
FunctionalAuxiliaryContract.getMby(ProgramVariable selfVar,
ImmutableList<ProgramVariable> paramVars,
Services services) |
Term |
FunctionalOperationContractImpl.getMby(ProgramVariable selfVar,
ImmutableList<ProgramVariable> paramVars,
Services services) |
Term |
InformationFlowContractImpl.getMby(ProgramVariable selfVar,
ImmutableList<ProgramVariable> paramVars,
Services services)
Deprecated.
|
Term |
DependencyContractImpl.getMby(ProgramVariable selfVar,
ImmutableList<ProgramVariable> paramVars,
Services services) |
Term |
WellDefinednessCheck.getMby(ProgramVariable selfVar,
ImmutableList<ProgramVariable> paramVars,
Services services)
Deprecated.
|
Term |
Contract.getMby(ProgramVariable selfVar,
ImmutableList<ProgramVariable> paramVars,
Services services)
Returns the measured_by clause of the contract.
|
Term |
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.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(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 |
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 |
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 |
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 |
FunctionalAuxiliaryContract.getPre(java.util.List<LocationVariable> heapContext,
ProgramVariable selfVar,
ImmutableList<ProgramVariable> paramVars,
java.util.Map<LocationVariable,? extends ProgramVariable> atPreVars,
Services services) |
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 |
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 |
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 |
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 |
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 |
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 |
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 |
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 |
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 |
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 |
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 |
Contract.getPre(LocationVariable heap,
ProgramVariable selfVar,
ImmutableList<ProgramVariable> paramVars,
java.util.Map<LocationVariable,? extends ProgramVariable> atPreVars,
Services services)
Returns the precondition of the contract.
|
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.
|
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 |
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 |
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
|
Constructor and Description |
---|
ClassAxiomImpl(java.lang.String name,
KeYJavaType kjt,
VisibilityModifier visibility,
Term rep,
ProgramVariable selfVar) |
ClassAxiomImpl(java.lang.String name,
java.lang.String displayName,
KeYJavaType kjt,
VisibilityModifier visibility,
Term rep,
ProgramVariable selfVar) |
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) |
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) |
Variables(ProgramVariable self,
java.util.Map<Label,ProgramVariable> breakFlags,
java.util.Map<Label,ProgramVariable> continueFlags,
ProgramVariable returnFlag,
ProgramVariable result,
ProgramVariable exception,
java.util.Map<LocationVariable,LocationVariable> remembranceHeaps,
java.util.Map<LocationVariable,LocationVariable> remembranceLocalVariables,
java.util.Map<LocationVariable,LocationVariable> outerRemembranceHeaps,
java.util.Map<LocationVariable,LocationVariable> outerRemembranceVariables,
TermServices services)
You should use
#create() instead of this constructor. |
Constructor and Description |
---|
BlockWellDefinedness(BlockContract block,
AuxiliaryContract.Variables variables,
ImmutableSet<ProgramVariable> params,
Services services)
Creates a contract to check well-definedness of a block contract
|
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,
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) |
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) |
LoopWellDefinedness(LoopSpecification inv,
ImmutableSet<ProgramVariable> params,
Services services) |
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
|
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,
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) |
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) |
Variables(ProgramVariable self,
java.util.Map<Label,ProgramVariable> breakFlags,
java.util.Map<Label,ProgramVariable> continueFlags,
ProgramVariable returnFlag,
ProgramVariable result,
ProgramVariable exception,
java.util.Map<LocationVariable,LocationVariable> remembranceHeaps,
java.util.Map<LocationVariable,LocationVariable> remembranceLocalVariables,
java.util.Map<LocationVariable,LocationVariable> outerRemembranceHeaps,
java.util.Map<LocationVariable,LocationVariable> outerRemembranceVariables,
TermServices services)
You should use
#create() instead of this constructor. |
Variables(ProgramVariable self,
java.util.Map<Label,ProgramVariable> breakFlags,
java.util.Map<Label,ProgramVariable> continueFlags,
ProgramVariable returnFlag,
ProgramVariable result,
ProgramVariable exception,
java.util.Map<LocationVariable,LocationVariable> remembranceHeaps,
java.util.Map<LocationVariable,LocationVariable> remembranceLocalVariables,
java.util.Map<LocationVariable,LocationVariable> outerRemembranceHeaps,
java.util.Map<LocationVariable,LocationVariable> outerRemembranceVariables,
TermServices services)
You should use
#create() instead of this constructor. |
Modifier and Type | Method and Description |
---|---|
ImmutableSet<MergeContract> |
JMLSpecExtractor.extractMergeContracts(IProgramMethod method,
MergePointStatement mps,
ImmutableList<ProgramVariable> methodParams) |
Modifier and Type | Field and Description |
---|---|
ProgramVariable |
ProgramVariableCollection.excVar
exception |
ProgramVariable |
ProgramVariableCollection.resultVar
result |
ProgramVariable |
ProgramVariableCollection.selfVar
self |
Modifier and Type | Field and Description |
---|---|
java.util.Map<ProgramVariable,Term> |
JMLSpecFactory.ContractClauses.accessibles |
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.
|
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 |
---|---|
SLExpression |
JmlTermFactory.commentary(java.lang.String desc,
ProgramVariable selfVar,
ProgramVariable resultVar,
ImmutableList<ProgramVariable> paramVars,
Term heapAtPre) |
JmlIO |
JmlIO.exceptionVariable(ProgramVariable excVar)
Sets the variable that is used to store exceptions.
|
JmlIO |
JmlIO.resultVariable(ProgramVariable resultVar)
Sets the variable representing
\result . |
JmlIO |
JmlIO.selfVar(ProgramVariable selfVar)
Sets the variable representing the
this reference. |
Term |
JmlTermFactory.signals(Term result,
LogicVariable eVar,
ProgramVariable excVar,
KeYJavaType excType) |
Term |
JmlTermFactory.signalsOnly(ImmutableList<KeYJavaType> signalsonly,
ProgramVariable excVar) |
Modifier and Type | Method and Description |
---|---|
SLExpression |
JmlTermFactory.commentary(java.lang.String desc,
ProgramVariable selfVar,
ProgramVariable resultVar,
ImmutableList<ProgramVariable> paramVars,
Term heapAtPre) |
JmlIO |
JmlIO.parameters(ImmutableList<ProgramVariable> params)
Sets the current list of known parameter.
|
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.
|
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 |
---|---|
void |
SLResolverManager.putIntoTopLocalVariablesNamespace(ProgramVariable pv)
Puts a local variable into the topmost namespace on the stack
|
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.
|
Modifier and Type | Method and Description |
---|---|
ProgramVariable |
AbstractUpdateExtractor.ExtractLocationParameter.getProgramVariable()
Returns the
ProgramVariable or null if an array index is used instead. |
ProgramVariable |
AbstractUpdateExtractor.ExecutionVariableValuePair.getProgramVariable()
Returns the
ProgramVariable or null if an array index is used instead. |
Modifier and Type | Method and Description |
---|---|
protected boolean |
AbstractUpdateExtractor.isImplicitProgramVariable(ProgramVariable var)
Checks if the given
ProgramVariable is implicit. |
Constructor and Description |
---|
ExecutionVariableValuePair(ProgramVariable programVariable,
Term parent,
Term value,
Term condition,
boolean stateMember,
Node goalNode)
Constructor.
|
ExtractLocationParameter(ProgramVariable programVariable,
boolean stateMember)
Constructor.
|
ExtractLocationParameter(ProgramVariable programVariable,
Term parentTerm)
Constructor.
|
ExtractLocationParameter(ProgramVariable programVariable,
Term parentTerm,
boolean stateMember)
Constructor.
|
Modifier and Type | Method and Description |
---|---|
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 |
ProgramMethodPO.generateMbyAtPreDef(ProgramVariable selfVar,
ImmutableList<ProgramVariable> paramVars,
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 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 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.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 |
---|---|
ProgramVariable |
Access.getProgramVariable()
Returns the
ProgramVariable or null if an array index is accessed. |
Modifier and Type | Method and Description |
---|---|
java.util.Map<ProgramVariable,Term> |
AbstractSlicer.SequentInfo.getLocalValues()
Returns the local values.
|
Modifier and Type | Method and Description |
---|---|
protected void |
AbstractSlicer.analyzeUpdate(Term term,
Services services,
HeapLDT heapLDT,
java.util.Map<Location,java.util.SortedSet<Location>> aliases,
java.util.Map<ProgramVariable,Term> localValues,
ExecutionContext ec,
ReferencePrefix thisReference)
Recursive utility method used by
#analyzeUpdates(ImmutableList, Services, HeapLDT, Map) to analyze a given update. |
protected void |
AbstractSlicer.analyzeUpdates(ImmutableList<Term> updates,
Services services,
HeapLDT heapLDT,
java.util.Map<Location,java.util.SortedSet<Location>> aliases,
java.util.Map<ProgramVariable,Term> localValues,
ExecutionContext ec,
ReferencePrefix thisReference)
Utility method used by
#analyzeSequent(Node) to analyze the given updates. |
Constructor and Description |
---|
Access(ProgramVariable programVariable)
Constructor.
|
Constructor and Description |
---|
SequentInfo(java.util.Map<Location,java.util.SortedSet<Location>> aliases,
java.util.Map<ProgramVariable,Term> localValues,
ExecutionContext executionContext,
ReferencePrefix thisReference)
Constructor.
|
Modifier and Type | Method and Description |
---|---|
ProgramVariable |
AbstractConditionalBreakpoint.getSelfVar() |
Modifier and Type | Method and Description |
---|---|
ImmutableList<ProgramVariable> |
AbstractConditionalBreakpoint.getVarsForCondition() |
Modifier and Type | Method and Description |
---|---|
void |
AbstractConditionalBreakpoint.setSelfVar(ProgramVariable selfVar) |
Modifier and Type | Method and Description |
---|---|
void |
AbstractConditionalBreakpoint.setVarsForCondition(ImmutableList<ProgramVariable> varsForCondition) |
Modifier and Type | Method and Description |
---|---|
static ProgramVariable |
SymbolicExecutionUtil.getProgramVariable(Services services,
HeapLDT heapLDT,
Term locationTerm)
Returns the
ProgramVariable defined by the given Term . |
Modifier and Type | Method and Description |
---|---|
static ProgramVariable |
MiscTools.findActualVariable(ProgramVariable originalVar,
Node node)
Returns the actual variable for a given one (this means it returns the renamed variable).
|
static ProgramVariable |
MiscTools.getSelf(MethodFrame mf) |
Modifier and Type | Method and Description |
---|---|
static ImmutableSet<ProgramVariable> |
MiscTools.getLocalIns(ProgramElement pe,
Services services)
All variables read in the specified program element, excluding newly declared variables.
|
static ImmutableSet<ProgramVariable> |
MiscTools.getLocallyDeclaredVars(ProgramElement pe,
Services services)
All variables newly declared in the specified program element.
|
static ImmutableSet<ProgramVariable> |
MiscTools.getLocalOuts(ProgramElement pe,
Services services)
All variables changed in the specified program element, excluding newly declared variables.
|
static ImmutableSet<ProgramVariable> |
MiscTools.getLocalOutsAndDeclared(ProgramElement pe,
Services services)
All variables changed in the specified program element, including newly declared variables.
|
Modifier and Type | Method and Description |
---|---|
static ProgramVariable |
MiscTools.findActualVariable(ProgramVariable originalVar,
Node node)
Returns the actual variable for a given one (this means it returns the renamed variable).
|
Modifier and Type | Method and Description |
---|---|
static ImmutableList<Term> |
MiscTools.toTermList(java.lang.Iterable<ProgramVariable> list,
TermBuilder tb) |
Copyright © 2003-2019 The KeY-Project.