Package | Description |
---|---|
de.uka.ilkd.key.axiom_abstraction.predicateabstraction | |
de.uka.ilkd.key.gui |
This package contains classes forming the graphical user interface of KeY.
|
de.uka.ilkd.key.gui.mergerule.predicateabstraction | |
de.uka.ilkd.key.informationflow.po | |
de.uka.ilkd.key.java.expression.operator |
Elements of the Java syntax tree representing operators and operator-like
expressions.
|
de.uka.ilkd.key.java.statement |
Elements of the Java syntax tree representing pure statements.
|
de.uka.ilkd.key.java.visitor |
contains classes representing visitors traversing the tree
structure of Java programs.
|
de.uka.ilkd.key.ldt |
This package contains the "language data types" (LDTs) of KeY.
|
de.uka.ilkd.key.logic |
provides a representation for the term and sequent
structure.
|
de.uka.ilkd.key.logic.op |
contains the operators of
Term s. |
de.uka.ilkd.key.proof |
This package contains the core data structures of proofs, nodes, goals, as well
as machinery to deal with these data structures.
|
de.uka.ilkd.key.proof.init |
This package contains classes handling prover initialisation.
|
de.uka.ilkd.key.rule |
This package contains classes for implementing rules.
|
de.uka.ilkd.key.rule.merge | |
de.uka.ilkd.key.rule.metaconstruct |
contains classes representing the meta constructs of
Taclet s. |
de.uka.ilkd.key.rule.tacletbuilder | |
de.uka.ilkd.key.speclang |
This package contains the specification language frontends of KeY.
|
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.symbolic_execution | |
de.uka.ilkd.key.symbolic_execution.model.impl | |
de.uka.ilkd.key.symbolic_execution.po | |
de.uka.ilkd.key.symbolic_execution.strategy.breakpoint | |
de.uka.ilkd.key.util |
This package is a grab bag of miscellaneous useful code fragments.
|
de.uka.ilkd.key.util.mergerule |
Modifier and Type | Method and Description |
---|---|
Pair<LocationVariable,Term> |
AbstractionPredicate.getPredicateFormWithPlaceholder() |
Modifier and Type | Method and Description |
---|---|
static AbstractionPredicate |
AbstractionPredicate.create(Term predicate,
LocationVariable placeholder,
Services services)
Creates a new
AbstractionPredicate for the given predicate. |
Modifier and Type | Method and Description |
---|---|
static void |
DependencyContractCompletion.extractHeaps(java.util.List<LocationVariable> heapContext,
java.util.List<PosInOccurrence> steps,
DependencyContractCompletion.TermStringWrapper[] heaps,
LogicPrinter lp) |
LoopSpecification |
InvariantConfigurator.getLoopInvariant(LoopSpecification loopInv,
Services services,
boolean requiresVariant,
java.util.List<LocationVariable> heapContext)
Creates a Dialog.
|
Constructor and Description |
---|
AbstractionPredicatesChoiceDialog(Goal goal,
java.util.List<LocationVariable> differingLocVars)
Constructs a new
AbstractionPredicatesChoiceDialog . |
Modifier and Type | Method and Description |
---|---|
protected Term |
LoopInvExecutionPO.getGlobalDefs(LocationVariable heap,
Term heapTerm,
Term selfTerm,
ImmutableList<Term> paramTerms,
Services services) |
protected Term |
InfFlowContractPO.getGlobalDefs(LocationVariable heap,
Term heapTerm,
Term selfTerm,
ImmutableList<Term> paramTerms,
Services services) |
protected Term |
BlockExecutionPO.getGlobalDefs(LocationVariable heap,
Term heapTerm,
Term selfTerm,
ImmutableList<Term> paramTerms,
Services services) |
protected Term |
SymbolicExecutionPO.getGlobalDefs(LocationVariable heap,
Term heapTerm,
Term selfTerm,
ImmutableList<Term> paramTerms,
Services services) |
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.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.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.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 |
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 |
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 |
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 |
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 |
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 |
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 |
LoopInvExecutionPO.getPre(java.util.List<LocationVariable> modHeaps,
ProgramVariable selfVar,
ImmutableList<ProgramVariable> paramVars,
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 |
InfFlowContractPO.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 |
BlockExecutionPO.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.
|
protected Term |
SymbolicExecutionPO.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 |
---|---|
Term |
DLEmbeddedExpression.makeTerm(LocationVariable heap,
Term[] subs,
Services services) |
Modifier and Type | Method and Description |
---|---|
LocationVariable |
CatchAllStatement.getParam() |
Constructor and Description |
---|
CatchAllStatement(StatementBlock body,
LocationVariable param) |
MergePointStatement(LocationVariable identifier,
Comment[] comments) |
Modifier and Type | Method and Description |
---|---|
static LocationVariable |
ProgVarReplaceVisitor.copy(ProgramVariable pv) |
static LocationVariable |
ProgVarReplaceVisitor.copy(ProgramVariable pv,
java.lang.String postFix) |
Modifier and Type | Method and Description |
---|---|
java.util.LinkedHashSet<LocationVariable> |
UndeclaredProgramVariableCollector.getAllVariables()
Returns all used variables.
|
java.util.LinkedHashSet<LocationVariable> |
ProgramVariableCollector.result() |
java.util.LinkedHashSet<LocationVariable> |
UndeclaredProgramVariableCollector.result()
Returns the undeclared variables as result.
|
Modifier and Type | Method and Description |
---|---|
void |
ProgVarReplaceVisitor.performActionOnLocationVariable(LocationVariable x) |
void |
Visitor.performActionOnLocationVariable(LocationVariable variable) |
void |
JavaASTVisitor.performActionOnLocationVariable(LocationVariable x) |
void |
ProgramVariableCollector.performActionOnLocationVariable(LocationVariable x) |
void |
DeclarationProgramVariableCollector.performActionOnLocationVariable(LocationVariable x) |
Modifier and Type | Method and Description |
---|---|
LocationVariable |
HeapLDT.getHeap() |
LocationVariable |
HeapLDT.getHeapForName(Name name) |
LocationVariable |
HeapLDT.getPermissionHeap() |
LocationVariable |
HeapLDT.getSavedHeap() |
Modifier and Type | Method and Description |
---|---|
ImmutableList<LocationVariable> |
HeapLDT.getAllHeaps() |
Modifier and Type | Method and Description |
---|---|
Function |
HeapLDT.getFieldSymbolForPV(LocationVariable fieldPV,
Services services)
Given a "program variable" representing a field or a model field,
returns the function symbol representing the same field.
|
Modifier and Type | Method and Description |
---|---|
LocationVariable |
TermBuilder.excVar(IProgramMethod pm,
boolean makeNameUnique)
Creates a program variable for the thrown exception.
|
LocationVariable |
TermBuilder.excVar(java.lang.String name,
IProgramMethod pm,
boolean makeNameUnique)
Creates a program variable for the thrown exception.
|
LocationVariable |
TermBuilder.heapAtPreVar(java.lang.String baseName,
boolean makeNameUnique)
Creates a program variable for the atPre heap.
|
LocationVariable |
TermBuilder.heapAtPreVar(java.lang.String baseName,
Sort sort,
boolean makeNameUnique)
Creates a program variable for the atPre heap.
|
LocationVariable |
TermBuilder.resultVar(IProgramMethod pm,
boolean makeNameUnique)
Creates a program variable for the result.
|
LocationVariable |
TermBuilder.resultVar(java.lang.String name,
IProgramMethod pm,
boolean makeNameUnique)
Creates a program variable for the result with passed name.
|
LocationVariable |
TermBuilder.selfVar(IProgramMethod pm,
KeYJavaType kjt,
boolean makeNameUnique)
Creates a program variable for "self".
|
LocationVariable |
TermBuilder.selfVar(IProgramMethod pm,
KeYJavaType kjt,
boolean makeNameUnique,
java.lang.String postfix)
Creates a program variable for "self".
|
LocationVariable |
TermBuilder.selfVar(KeYJavaType kjt,
boolean makeNameUnique)
Creates a program variable for "self".
|
LocationVariable |
TermBuilder.selfVar(KeYJavaType kjt,
boolean makeNameUnique,
java.lang.String postfix)
Creates a program variable for "self".
|
Modifier and Type | Method and Description |
---|---|
Term |
TermBuilder.anonUpd(LocationVariable heap,
Term mod,
Term anonHeap) |
Term |
TermBuilder.dot(Sort asSort,
Term o,
LocationVariable field) |
Term |
TermBuilder.permissionsFor(LocationVariable permHeap,
LocationVariable regularHeap) |
Term |
TermBuilder.select(Sort asSort,
Term h,
Term o,
LocationVariable field)
Get the select expression for a location variabe representing the field.
|
Term |
TermBuilder.wellFormed(LocationVariable heap) |
Modifier and Type | Method and Description |
---|---|
ImmutableList<LocationVariable> |
ProgramMethod.collectParameters() |
ImmutableList<LocationVariable> |
IProgramMethod.collectParameters() |
ImmutableList<LocationVariable> |
ProgramSV.collectParameters() |
Modifier and Type | Method and Description |
---|---|
java.util.HashSet<LocationVariable> |
TermProgramVariableCollector.result() |
Modifier and Type | Field and Description |
---|---|
LocationVariable |
WellDefinednessPO.Variables.heap |
Modifier and Type | Field and Description |
---|---|
java.util.Map<LocationVariable,ProgramVariable> |
WellDefinednessPO.Variables.atPres |
Modifier and Type | Method and Description |
---|---|
protected LocationVariable |
AbstractOperationPO.getBaseHeap(Services services)
Returns the base heap.
|
protected LocationVariable |
AbstractOperationPO.getSavedHeap(Services services)
Returns the saved heap.
|
Modifier and Type | Method and Description |
---|---|
protected abstract Term |
AbstractOperationPO.getGlobalDefs(LocationVariable heap,
Term heapTerm,
Term selfTerm,
ImmutableList<Term> paramTerms,
Services services) |
protected Term |
FunctionalOperationContractPO.getGlobalDefs(LocationVariable heap,
Term heapTerm,
Term selfTerm,
ImmutableList<Term> paramTerms,
Services services) |
Modifier and Type | Method and Description |
---|---|
static Term |
AbstractOperationPO.addAdditionalUninterpretedPredicateIfRequired(Services services,
Term term,
ImmutableList<LocationVariable> variablesToProtect,
Term exceptionVar)
This method adds the uninterpreted predicate to the given
Term
if the used ProofOblInput is an instance of AbstractOperationPO
and AbstractOperationPO.isAddUninterpretedPredicate() is true . |
protected abstract Term |
AbstractOperationPO.buildFrameClause(java.util.List<LocationVariable> modHeaps,
java.util.Map<Term,Term> heapToAtPre,
ProgramVariable selfVar,
ImmutableList<ProgramVariable> paramVars,
Services services)
Builds the frame clause including the modifies clause.
|
protected Term |
FunctionalOperationContractPO.buildFrameClause(java.util.List<LocationVariable> modHeaps,
java.util.Map<Term,Term> heapToAtPre,
ProgramVariable selfVar,
ImmutableList<ProgramVariable> paramVars,
Services services)
Builds the frame clause including the modifies clause.
|
protected Term |
AbstractOperationPO.buildFreePre(ProgramVariable selfVar,
KeYJavaType selfKJT,
ImmutableList<ProgramVariable> paramVars,
java.util.List<LocationVariable> heaps,
Services services)
Builds the "general assumption".
|
protected JavaBlock |
AbstractOperationPO.buildJavaBlock(ImmutableList<LocationVariable> formalParVars,
ProgramVariable selfVar,
ProgramVariable resultVar,
ProgramVariable exceptionVar,
boolean transaction,
ImmutableList<StatementBlock> sb)
Creates the try catch block to execute.
|
protected abstract ImmutableList<StatementBlock> |
AbstractOperationPO.buildOperationBlocks(ImmutableList<LocationVariable> formalParVars,
ProgramVariable selfVar,
ProgramVariable resultVar,
Services services)
Builds the code to execute in different statement blocks.
|
protected ImmutableList<StatementBlock> |
FunctionalOperationContractPO.buildOperationBlocks(ImmutableList<LocationVariable> formalParVars,
ProgramVariable selfVar,
ProgramVariable resultVar,
Services services)
Builds the code to execute in different statement blocks.
|
protected Term |
AbstractOperationPO.buildProgramTerm(ImmutableList<ProgramVariable> paramVars,
ImmutableList<LocationVariable> formalParamVars,
ProgramVariable selfVar,
ProgramVariable resultVar,
ProgramVariable exceptionVar,
java.util.Map<LocationVariable,LocationVariable> atPreVars,
Term postTerm,
ImmutableList<StatementBlock> sb,
Services services)
Creates the
Term which contains the modality including
the complete program to execute. |
protected Term |
AbstractOperationPO.buildProgramTerm(ImmutableList<ProgramVariable> paramVars,
ImmutableList<LocationVariable> formalParamVars,
ProgramVariable selfVar,
ProgramVariable resultVar,
ProgramVariable exceptionVar,
java.util.Map<LocationVariable,LocationVariable> atPreVars,
Term postTerm,
ImmutableList<StatementBlock> sb,
Services services)
Creates the
Term which contains the modality including
the complete program to execute. |
protected Term |
AbstractOperationPO.buildProgramTerm(ImmutableList<ProgramVariable> paramVars,
ImmutableList<LocationVariable> formalParamVars,
ProgramVariable selfVar,
ProgramVariable resultVar,
ProgramVariable exceptionVar,
java.util.Map<LocationVariable,LocationVariable> atPreVars,
Term postTerm,
ImmutableList<StatementBlock> sb,
Services services)
Creates the
Term which contains the modality including
the complete program to execute. |
protected Term |
AbstractOperationPO.buildUpdate(ImmutableList<ProgramVariable> paramVars,
ImmutableList<LocationVariable> formalParamVars,
java.util.Map<LocationVariable,LocationVariable> atPreVars,
Services services)
Builds the initial updates.
|
protected Term |
AbstractOperationPO.buildUpdate(ImmutableList<ProgramVariable> paramVars,
ImmutableList<LocationVariable> formalParamVars,
java.util.Map<LocationVariable,LocationVariable> atPreVars,
Services services)
Builds the initial updates.
|
protected Term |
AbstractOperationPO.buildUpdate(ImmutableList<ProgramVariable> paramVars,
ImmutableList<LocationVariable> formalParamVars,
java.util.Map<LocationVariable,LocationVariable> atPreVars,
Services services)
Builds the initial updates.
|
protected Term |
FunctionalOperationContractPO.buildUpdate(ImmutableList<ProgramVariable> paramVars,
ImmutableList<LocationVariable> formalParamVars,
java.util.Map<LocationVariable,LocationVariable> atPreVars,
Services services)
Builds the initial updates.
|
protected Term |
FunctionalOperationContractPO.buildUpdate(ImmutableList<ProgramVariable> paramVars,
ImmutableList<LocationVariable> formalParamVars,
java.util.Map<LocationVariable,LocationVariable> atPreVars,
Services services)
Builds the initial updates.
|
protected Term |
FunctionalOperationContractPO.buildUpdate(ImmutableList<ProgramVariable> paramVars,
ImmutableList<LocationVariable> formalParamVars,
java.util.Map<LocationVariable,LocationVariable> atPreVars,
Services services)
Builds the initial updates.
|
protected Term |
AbstractOperationPO.createUninterpretedPredicate(ImmutableList<LocationVariable> formalParamVars,
Term exceptionVar,
java.lang.String name,
Services services)
|
protected Term |
AbstractOperationPO.ensureUninterpretedPredicateExists(ImmutableList<ProgramVariable> paramVars,
ImmutableList<LocationVariable> formalParamVars,
ProgramVariable exceptionVar,
java.lang.String name,
Services services)
|
protected Term |
AbstractPO.generateSelfCreated(java.util.List<LocationVariable> heaps,
IProgramMethod pm,
ProgramVariable selfVar,
Services services)
Generates the general assumption that self is created.
|
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 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 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 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 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 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 abstract Term |
AbstractOperationPO.getPre(java.util.List<LocationVariable> modHeaps,
ProgramVariable selfVar,
ImmutableList<ProgramVariable> paramVars,
java.util.Map<LocationVariable,LocationVariable> atPreVars,
Services services)
Creates the precondition.
|
protected Term |
FunctionalOperationContractPO.getPre(java.util.List<LocationVariable> modHeaps,
ProgramVariable selfVar,
ImmutableList<ProgramVariable> paramVars,
java.util.Map<LocationVariable,LocationVariable> atPreVars,
Services services)
Creates the precondition.
|
protected Term |
FunctionalOperationContractPO.getPre(java.util.List<LocationVariable> modHeaps,
ProgramVariable selfVar,
ImmutableList<ProgramVariable> paramVars,
java.util.Map<LocationVariable,LocationVariable> atPreVars,
Services services)
Creates the precondition.
|
protected Term |
FunctionalOperationContractPO.getPre(java.util.List<LocationVariable> modHeaps,
ProgramVariable selfVar,
ImmutableList<ProgramVariable> paramVars,
java.util.Map<LocationVariable,LocationVariable> atPreVars,
Services services)
Creates the precondition.
|
protected Term |
AbstractOperationPO.newAdditionalUninterpretedPredicate(ImmutableList<LocationVariable> formalParamVars,
Term exceptionVar,
java.lang.String name,
Services services)
Creates a new uninterpreted predicate which is added to
AbstractOperationPO.additionalUninterpretedPredicates . |
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) |
Modifier and Type | Field and Description |
---|---|
protected java.util.List<LocationVariable> |
AbstractAuxiliaryContractBuiltInRuleApp.heaps |
Modifier and Type | Method and Description |
---|---|
java.util.Map<LocationVariable,Term> |
AuxiliaryContractBuilders.ConditionsAndClausesBuilder.buildModifiesClauses() |
static java.util.Map<LocationVariable,LocationVariable> |
UseOperationContractRule.computeAtPreVars(java.util.List<LocationVariable> heapContext,
TermServices services,
UseOperationContractRule.Instantiation inst)
Returns the correct pre-heap variables.
|
static java.util.Map<LocationVariable,LocationVariable> |
UseOperationContractRule.computeAtPreVars(java.util.List<LocationVariable> heapContext,
TermServices services,
UseOperationContractRule.Instantiation inst)
Returns the correct pre-heap variables.
|
protected static java.util.Map<LocationVariable,Function> |
AbstractBlockContractRule.createAndRegisterAnonymisationVariables(java.lang.Iterable<LocationVariable> variables,
BlockContract contract,
TermServices services) |
protected java.util.Map<LocationVariable,Function> |
AbstractLoopContractRule.createAndRegisterAnonymisationVariables(java.lang.Iterable<LocationVariable> variables,
LoopContract contract,
TermServices services) |
java.util.List<LocationVariable> |
LoopInvariantBuiltInRuleApp.getHeapContext() |
java.util.List<LocationVariable> |
IBuiltInRuleApp.getHeapContext() |
java.util.List<LocationVariable> |
AbstractBuiltInRuleApp.getHeapContext() |
java.util.List<LocationVariable> |
UseDependencyContractApp.getHeapContext() |
java.util.List<LocationVariable> |
ContractRuleApp.getHeapContext() |
java.util.List<LocationVariable> |
AbstractAuxiliaryContractBuiltInRuleApp.getHeapContext() |
Modifier and Type | Method and Description |
---|---|
static ImmutableList<Term> |
UseOperationContractRule.computeParams(Term baseHeapTerm,
java.util.Map<LocationVariable,Term> atPres,
LocationVariable baseHeap,
UseOperationContractRule.Instantiation inst,
TermFactory tf)
Returns the correct parameter terms.
|
static Term |
UseOperationContractRule.computeSelf(Term baseHeapTerm,
java.util.Map<LocationVariable,Term> atPres,
LocationVariable baseHeap,
UseOperationContractRule.Instantiation inst,
Term resultTerm,
TermFactory tf)
Returns the correct self term.
|
protected static AbstractLoopInvariantRule.AnonUpdateData |
AbstractLoopInvariantRule.createAnonUpdate(LocationVariable heap,
Term mod,
LoopSpecification inv,
Services services)
Computes the anonymizing update, the loop heap, the base heap, and the
anonymized heap.
|
Term |
AuxiliaryContractBuilders.GoalsConfigurator.setUpWdGoal(Goal goal,
BlockContract contract,
Term update,
Term anonUpdate,
LocationVariable heap,
Function anonHeap,
ImmutableSet<ProgramVariable> localIns) |
Modifier and Type | Method and Description |
---|---|
Term |
AuxiliaryContractBuilders.UpdatesBuilder.buildAnonInUpdate(java.util.Map<LocationVariable,Function> anonymisationHeaps) |
Term |
AuxiliaryContractBuilders.UpdatesBuilder.buildAnonOutUpdate(java.util.Map<LocationVariable,Function> anonymisationHeaps,
java.util.Map<LocationVariable,Term> modifiesClauses) |
Term |
AuxiliaryContractBuilders.UpdatesBuilder.buildAnonOutUpdate(java.util.Map<LocationVariable,Function> anonymisationHeaps,
java.util.Map<LocationVariable,Term> modifiesClauses) |
Term |
AuxiliaryContractBuilders.UpdatesBuilder.buildAnonOutUpdate(ProgramElement el,
java.util.Map<LocationVariable,Function> anonymisationHeaps,
java.util.Map<LocationVariable,Term> modifiesClauses) |
Term |
AuxiliaryContractBuilders.UpdatesBuilder.buildAnonOutUpdate(ProgramElement el,
java.util.Map<LocationVariable,Function> anonymisationHeaps,
java.util.Map<LocationVariable,Term> modifiesClauses) |
Term |
AuxiliaryContractBuilders.UpdatesBuilder.buildAnonOutUpdate(ProgramElement el,
java.util.Map<LocationVariable,Function> anonymisationHeaps,
java.util.Map<LocationVariable,Term> modifiesClauses,
java.lang.String prefix) |
Term |
AuxiliaryContractBuilders.UpdatesBuilder.buildAnonOutUpdate(ProgramElement el,
java.util.Map<LocationVariable,Function> anonymisationHeaps,
java.util.Map<LocationVariable,Term> modifiesClauses,
java.lang.String prefix) |
Term |
AuxiliaryContractBuilders.UpdatesBuilder.buildAnonOutUpdate(java.util.Set<LocationVariable> vars,
java.util.Map<LocationVariable,Function> anonymisationHeaps,
java.util.Map<LocationVariable,Term> modifiesClauses,
java.lang.String prefix) |
Term |
AuxiliaryContractBuilders.UpdatesBuilder.buildAnonOutUpdate(java.util.Set<LocationVariable> vars,
java.util.Map<LocationVariable,Function> anonymisationHeaps,
java.util.Map<LocationVariable,Term> modifiesClauses,
java.lang.String prefix) |
Term |
AuxiliaryContractBuilders.UpdatesBuilder.buildAnonOutUpdate(java.util.Set<LocationVariable> vars,
java.util.Map<LocationVariable,Function> anonymisationHeaps,
java.util.Map<LocationVariable,Term> modifiesClauses,
java.lang.String prefix) |
Term |
AuxiliaryContractBuilders.ConditionsAndClausesBuilder.buildFrameCondition(java.util.Map<LocationVariable,Term> modifiesClauses) |
Term |
AuxiliaryContractBuilders.UpdatesBuilder.buildRemembranceUpdate(java.util.List<LocationVariable> heaps) |
Term |
AuxiliaryContractBuilders.ConditionsAndClausesBuilder.buildSelfConditions(java.util.List<LocationVariable> heaps,
IProgramMethod pm,
KeYJavaType selfKJT,
Term self,
Services services)
Builds the assumptions for the
self variable
(self != null & self.created == true & exactInstance(self) ) |
Term |
AuxiliaryContractBuilders.ConditionsAndClausesBuilder.buildWellFormedAnonymisationHeapsCondition(java.util.Map<LocationVariable,Function> anonymisationHeaps) |
static java.util.Map<LocationVariable,LocationVariable> |
UseOperationContractRule.computeAtPreVars(java.util.List<LocationVariable> heapContext,
TermServices services,
UseOperationContractRule.Instantiation inst)
Returns the correct pre-heap variables.
|
static ImmutableList<Term> |
UseOperationContractRule.computeParams(Term baseHeapTerm,
java.util.Map<LocationVariable,Term> atPres,
LocationVariable baseHeap,
UseOperationContractRule.Instantiation inst,
TermFactory tf)
Returns the correct parameter terms.
|
static Term |
UseOperationContractRule.computeSelf(Term baseHeapTerm,
java.util.Map<LocationVariable,Term> atPres,
LocationVariable baseHeap,
UseOperationContractRule.Instantiation inst,
Term resultTerm,
TermFactory tf)
Returns the correct self term.
|
protected static Term |
AbstractLoopInvariantRule.conjunctFreeInv(Services services,
AbstractLoopInvariantRule.Instantiation inst,
java.util.Map<LocationVariable,Term> atPres,
java.util.List<LocationVariable> heapContext)
Creates a conjunction of all free invariant formulas for the
LocationVariable s in heapContext. |
protected static Term |
AbstractLoopInvariantRule.conjunctFreeInv(Services services,
AbstractLoopInvariantRule.Instantiation inst,
java.util.Map<LocationVariable,Term> atPres,
java.util.List<LocationVariable> heapContext)
Creates a conjunction of all free invariant formulas for the
LocationVariable s in heapContext. |
protected static Term |
AbstractLoopInvariantRule.conjunctInv(Services services,
AbstractLoopInvariantRule.Instantiation inst,
java.util.Map<LocationVariable,Term> atPres,
java.util.List<LocationVariable> heapContext)
Creates a conjunction of all invariant formulas for the
LocationVariable s in heapContext. |
protected static Term |
AbstractLoopInvariantRule.conjunctInv(Services services,
AbstractLoopInvariantRule.Instantiation inst,
java.util.Map<LocationVariable,Term> atPres,
java.util.List<LocationVariable> heapContext)
Creates a conjunction of all invariant formulas for the
LocationVariable s in heapContext. |
protected static AbstractLoopInvariantRule.AdditionalHeapTerms |
AbstractLoopInvariantRule.createAdditionalHeapTerms(Services services,
AbstractLoopInvariantRule.Instantiation inst,
java.util.List<LocationVariable> heapContext,
ImmutableSet<ProgramVariable> localOuts,
java.util.Map<LocationVariable,java.util.Map<Term,Term>> heapToBeforeLoop,
java.util.Map<LocationVariable,Term> atPres)
Prepare anon update, wellformed formula, frame condition and reachable
state formula.
|
protected static AbstractLoopInvariantRule.AdditionalHeapTerms |
AbstractLoopInvariantRule.createAdditionalHeapTerms(Services services,
AbstractLoopInvariantRule.Instantiation inst,
java.util.List<LocationVariable> heapContext,
ImmutableSet<ProgramVariable> localOuts,
java.util.Map<LocationVariable,java.util.Map<Term,Term>> heapToBeforeLoop,
java.util.Map<LocationVariable,Term> atPres)
Prepare anon update, wellformed formula, frame condition and reachable
state formula.
|
protected static AbstractLoopInvariantRule.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 java.util.Map<LocationVariable,Function> |
AbstractBlockContractRule.createAndRegisterAnonymisationVariables(java.lang.Iterable<LocationVariable> variables,
BlockContract contract,
TermServices services) |
protected java.util.Map<LocationVariable,Function> |
AbstractLoopContractRule.createAndRegisterAnonymisationVariables(java.lang.Iterable<LocationVariable> variables,
LoopContract contract,
TermServices services) |
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 |
AbstractLoopInvariantRule.createBeforeLoopUpdate(Services services,
java.util.List<LocationVariable> heapContext,
ImmutableSet<ProgramVariable> localOuts,
java.util.Map<LocationVariable,java.util.Map<Term,Term>> heapToBeforeLoop)
Creates the "...Before_LOOP" update needed for the variant.
|
static java.util.List<PosInOccurrence> |
UseDependencyContractRule.getSteps(java.util.List<LocationVariable> heapContext,
PosInOccurrence pos,
Sequent seq,
Services services) |
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.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.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) |
void |
AbstractBlockContractBuiltInRuleApp.update(JavaStatement statement,
BlockContract contract,
java.util.List<LocationVariable> heaps) |
void |
AbstractLoopContractBuiltInRuleApp.update(JavaStatement statement,
LoopContract contract,
java.util.List<LocationVariable> heaps) |
Modifier and Type | Method and Description |
---|---|
protected MergeProcedure.ValuesMergeResult |
MergeRule.mergeHeaps(MergeProcedure mergeRule,
LocationVariable heapVar,
Term heap1,
Term heap2,
SymbolicExecutionState state1,
SymbolicExecutionState state2,
Term distinguishingFormula,
Services services)
Merges two heaps in a zip-like procedure.
|
Modifier and Type | Method and Description |
---|---|
void |
IntroAtPreDefsOp.updateBlockAndLoopContracts(ImmutableSet<? extends JavaStatement> statements,
java.util.Map<LocationVariable,LocationVariable> atPreVars,
java.util.Map<LocationVariable,LocationVariable> atPreHeapVars,
Services services)
Replace the placeholder variables
(see
AuxiliaryContract.getPlaceholderVariables() )
of all block contracts for blocks in blocks by
atPreVars and atPreHeapVars |
void |
IntroAtPreDefsOp.updateBlockAndLoopContracts(ImmutableSet<? extends JavaStatement> statements,
java.util.Map<LocationVariable,LocationVariable> atPreVars,
java.util.Map<LocationVariable,LocationVariable> atPreHeapVars,
Services services)
Replace the placeholder variables
(see
AuxiliaryContract.getPlaceholderVariables() )
of all block contracts for blocks in blocks by
atPreVars and atPreHeapVars |
void |
IntroAtPreDefsOp.updateBlockAndLoopContracts(ImmutableSet<? extends JavaStatement> statements,
java.util.Map<LocationVariable,LocationVariable> atPreVars,
java.util.Map<LocationVariable,LocationVariable> atPreHeapVars,
Services services)
Replace the placeholder variables
(see
AuxiliaryContract.getPlaceholderVariables() )
of all block contracts for blocks in blocks by
atPreVars and atPreHeapVars |
void |
IntroAtPreDefsOp.updateBlockAndLoopContracts(ImmutableSet<? extends JavaStatement> statements,
java.util.Map<LocationVariable,LocationVariable> atPreVars,
java.util.Map<LocationVariable,LocationVariable> atPreHeapVars,
Services services)
Replace the placeholder variables
(see
AuxiliaryContract.getPlaceholderVariables() )
of all block contracts for blocks in blocks by
atPreVars and atPreHeapVars |
void |
IntroAtPreDefsOp.updateBlockAndLoopContracts(ImmutableSet<StatementBlock> blocks,
ImmutableSet<LoopStatement> loops,
java.util.Map<LocationVariable,LocationVariable> atPreVars,
java.util.Map<LocationVariable,LocationVariable> atPreHeapVars,
Services services)
Replace the placeholder variables
(see
AuxiliaryContract.getPlaceholderVariables() )
of all block contracts for blocks in blocks by
atPreVars and atPreHeapVars |
void |
IntroAtPreDefsOp.updateBlockAndLoopContracts(ImmutableSet<StatementBlock> blocks,
ImmutableSet<LoopStatement> loops,
java.util.Map<LocationVariable,LocationVariable> atPreVars,
java.util.Map<LocationVariable,LocationVariable> atPreHeapVars,
Services services)
Replace the placeholder variables
(see
AuxiliaryContract.getPlaceholderVariables() )
of all block contracts for blocks in blocks by
atPreVars and atPreHeapVars |
void |
IntroAtPreDefsOp.updateBlockAndLoopContracts(ImmutableSet<StatementBlock> blocks,
ImmutableSet<LoopStatement> loops,
java.util.Map<LocationVariable,LocationVariable> atPreVars,
java.util.Map<LocationVariable,LocationVariable> atPreHeapVars,
Services services)
Replace the placeholder variables
(see
AuxiliaryContract.getPlaceholderVariables() )
of all block contracts for blocks in blocks by
atPreVars and atPreHeapVars |
void |
IntroAtPreDefsOp.updateBlockAndLoopContracts(ImmutableSet<StatementBlock> blocks,
ImmutableSet<LoopStatement> loops,
java.util.Map<LocationVariable,LocationVariable> atPreVars,
java.util.Map<LocationVariable,LocationVariable> atPreHeapVars,
Services services)
Replace the placeholder variables
(see
AuxiliaryContract.getPlaceholderVariables() )
of all block contracts for blocks in blocks by
atPreVars and atPreHeapVars |
Modifier and Type | 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 | Field and Description |
---|---|
java.util.Map<LocationVariable,ProgramVariable> |
Contract.OriginalVariables.atPres |
protected java.util.Map<LocationVariable,Term> |
AbstractAuxiliaryContractImpl.freePostconditions |
protected java.util.Map<LocationVariable,Term> |
AbstractAuxiliaryContractImpl.Combinator.freePostconditions |
protected java.util.Map<LocationVariable,Term> |
AbstractAuxiliaryContractImpl.freePreconditions |
protected java.util.Map<LocationVariable,Term> |
AbstractAuxiliaryContractImpl.Combinator.freePreconditions |
protected java.util.Map<LocationVariable,java.lang.Boolean> |
AbstractAuxiliaryContractImpl.hasMod |
protected java.util.Map<LocationVariable,Term> |
AbstractAuxiliaryContractImpl.modifiesClauses |
protected java.util.Map<LocationVariable,Term> |
AbstractAuxiliaryContractImpl.Combinator.modifiesClauses |
java.util.Map<LocationVariable,LocationVariable> |
AuxiliaryContract.Variables.outerRemembranceHeaps
A map from every heap
heap that is accessible inside the block to
heap_Before_METHOD . |
java.util.Map<LocationVariable,LocationVariable> |
AuxiliaryContract.Variables.outerRemembranceHeaps
A map from every heap
heap that is accessible inside the block to
heap_Before_METHOD . |
java.util.Map<LocationVariable,Term> |
AuxiliaryContract.Terms.outerRemembranceHeaps |
java.util.Map<LocationVariable,LocationVariable> |
AuxiliaryContract.Variables.outerRemembranceVariables
A map from every variable
var that is accessible inside the block to
var_Before_METHOD . |
java.util.Map<LocationVariable,LocationVariable> |
AuxiliaryContract.Variables.outerRemembranceVariables
A map from every variable
var that is accessible inside the block to
var_Before_METHOD . |
java.util.Map<LocationVariable,Term> |
AuxiliaryContract.Terms.outerRemembranceVariables |
protected java.util.Map<LocationVariable,Term> |
AbstractAuxiliaryContractImpl.postconditions |
protected java.util.Map<LocationVariable,Term> |
AbstractAuxiliaryContractImpl.Combinator.postconditions |
protected java.util.Map<LocationVariable,Term> |
AbstractAuxiliaryContractImpl.preconditions |
protected java.util.Map<LocationVariable,Term> |
AbstractAuxiliaryContractImpl.Combinator.preconditions |
java.util.Map<LocationVariable,LocationVariable> |
AuxiliaryContract.Variables.remembranceHeaps
A map from every heap
heap to heap_Before_BLOCK . |
java.util.Map<LocationVariable,LocationVariable> |
AuxiliaryContract.Variables.remembranceHeaps
A map from every heap
heap to heap_Before_BLOCK . |
java.util.Map<LocationVariable,Term> |
AuxiliaryContract.Terms.remembranceHeaps |
java.util.Map<LocationVariable,LocationVariable> |
AuxiliaryContract.Variables.remembranceLocalVariables
A map from every variable
var that is assignable inside the block to
var_Before_BLOCK . |
java.util.Map<LocationVariable,LocationVariable> |
AuxiliaryContract.Variables.remembranceLocalVariables
A map from every variable
var that is assignable inside the block to
var_Before_BLOCK . |
java.util.Map<LocationVariable,Term> |
AuxiliaryContract.Terms.remembranceLocalVariables |
protected java.util.Map<LocationVariable,LocationVariable> |
AbstractAuxiliaryContractImpl.Combinator.remembranceVariables |
protected java.util.Map<LocationVariable,LocationVariable> |
AbstractAuxiliaryContractImpl.Combinator.remembranceVariables |
Modifier and Type | Method and Description |
---|---|
LocationVariable |
WellDefinednessCheck.getHeap() |
Modifier and Type | Method and Description |
---|---|
protected java.util.Map<LocationVariable,Term> |
AbstractAuxiliaryContractImpl.Creator.buildFreePostconditions() |
protected java.util.Map<LocationVariable,Term> |
AbstractAuxiliaryContractImpl.Creator.buildFreePreconditions() |
protected java.util.Map<LocationVariable,Term> |
AbstractAuxiliaryContractImpl.Creator.buildPostconditions() |
protected java.util.Map<LocationVariable,Term> |
AbstractAuxiliaryContractImpl.Creator.buildPreconditions() |
protected java.util.Map<LocationVariable,Term> |
LoopContractImpl.Creator.buildPreconditions() |
java.util.Map<LocationVariable,LocationVariable> |
AuxiliaryContract.Variables.combineOuterRemembranceVariables() |
java.util.Map<LocationVariable,LocationVariable> |
AuxiliaryContract.Variables.combineOuterRemembranceVariables() |
java.util.Map<LocationVariable,LocationVariable> |
AuxiliaryContract.Variables.combineRemembranceVariables() |
java.util.Map<LocationVariable,LocationVariable> |
AuxiliaryContract.Variables.combineRemembranceVariables() |
java.util.Map<LocationVariable,Term> |
PredicateAbstractionMergeContract.getAtPres() |
static java.util.Map<LocationVariable,Term> |
HeapContext.getAtPres(java.util.Map<LocationVariable,LocationVariable> atPreVars,
Services services) |
static java.util.Map<LocationVariable,LocationVariable> |
HeapContext.getBeforeAtPreVars(java.util.List<LocationVariable> heaps,
TermServices services,
java.lang.String contextName) |
static java.util.Map<LocationVariable,LocationVariable> |
HeapContext.getBeforeAtPreVars(java.util.List<LocationVariable> heaps,
TermServices services,
java.lang.String contextName) |
java.util.Map<LocationVariable,Term> |
LoopSpecification.getInternalAtPres()
Returns operators internally used for the pre-heap.
|
java.util.Map<LocationVariable,Term> |
LoopSpecImpl.getInternalAtPres() |
java.util.Map<LocationVariable,Term> |
LoopSpecification.getInternalFreeInvariants()
Returns the term internally used for the "free" invariant.
|
java.util.Map<LocationVariable,Term> |
LoopSpecImpl.getInternalFreeInvariants() |
java.util.Map<LocationVariable,ImmutableList<InfFlowSpec>> |
LoopSpecification.getInternalInfFlowSpec() |
java.util.Map<LocationVariable,ImmutableList<InfFlowSpec>> |
LoopSpecImpl.getInternalInfFlowSpec() |
java.util.Map<LocationVariable,Term> |
LoopSpecification.getInternalInvariants()
Returns the term internally used for the invariant.
|
java.util.Map<LocationVariable,Term> |
LoopSpecImpl.getInternalInvariants() |
java.util.Map<LocationVariable,Term> |
LoopSpecification.getInternalModifies()
Returns the term internally used for the modifies clause.
|
java.util.Map<LocationVariable,Term> |
LoopSpecImpl.getInternalModifies() |
static java.util.List<LocationVariable> |
HeapContext.getModHeaps(Services services,
boolean transaction) |
Modifier and Type | Method and Description |
---|---|
DependencyContract |
ContractFactory.dep(KeYJavaType kjt,
LocationVariable targetHeap,
Triple<IObserverFunction,Term,Term> dep,
ProgramVariable selfVar) |
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 |
AbstractAuxiliaryContractImpl.getAssignable(LocationVariable heap) |
Term |
FunctionalAuxiliaryContract.getAssignable(LocationVariable heap) |
Term |
FunctionalOperationContractImpl.getAssignable(LocationVariable heap) |
Term |
InformationFlowContractImpl.getAssignable(LocationVariable heap) |
Term |
DependencyContractImpl.getAssignable(LocationVariable heap) |
Term |
WellDefinednessCheck.getAssignable(LocationVariable heap) |
Term |
Contract.getAssignable(LocationVariable heap) |
Term |
AuxiliaryContract.getAssignable(LocationVariable heap) |
Term |
FunctionalAuxiliaryContract.getDep(LocationVariable heap,
boolean atPre,
ProgramVariable selfVar,
ImmutableList<ProgramVariable> paramVars,
java.util.Map<LocationVariable,? extends ProgramVariable> atPreVars,
Services services) |
Term |
FunctionalOperationContractImpl.getDep(LocationVariable heap,
boolean atPre,
ProgramVariable selfVar,
ImmutableList<ProgramVariable> paramVars,
java.util.Map<LocationVariable,? extends ProgramVariable> atPreVars,
Services services) |
Term |
InformationFlowContractImpl.getDep(LocationVariable heap,
boolean atPre,
ProgramVariable selfVar,
ImmutableList<ProgramVariable> paramVars,
java.util.Map<LocationVariable,? extends ProgramVariable> atPreVars,
Services services) |
Term |
DependencyContractImpl.getDep(LocationVariable heap,
boolean atPre,
ProgramVariable selfVar,
ImmutableList<ProgramVariable> paramVars,
java.util.Map<LocationVariable,? extends ProgramVariable> atPreVars,
Services services) |
Term |
WellDefinednessCheck.getDep(LocationVariable heap,
boolean atPre,
ProgramVariable selfVar,
ImmutableList<ProgramVariable> paramVars,
java.util.Map<LocationVariable,? extends ProgramVariable> atPreVars,
Services services)
Deprecated.
|
Term |
Contract.getDep(LocationVariable heap,
boolean atPre,
ProgramVariable selfVar,
ImmutableList<ProgramVariable> paramVars,
java.util.Map<LocationVariable,? extends ProgramVariable> atPreVars,
Services services)
Returns the dependency set of the contract.
|
Term |
FunctionalAuxiliaryContract.getDep(LocationVariable heap,
boolean atPre,
Term heapTerm,
Term selfTerm,
ImmutableList<Term> paramTerms,
java.util.Map<LocationVariable,Term> atPres,
Services services) |
Term |
FunctionalOperationContractImpl.getDep(LocationVariable heap,
boolean atPre,
Term heapTerm,
Term selfTerm,
ImmutableList<Term> paramTerms,
java.util.Map<LocationVariable,Term> atPres,
Services services) |
Term |
InformationFlowContractImpl.getDep(LocationVariable heap,
boolean atPre,
Term heapTerm,
Term selfTerm,
ImmutableList<Term> paramTerms,
java.util.Map<LocationVariable,Term> atPres,
Services services) |
Term |
DependencyContractImpl.getDep(LocationVariable heap,
boolean atPre,
Term heapTerm,
Term selfTerm,
ImmutableList<Term> paramTerms,
java.util.Map<LocationVariable,Term> atPres,
Services services) |
Term |
WellDefinednessCheck.getDep(LocationVariable heap,
boolean atPre,
Term heapTerm,
Term selfTerm,
ImmutableList<Term> paramTerms,
java.util.Map<LocationVariable,Term> atPres,
Services services)
Deprecated.
|
Term |
Contract.getDep(LocationVariable heap,
boolean atPre,
Term heapTerm,
Term selfTerm,
ImmutableList<Term> paramTerms,
java.util.Map<LocationVariable,Term> atPres,
Services services)
Returns the dependency set of the contract.
|
Term |
AbstractAuxiliaryContractImpl.getEnsures(LocationVariable heap) |
Term |
FunctionalOperationContractImpl.getEnsures(LocationVariable heap) |
Term |
FunctionalOperationContract.getEnsures(LocationVariable heap) |
Term |
WellDefinednessCheck.getEnsures(LocationVariable heap) |
Term |
AuxiliaryContract.getEnsures(LocationVariable heap) |
Term |
AbstractAuxiliaryContractImpl.getEnsuresFree(LocationVariable heap) |
Term |
AuxiliaryContract.getEnsuresFree(LocationVariable heap) |
Term |
LoopSpecification.getFreeInvariant(LocationVariable heap,
Term selfTerm,
java.util.Map<LocationVariable,Term> atPres,
Services services)
Returns the free invariant formula.
|
Term |
LoopSpecImpl.getFreeInvariant(LocationVariable heap,
Term selfTerm,
java.util.Map<LocationVariable,Term> atPres,
Services services) |
Term |
FunctionalOperationContractImpl.getFreePost(LocationVariable heap,
ProgramVariable selfVar,
ImmutableList<ProgramVariable> paramVars,
ProgramVariable resultVar,
ProgramVariable excVar,
java.util.Map<LocationVariable,? extends ProgramVariable> atPreVars,
Services services) |
Term |
FunctionalOperationContract.getFreePost(LocationVariable heap,
ProgramVariable selfVar,
ImmutableList<ProgramVariable> paramVars,
ProgramVariable resultVar,
ProgramVariable excVar,
java.util.Map<LocationVariable,? extends ProgramVariable> atPreVars,
Services services) |
Term |
FunctionalOperationContractImpl.getFreePost(LocationVariable heap,
Term heapTerm,
Term selfTerm,
ImmutableList<Term> paramTerms,
Term resultTerm,
Term excTerm,
java.util.Map<LocationVariable,Term> atPres,
Services services) |
Term |
FunctionalOperationContract.getFreePost(LocationVariable heap,
Term heapTerm,
Term selfTerm,
ImmutableList<Term> paramTerms,
Term resultTerm,
Term excTerm,
java.util.Map<LocationVariable,Term> atPres,
Services services) |
Term |
AbstractAuxiliaryContractImpl.getFreePostcondition(LocationVariable heap,
AuxiliaryContract.Variables variables,
Services services) |
Term |
AuxiliaryContract.getFreePostcondition(LocationVariable heap,
AuxiliaryContract.Variables variables,
Services services) |
Term |
AbstractAuxiliaryContractImpl.getFreePostcondition(LocationVariable heap,
Services services) |
Term |
AuxiliaryContract.getFreePostcondition(LocationVariable heap,
Services services) |
Term |
AbstractAuxiliaryContractImpl.getFreePostcondition(LocationVariable heapVariable,
Term heap,
AuxiliaryContract.Terms terms,
Services services) |
Term |
AuxiliaryContract.getFreePostcondition(LocationVariable heapVariable,
Term heap,
AuxiliaryContract.Terms terms,
Services services) |
Term |
FunctionalOperationContractImpl.getFreePre(LocationVariable heap,
ProgramVariable selfVar,
ImmutableList<ProgramVariable> paramVars,
java.util.Map<LocationVariable,? extends ProgramVariable> atPreVars,
Services services) |
Term |
OperationContract.getFreePre(LocationVariable heap,
ProgramVariable selfVar,
ImmutableList<ProgramVariable> paramVars,
java.util.Map<LocationVariable,? extends ProgramVariable> atPreVars,
Services services) |
Term |
FunctionalOperationContractImpl.getFreePre(LocationVariable heap,
Term heapTerm,
Term selfTerm,
ImmutableList<Term> paramTerms,
java.util.Map<LocationVariable,Term> atPres,
Services services) |
Term |
OperationContract.getFreePre(LocationVariable heap,
Term heapTerm,
Term selfTerm,
ImmutableList<Term> paramTerms,
java.util.Map<LocationVariable,Term> atPres,
Services services) |
Term |
AbstractAuxiliaryContractImpl.getFreePrecondition(LocationVariable heap,
AuxiliaryContract.Variables variables,
Services services) |
Term |
AuxiliaryContract.getFreePrecondition(LocationVariable heap,
AuxiliaryContract.Variables variables,
Services services) |
Term |
AbstractAuxiliaryContractImpl.getFreePrecondition(LocationVariable heap,
ProgramVariable self,
java.util.Map<LocationVariable,LocationVariable> atPres,
Services services) |
Term |
AuxiliaryContract.getFreePrecondition(LocationVariable heap,
ProgramVariable self,
java.util.Map<LocationVariable,LocationVariable> atPres,
Services services) |
Term |
AbstractAuxiliaryContractImpl.getFreePrecondition(LocationVariable heap,
Services services) |
Term |
AuxiliaryContract.getFreePrecondition(LocationVariable heap,
Services services) |
Term |
AbstractAuxiliaryContractImpl.getFreePrecondition(LocationVariable heapVariable,
Term heap,
AuxiliaryContract.Terms terms,
Services services) |
Term |
AuxiliaryContract.getFreePrecondition(LocationVariable heapVariable,
Term heap,
AuxiliaryContract.Terms terms,
Services services) |
Term |
AbstractAuxiliaryContractImpl.getFreePrecondition(LocationVariable heapVariable,
Term heap,
Term self,
java.util.Map<LocationVariable,Term> atPres,
Services services) |
Term |
AuxiliaryContract.getFreePrecondition(LocationVariable heapVariable,
Term heap,
Term self,
java.util.Map<LocationVariable,Term> atPres,
Services services) |
Term |
FunctionalAuxiliaryContract.getGlobalDefs(LocationVariable heap,
Term heapTerm,
Term selfTerm,
ImmutableList<Term> paramTerms,
Services services) |
Term |
FunctionalOperationContractImpl.getGlobalDefs(LocationVariable heap,
Term heapTerm,
Term selfTerm,
ImmutableList<Term> paramTerms,
Services services) |
Term |
InformationFlowContractImpl.getGlobalDefs(LocationVariable heap,
Term heapTerm,
Term selfTerm,
ImmutableList<Term> paramTerms,
Services services) |
Term |
DependencyContractImpl.getGlobalDefs(LocationVariable heap,
Term heapTerm,
Term selfTerm,
ImmutableList<Term> paramTerms,
Services services) |
Term |
WellDefinednessCheck.getGlobalDefs(LocationVariable heap,
Term heapTerm,
Term selfTerm,
ImmutableList<Term> paramTerms,
Services services)
Deprecated.
|
Term |
Contract.getGlobalDefs(LocationVariable heap,
Term heapTerm,
Term selfTerm,
ImmutableList<Term> paramTerms,
Services services) |
ImmutableList<InfFlowSpec> |
LoopSpecification.getInfFlowSpecs(LocationVariable heap)
Returns the information flow specification clause.
|
ImmutableList<InfFlowSpec> |
LoopSpecImpl.getInfFlowSpecs(LocationVariable heap) |
ImmutableList<InfFlowSpec> |
LoopSpecification.getInfFlowSpecs(LocationVariable heap,
Term selfTerm,
java.util.Map<LocationVariable,Term> atPres,
Services services) |
ImmutableList<InfFlowSpec> |
LoopSpecImpl.getInfFlowSpecs(LocationVariable heap,
Term selfTerm,
java.util.Map<LocationVariable,Term> atPres,
Services services) |
Term |
LoopSpecification.getInvariant(LocationVariable heap,
Term selfTerm,
java.util.Map<LocationVariable,Term> atPres,
Services services)
Returns the invariant formula.
|
Term |
LoopSpecImpl.getInvariant(LocationVariable heap,
Term selfTerm,
java.util.Map<LocationVariable,Term> atPres,
Services services) |
Term |
FunctionalOperationContractImpl.getMod(LocationVariable heap,
ProgramVariable selfVar,
ImmutableList<ProgramVariable> paramVars,
Services services) |
Term |
OperationContract.getMod(LocationVariable heapVar,
ProgramVariable selfVar,
ImmutableList<ProgramVariable> paramVars,
Services services)
Returns the modifies clause of the contract.
|
Term |
FunctionalOperationContractImpl.getMod(LocationVariable heap,
Term heapTerm,
Term selfTerm,
ImmutableList<Term> paramTerms,
Services services) |
Term |
OperationContract.getMod(LocationVariable heapVar,
Term heapTerm,
Term selfTerm,
ImmutableList<Term> paramTerms,
Services services)
Returns the modifies clause of the contract.
|
Term |
LoopSpecification.getModifies(LocationVariable heap,
Term selfTerm,
java.util.Map<LocationVariable,Term> atPres,
Services services)
Returns the modifies clause.
|
Term |
LoopSpecImpl.getModifies(LocationVariable heap,
Term selfTerm,
java.util.Map<LocationVariable,Term> atPres,
Services services) |
Term |
AbstractAuxiliaryContractImpl.getModifiesClause(LocationVariable heap,
AuxiliaryContract.Variables variables,
Services services) |
Term |
AuxiliaryContract.getModifiesClause(LocationVariable heap,
AuxiliaryContract.Variables variables,
Services services) |
Term |
AbstractAuxiliaryContractImpl.getModifiesClause(LocationVariable heap,
ProgramVariable self,
Services services) |
Term |
AuxiliaryContract.getModifiesClause(LocationVariable heap,
ProgramVariable self,
Services services) |
Term |
AbstractAuxiliaryContractImpl.getModifiesClause(LocationVariable heap,
Services services) |
Term |
AuxiliaryContract.getModifiesClause(LocationVariable heap,
Services services) |
Term |
AbstractAuxiliaryContractImpl.getModifiesClause(LocationVariable heapVariable,
Term heap,
Term self,
Services services) |
Term |
AuxiliaryContract.getModifiesClause(LocationVariable heapVariable,
Term heap,
Term self,
Services services) |
Term |
FunctionalOperationContractImpl.getPost(LocationVariable heap,
ProgramVariable selfVar,
ImmutableList<ProgramVariable> paramVars,
ProgramVariable resultVar,
ProgramVariable excVar,
java.util.Map<LocationVariable,? extends ProgramVariable> atPreVars,
Services services) |
Term |
FunctionalOperationContract.getPost(LocationVariable heap,
ProgramVariable selfVar,
ImmutableList<ProgramVariable> paramVars,
ProgramVariable resultVar,
ProgramVariable excVar,
java.util.Map<LocationVariable,? extends ProgramVariable> atPreVars,
Services services)
Returns the postcondition of the contract.
|
Term |
FunctionalOperationContractImpl.getPost(LocationVariable heap,
Term heapTerm,
Term selfTerm,
ImmutableList<Term> paramTerms,
Term resultTerm,
Term excTerm,
java.util.Map<LocationVariable,Term> atPres,
Services services) |
Term |
FunctionalOperationContract.getPost(LocationVariable heap,
Term heapTerm,
Term selfTerm,
ImmutableList<Term> paramTerms,
Term resultTerm,
Term excTerm,
java.util.Map<LocationVariable,Term> atPres,
Services services)
Returns the postcondition of the contract.
|
Term |
AbstractAuxiliaryContractImpl.getPostcondition(LocationVariable heap,
AuxiliaryContract.Variables variables,
Services services) |
Term |
AuxiliaryContract.getPostcondition(LocationVariable heap,
AuxiliaryContract.Variables variables,
Services services) |
Term |
AbstractAuxiliaryContractImpl.getPostcondition(LocationVariable heap,
Services services) |
Term |
AuxiliaryContract.getPostcondition(LocationVariable heap,
Services services) |
Term |
AbstractAuxiliaryContractImpl.getPostcondition(LocationVariable heapVariable,
Term heap,
AuxiliaryContract.Terms terms,
Services services) |
Term |
AuxiliaryContract.getPostcondition(LocationVariable heapVariable,
Term heap,
AuxiliaryContract.Terms terms,
Services services) |
Term |
FunctionalAuxiliaryContract.getPre(LocationVariable heap,
ProgramVariable selfVar,
ImmutableList<ProgramVariable> paramVars,
java.util.Map<LocationVariable,? extends ProgramVariable> atPreVars,
Services services) |
Term |
FunctionalOperationContractImpl.getPre(LocationVariable heap,
ProgramVariable selfVar,
ImmutableList<ProgramVariable> paramVars,
java.util.Map<LocationVariable,? extends ProgramVariable> atPreVars,
Services services) |
Term |
InformationFlowContractImpl.getPre(LocationVariable heap,
ProgramVariable selfVar,
ImmutableList<ProgramVariable> paramVars,
java.util.Map<LocationVariable,? extends ProgramVariable> atPreVars,
Services services)
Deprecated.
|
Term |
DependencyContractImpl.getPre(LocationVariable heap,
ProgramVariable selfVar,
ImmutableList<ProgramVariable> paramVars,
java.util.Map<LocationVariable,? extends ProgramVariable> atPreVars,
Services services) |
Term |
WellDefinednessCheck.getPre(LocationVariable heap,
ProgramVariable selfVar,
ImmutableList<ProgramVariable> paramVars,
java.util.Map<LocationVariable,? extends ProgramVariable> atPreVars,
Services services)
Deprecated.
|
Term |
Contract.getPre(LocationVariable heap,
ProgramVariable selfVar,
ImmutableList<ProgramVariable> paramVars,
java.util.Map<LocationVariable,? extends ProgramVariable> atPreVars,
Services services)
Returns the precondition of the contract.
|
Term |
FunctionalAuxiliaryContract.getPre(LocationVariable heap,
Term heapTerm,
Term selfTerm,
ImmutableList<Term> paramTerms,
java.util.Map<LocationVariable,Term> atPres,
Services services) |
Term |
FunctionalOperationContractImpl.getPre(LocationVariable heap,
Term heapTerm,
Term selfTerm,
ImmutableList<Term> paramTerms,
java.util.Map<LocationVariable,Term> atPres,
Services services) |
Term |
InformationFlowContractImpl.getPre(LocationVariable heap,
Term heapTerm,
Term selfTerm,
ImmutableList<Term> paramTerms,
java.util.Map<LocationVariable,Term> atPres,
Services services)
Deprecated.
|
Term |
DependencyContractImpl.getPre(LocationVariable heap,
Term heapTerm,
Term selfTerm,
ImmutableList<Term> paramTerms,
java.util.Map<LocationVariable,Term> atPres,
Services services) |
Term |
WellDefinednessCheck.getPre(LocationVariable heap,
Term heapTerm,
Term selfTerm,
ImmutableList<Term> paramTerms,
java.util.Map<LocationVariable,Term> atPres,
Services services)
Deprecated.
|
Term |
Contract.getPre(LocationVariable heap,
Term heapTerm,
Term selfTerm,
ImmutableList<Term> paramTerms,
java.util.Map<LocationVariable,Term> atPres,
Services services)
Returns the precondition of the contract.
|
Term |
AbstractAuxiliaryContractImpl.getPrecondition(LocationVariable heap,
AuxiliaryContract.Variables variables,
Services services) |
Term |
AuxiliaryContract.getPrecondition(LocationVariable heap,
AuxiliaryContract.Variables variables,
Services services) |
Term |
AbstractAuxiliaryContractImpl.getPrecondition(LocationVariable heap,
ProgramVariable self,
java.util.Map<LocationVariable,LocationVariable> atPres,
Services services) |
Term |
AuxiliaryContract.getPrecondition(LocationVariable heap,
ProgramVariable self,
java.util.Map<LocationVariable,LocationVariable> atPres,
Services services) |
Term |
AbstractAuxiliaryContractImpl.getPrecondition(LocationVariable heap,
Services services) |
Term |
AuxiliaryContract.getPrecondition(LocationVariable heap,
Services services) |
Term |
AbstractAuxiliaryContractImpl.getPrecondition(LocationVariable heapVariable,
Term heap,
AuxiliaryContract.Terms terms,
Services services) |
Term |
AuxiliaryContract.getPrecondition(LocationVariable heapVariable,
Term heap,
AuxiliaryContract.Terms terms,
Services services) |
Term |
AbstractAuxiliaryContractImpl.getPrecondition(LocationVariable heapVariable,
Term heap,
Term self,
java.util.Map<LocationVariable,Term> atPres,
Services services) |
Term |
AuxiliaryContract.getPrecondition(LocationVariable heapVariable,
Term heap,
Term self,
java.util.Map<LocationVariable,Term> atPres,
Services services) |
protected java.util.Map<Term,Term> |
FunctionalOperationContractImpl.getReplaceMap(LocationVariable heap,
Term heapTerm,
Term selfTerm,
ImmutableList<Term> paramTerms,
Services services)
Deprecated.
|
protected java.util.Map<Term,Term> |
FunctionalOperationContractImpl.getReplaceMap(LocationVariable heap,
Term heapTerm,
Term selfTerm,
ImmutableList<Term> paramTerms,
Term resultTerm,
Term excTerm,
Term atPre,
Services services)
Deprecated.
|
Term |
FunctionalOperationContractImpl.getRepresentsAxiom(LocationVariable heap,
ProgramVariable selfVar,
ImmutableList<ProgramVariable> paramVars,
ProgramVariable resultVar,
java.util.Map<LocationVariable,? extends ProgramVariable> atPreVars,
Services services) |
Term |
FunctionalOperationContract.getRepresentsAxiom(LocationVariable heap,
ProgramVariable selfVar,
ImmutableList<ProgramVariable> paramVars,
ProgramVariable resultVar,
java.util.Map<LocationVariable,? extends ProgramVariable> atPreVars,
Services services)
Returns the model method definition for model method contracts
|
Term |
FunctionalOperationContractImpl.getRepresentsAxiom(LocationVariable heap,
Term heapTerm,
Term selfTerm,
ImmutableList<Term> paramTerms,
Term resultTerm,
Term excTerm,
java.util.Map<LocationVariable,Term> atPres,
Services services) |
Term |
FunctionalOperationContract.getRepresentsAxiom(LocationVariable heap,
Term heapTerm,
Term selfTerm,
ImmutableList<Term> paramTerms,
Term resultTerm,
Term excTerm,
java.util.Map<LocationVariable,Term> atPres,
Services services) |
Term |
AbstractAuxiliaryContractImpl.getRequires(LocationVariable heap) |
Term |
FunctionalAuxiliaryContract.getRequires(LocationVariable heap) |
Term |
FunctionalOperationContractImpl.getRequires(LocationVariable heap) |
Term |
InformationFlowContractImpl.getRequires(LocationVariable heap) |
Term |
DependencyContractImpl.getRequires(LocationVariable heap) |
Term |
WellDefinednessCheck.getRequires(LocationVariable heap) |
Term |
Contract.getRequires(LocationVariable heap) |
Term |
AuxiliaryContract.getRequires(LocationVariable heap) |
Term |
AbstractAuxiliaryContractImpl.getRequiresFree(LocationVariable heap) |
Term |
AuxiliaryContract.getRequiresFree(LocationVariable heap) |
static java.lang.String |
FunctionalOperationContractImpl.getText(FunctionalOperationContract contract,
ImmutableList<Term> contractParams,
Term resultTerm,
Term contractSelf,
Term excTerm,
LocationVariable baseHeap,
Term baseHeapTerm,
java.util.List<LocationVariable> heapContext,
java.util.Map<LocationVariable,Term> atPres,
boolean includeHtmlMarkup,
Services services,
boolean usePrettyPrinting,
boolean useUnicodeSymbols) |
Term |
WellDefinednessCheck.getUpdates(Term mod,
LocationVariable heap,
ProgramVariable heapAtPre,
Term anonHeap,
TermServices services)
Gets the necessary updates applicable to the post-condition
|
boolean |
AbstractAuxiliaryContractImpl.hasModifiesClause(LocationVariable heap) |
boolean |
FunctionalAuxiliaryContract.hasModifiesClause(LocationVariable heap)
Returns
true iff the method (according to the contract) does not modify the heap
at all, i.e., iff it is "strictly pure." |
boolean |
FunctionalOperationContractImpl.hasModifiesClause(LocationVariable heap) |
boolean |
OperationContract.hasModifiesClause(LocationVariable heap)
Returns
true iff the method (according to the contract) does
not modify the heap at all, i.e., iff it is "strictly pure." |
boolean |
AuxiliaryContract.hasModifiesClause(LocationVariable heap)
Returns
true iff the method (according to the contract) does not modify the heap
at all, i.e., iff it is "strictly pure." |
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.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.
|
FunctionalOperationContract |
ContractFactory.addPre(FunctionalOperationContract old,
Term addedPre,
ProgramVariable selfVar,
ImmutableList<ProgramVariable> paramVars,
java.util.Map<LocationVariable,LocationVariable> atPreVars)
Returns another contract like this one, except that the passed term has been added as a
precondition.
|
protected abstract T |
AbstractAuxiliaryContractImpl.Creator.build(java.lang.String baseName,
StatementBlock block,
java.util.List<Label> labels,
IProgramMethod method,
Modality modality,
java.util.Map<LocationVariable,Term> preconditions,
java.util.Map<LocationVariable,Term> freePreconditions,
Term measuredBy,
java.util.Map<LocationVariable,Term> postconditions,
java.util.Map<LocationVariable,Term> freePostconditions,
java.util.Map<LocationVariable,Term> modifiesClauses,
ImmutableList<InfFlowSpec> infFlowSpecs,
AuxiliaryContract.Variables variables,
boolean transactionApplicable,
java.util.Map<LocationVariable,java.lang.Boolean> hasMod) |
protected abstract T |
AbstractAuxiliaryContractImpl.Creator.build(java.lang.String baseName,
StatementBlock block,
java.util.List<Label> labels,
IProgramMethod method,
Modality modality,
java.util.Map<LocationVariable,Term> preconditions,
java.util.Map<LocationVariable,Term> freePreconditions,
Term measuredBy,
java.util.Map<LocationVariable,Term> postconditions,
java.util.Map<LocationVariable,Term> freePostconditions,
java.util.Map<LocationVariable,Term> modifiesClauses,
ImmutableList<InfFlowSpec> infFlowSpecs,
AuxiliaryContract.Variables variables,
boolean transactionApplicable,
java.util.Map<LocationVariable,java.lang.Boolean> hasMod) |
protected abstract T |
AbstractAuxiliaryContractImpl.Creator.build(java.lang.String baseName,
StatementBlock block,
java.util.List<Label> labels,
IProgramMethod method,
Modality modality,
java.util.Map<LocationVariable,Term> preconditions,
java.util.Map<LocationVariable,Term> freePreconditions,
Term measuredBy,
java.util.Map<LocationVariable,Term> postconditions,
java.util.Map<LocationVariable,Term> freePostconditions,
java.util.Map<LocationVariable,Term> modifiesClauses,
ImmutableList<InfFlowSpec> infFlowSpecs,
AuxiliaryContract.Variables variables,
boolean transactionApplicable,
java.util.Map<LocationVariable,java.lang.Boolean> hasMod) |
protected abstract T |
AbstractAuxiliaryContractImpl.Creator.build(java.lang.String baseName,
StatementBlock block,
java.util.List<Label> labels,
IProgramMethod method,
Modality modality,
java.util.Map<LocationVariable,Term> preconditions,
java.util.Map<LocationVariable,Term> freePreconditions,
Term measuredBy,
java.util.Map<LocationVariable,Term> postconditions,
java.util.Map<LocationVariable,Term> freePostconditions,
java.util.Map<LocationVariable,Term> modifiesClauses,
ImmutableList<InfFlowSpec> infFlowSpecs,
AuxiliaryContract.Variables variables,
boolean transactionApplicable,
java.util.Map<LocationVariable,java.lang.Boolean> hasMod) |
protected abstract T |
AbstractAuxiliaryContractImpl.Creator.build(java.lang.String baseName,
StatementBlock block,
java.util.List<Label> labels,
IProgramMethod method,
Modality modality,
java.util.Map<LocationVariable,Term> preconditions,
java.util.Map<LocationVariable,Term> freePreconditions,
Term measuredBy,
java.util.Map<LocationVariable,Term> postconditions,
java.util.Map<LocationVariable,Term> freePostconditions,
java.util.Map<LocationVariable,Term> modifiesClauses,
ImmutableList<InfFlowSpec> infFlowSpecs,
AuxiliaryContract.Variables variables,
boolean transactionApplicable,
java.util.Map<LocationVariable,java.lang.Boolean> hasMod) |
protected abstract T |
AbstractAuxiliaryContractImpl.Creator.build(java.lang.String baseName,
StatementBlock block,
java.util.List<Label> labels,
IProgramMethod method,
Modality modality,
java.util.Map<LocationVariable,Term> preconditions,
java.util.Map<LocationVariable,Term> freePreconditions,
Term measuredBy,
java.util.Map<LocationVariable,Term> postconditions,
java.util.Map<LocationVariable,Term> freePostconditions,
java.util.Map<LocationVariable,Term> modifiesClauses,
ImmutableList<InfFlowSpec> infFlowSpecs,
AuxiliaryContract.Variables variables,
boolean transactionApplicable,
java.util.Map<LocationVariable,java.lang.Boolean> hasMod) |
protected BlockContract |
BlockContractImpl.Creator.build(java.lang.String baseName,
StatementBlock block,
java.util.List<Label> labels,
IProgramMethod method,
Modality modality,
java.util.Map<LocationVariable,Term> preconditions,
java.util.Map<LocationVariable,Term> freePreconditions,
Term measuredBy,
java.util.Map<LocationVariable,Term> postconditions,
java.util.Map<LocationVariable,Term> freePostconditions,
java.util.Map<LocationVariable,Term> modifiesClauses,
ImmutableList<InfFlowSpec> infFlowSpecs,
AuxiliaryContract.Variables variables,
boolean transactionApplicable,
java.util.Map<LocationVariable,java.lang.Boolean> hasMod) |
protected BlockContract |
BlockContractImpl.Creator.build(java.lang.String baseName,
StatementBlock block,
java.util.List<Label> labels,
IProgramMethod method,
Modality modality,
java.util.Map<LocationVariable,Term> preconditions,
java.util.Map<LocationVariable,Term> freePreconditions,
Term measuredBy,
java.util.Map<LocationVariable,Term> postconditions,
java.util.Map<LocationVariable,Term> freePostconditions,
java.util.Map<LocationVariable,Term> modifiesClauses,
ImmutableList<InfFlowSpec> infFlowSpecs,
AuxiliaryContract.Variables variables,
boolean transactionApplicable,
java.util.Map<LocationVariable,java.lang.Boolean> hasMod) |
protected BlockContract |
BlockContractImpl.Creator.build(java.lang.String baseName,
StatementBlock block,
java.util.List<Label> labels,
IProgramMethod method,
Modality modality,
java.util.Map<LocationVariable,Term> preconditions,
java.util.Map<LocationVariable,Term> freePreconditions,
Term measuredBy,
java.util.Map<LocationVariable,Term> postconditions,
java.util.Map<LocationVariable,Term> freePostconditions,
java.util.Map<LocationVariable,Term> modifiesClauses,
ImmutableList<InfFlowSpec> infFlowSpecs,
AuxiliaryContract.Variables variables,
boolean transactionApplicable,
java.util.Map<LocationVariable,java.lang.Boolean> hasMod) |
protected BlockContract |
BlockContractImpl.Creator.build(java.lang.String baseName,
StatementBlock block,
java.util.List<Label> labels,
IProgramMethod method,
Modality modality,
java.util.Map<LocationVariable,Term> preconditions,
java.util.Map<LocationVariable,Term> freePreconditions,
Term measuredBy,
java.util.Map<LocationVariable,Term> postconditions,
java.util.Map<LocationVariable,Term> freePostconditions,
java.util.Map<LocationVariable,Term> modifiesClauses,
ImmutableList<InfFlowSpec> infFlowSpecs,
AuxiliaryContract.Variables variables,
boolean transactionApplicable,
java.util.Map<LocationVariable,java.lang.Boolean> hasMod) |
protected BlockContract |
BlockContractImpl.Creator.build(java.lang.String baseName,
StatementBlock block,
java.util.List<Label> labels,
IProgramMethod method,
Modality modality,
java.util.Map<LocationVariable,Term> preconditions,
java.util.Map<LocationVariable,Term> freePreconditions,
Term measuredBy,
java.util.Map<LocationVariable,Term> postconditions,
java.util.Map<LocationVariable,Term> freePostconditions,
java.util.Map<LocationVariable,Term> modifiesClauses,
ImmutableList<InfFlowSpec> infFlowSpecs,
AuxiliaryContract.Variables variables,
boolean transactionApplicable,
java.util.Map<LocationVariable,java.lang.Boolean> hasMod) |
protected BlockContract |
BlockContractImpl.Creator.build(java.lang.String baseName,
StatementBlock block,
java.util.List<Label> labels,
IProgramMethod method,
Modality modality,
java.util.Map<LocationVariable,Term> preconditions,
java.util.Map<LocationVariable,Term> freePreconditions,
Term measuredBy,
java.util.Map<LocationVariable,Term> postconditions,
java.util.Map<LocationVariable,Term> freePostconditions,
java.util.Map<LocationVariable,Term> modifiesClauses,
ImmutableList<InfFlowSpec> infFlowSpecs,
AuxiliaryContract.Variables variables,
boolean transactionApplicable,
java.util.Map<LocationVariable,java.lang.Boolean> hasMod) |
protected LoopContract |
LoopContractImpl.Creator.build(java.lang.String baseName,
StatementBlock block,
java.util.List<Label> labels,
IProgramMethod method,
Modality modality,
java.util.Map<LocationVariable,Term> preconditions,
java.util.Map<LocationVariable,Term> freePreconditions,
Term measuredBy,
java.util.Map<LocationVariable,Term> postconditions,
java.util.Map<LocationVariable,Term> freePostconditions,
java.util.Map<LocationVariable,Term> modifiesClauses,
ImmutableList<InfFlowSpec> infFlowSpecs,
AuxiliaryContract.Variables variables,
boolean transactionApplicable,
java.util.Map<LocationVariable,java.lang.Boolean> hasMod) |
protected LoopContract |
LoopContractImpl.Creator.build(java.lang.String baseName,
StatementBlock block,
java.util.List<Label> labels,
IProgramMethod method,
Modality modality,
java.util.Map<LocationVariable,Term> preconditions,
java.util.Map<LocationVariable,Term> freePreconditions,
Term measuredBy,
java.util.Map<LocationVariable,Term> postconditions,
java.util.Map<LocationVariable,Term> freePostconditions,
java.util.Map<LocationVariable,Term> modifiesClauses,
ImmutableList<InfFlowSpec> infFlowSpecs,
AuxiliaryContract.Variables variables,
boolean transactionApplicable,
java.util.Map<LocationVariable,java.lang.Boolean> hasMod) |
protected LoopContract |
LoopContractImpl.Creator.build(java.lang.String baseName,
StatementBlock block,
java.util.List<Label> labels,
IProgramMethod method,
Modality modality,
java.util.Map<LocationVariable,Term> preconditions,
java.util.Map<LocationVariable,Term> freePreconditions,
Term measuredBy,
java.util.Map<LocationVariable,Term> postconditions,
java.util.Map<LocationVariable,Term> freePostconditions,
java.util.Map<LocationVariable,Term> modifiesClauses,
ImmutableList<InfFlowSpec> infFlowSpecs,
AuxiliaryContract.Variables variables,
boolean transactionApplicable,
java.util.Map<LocationVariable,java.lang.Boolean> hasMod) |
protected LoopContract |
LoopContractImpl.Creator.build(java.lang.String baseName,
StatementBlock block,
java.util.List<Label> labels,
IProgramMethod method,
Modality modality,
java.util.Map<LocationVariable,Term> preconditions,
java.util.Map<LocationVariable,Term> freePreconditions,
Term measuredBy,
java.util.Map<LocationVariable,Term> postconditions,
java.util.Map<LocationVariable,Term> freePostconditions,
java.util.Map<LocationVariable,Term> modifiesClauses,
ImmutableList<InfFlowSpec> infFlowSpecs,
AuxiliaryContract.Variables variables,
boolean transactionApplicable,
java.util.Map<LocationVariable,java.lang.Boolean> hasMod) |
protected LoopContract |
LoopContractImpl.Creator.build(java.lang.String baseName,
StatementBlock block,
java.util.List<Label> labels,
IProgramMethod method,
Modality modality,
java.util.Map<LocationVariable,Term> preconditions,
java.util.Map<LocationVariable,Term> freePreconditions,
Term measuredBy,
java.util.Map<LocationVariable,Term> postconditions,
java.util.Map<LocationVariable,Term> freePostconditions,
java.util.Map<LocationVariable,Term> modifiesClauses,
ImmutableList<InfFlowSpec> infFlowSpecs,
AuxiliaryContract.Variables variables,
boolean transactionApplicable,
java.util.Map<LocationVariable,java.lang.Boolean> hasMod) |
protected LoopContract |
LoopContractImpl.Creator.build(java.lang.String baseName,
StatementBlock block,
java.util.List<Label> labels,
IProgramMethod method,
Modality modality,
java.util.Map<LocationVariable,Term> preconditions,
java.util.Map<LocationVariable,Term> freePreconditions,
Term measuredBy,
java.util.Map<LocationVariable,Term> postconditions,
java.util.Map<LocationVariable,Term> freePostconditions,
java.util.Map<LocationVariable,Term> modifiesClauses,
ImmutableList<InfFlowSpec> infFlowSpecs,
AuxiliaryContract.Variables variables,
boolean transactionApplicable,
java.util.Map<LocationVariable,java.lang.Boolean> hasMod) |
LoopSpecification |
LoopSpecification.configurate(java.util.Map<LocationVariable,Term> invariants,
java.util.Map<LocationVariable,Term> freeInvariants,
java.util.Map<LocationVariable,Term> modifies,
java.util.Map<LocationVariable,ImmutableList<InfFlowSpec>> infFlowSpecs,
Term variant)
Configure the existing loop specification element with new elements,
i.e., loop invariant clauses, a loop variant, modifies clauses,
information flow specification elements, and a loop variant,
possibly together with (if any) "free" loop invariant clauses.
|
LoopSpecification |
LoopSpecification.configurate(java.util.Map<LocationVariable,Term> invariants,
java.util.Map<LocationVariable,Term> freeInvariants,
java.util.Map<LocationVariable,Term> modifies,
java.util.Map<LocationVariable,ImmutableList<InfFlowSpec>> infFlowSpecs,
Term variant)
Configure the existing loop specification element with new elements,
i.e., loop invariant clauses, a loop variant, modifies clauses,
information flow specification elements, and a loop variant,
possibly together with (if any) "free" loop invariant clauses.
|
LoopSpecification |
LoopSpecification.configurate(java.util.Map<LocationVariable,Term> invariants,
java.util.Map<LocationVariable,Term> freeInvariants,
java.util.Map<LocationVariable,Term> modifies,
java.util.Map<LocationVariable,ImmutableList<InfFlowSpec>> infFlowSpecs,
Term variant)
Configure the existing loop specification element with new elements,
i.e., loop invariant clauses, a loop variant, modifies clauses,
information flow specification elements, and a loop variant,
possibly together with (if any) "free" loop invariant clauses.
|
LoopSpecification |
LoopSpecification.configurate(java.util.Map<LocationVariable,Term> invariants,
java.util.Map<LocationVariable,Term> freeInvariants,
java.util.Map<LocationVariable,Term> modifies,
java.util.Map<LocationVariable,ImmutableList<InfFlowSpec>> infFlowSpecs,
Term variant)
Configure the existing loop specification element with new elements,
i.e., loop invariant clauses, a loop variant, modifies clauses,
information flow specification elements, and a loop variant,
possibly together with (if any) "free" loop invariant clauses.
|
LoopSpecification |
LoopSpecImpl.configurate(java.util.Map<LocationVariable,Term> invariants,
java.util.Map<LocationVariable,Term> freeInvariants,
java.util.Map<LocationVariable,Term> modifies,
java.util.Map<LocationVariable,ImmutableList<InfFlowSpec>> infFlowSpecs,
Term variant) |
LoopSpecification |
LoopSpecImpl.configurate(java.util.Map<LocationVariable,Term> invariants,
java.util.Map<LocationVariable,Term> freeInvariants,
java.util.Map<LocationVariable,Term> modifies,
java.util.Map<LocationVariable,ImmutableList<InfFlowSpec>> infFlowSpecs,
Term variant) |
LoopSpecification |
LoopSpecImpl.configurate(java.util.Map<LocationVariable,Term> invariants,
java.util.Map<LocationVariable,Term> freeInvariants,
java.util.Map<LocationVariable,Term> modifies,
java.util.Map<LocationVariable,ImmutableList<InfFlowSpec>> infFlowSpecs,
Term variant) |
LoopSpecification |
LoopSpecImpl.configurate(java.util.Map<LocationVariable,Term> invariants,
java.util.Map<LocationVariable,Term> freeInvariants,
java.util.Map<LocationVariable,Term> modifies,
java.util.Map<LocationVariable,ImmutableList<InfFlowSpec>> infFlowSpecs,
Term variant) |
LoopSpecification |
LoopSpecification.create(LoopStatement loop,
IProgramMethod pm,
KeYJavaType kjt,
java.util.Map<LocationVariable,Term> invariants,
java.util.Map<LocationVariable,Term> freeInvariants,
java.util.Map<LocationVariable,Term> modifies,
java.util.Map<LocationVariable,ImmutableList<InfFlowSpec>> infFlowSpecs,
Term variant,
Term selfTerm,
ImmutableList<Term> localIns,
ImmutableList<Term> localOuts,
java.util.Map<LocationVariable,Term> atPres)
Create and return a new loop specification element from the existing one
where the arguments given are replaced.
|
LoopSpecification |
LoopSpecification.create(LoopStatement loop,
IProgramMethod pm,
KeYJavaType kjt,
java.util.Map<LocationVariable,Term> invariants,
java.util.Map<LocationVariable,Term> freeInvariants,
java.util.Map<LocationVariable,Term> modifies,
java.util.Map<LocationVariable,ImmutableList<InfFlowSpec>> infFlowSpecs,
Term variant,
Term selfTerm,
ImmutableList<Term> localIns,
ImmutableList<Term> localOuts,
java.util.Map<LocationVariable,Term> atPres)
Create and return a new loop specification element from the existing one
where the arguments given are replaced.
|
LoopSpecification |
LoopSpecification.create(LoopStatement loop,
IProgramMethod pm,
KeYJavaType kjt,
java.util.Map<LocationVariable,Term> invariants,
java.util.Map<LocationVariable,Term> freeInvariants,
java.util.Map<LocationVariable,Term> modifies,
java.util.Map<LocationVariable,ImmutableList<InfFlowSpec>> infFlowSpecs,
Term variant,
Term selfTerm,
ImmutableList<Term> localIns,
ImmutableList<Term> localOuts,
java.util.Map<LocationVariable,Term> atPres)
Create and return a new loop specification element from the existing one
where the arguments given are replaced.
|
LoopSpecification |
LoopSpecification.create(LoopStatement loop,
IProgramMethod pm,
KeYJavaType kjt,
java.util.Map<LocationVariable,Term> invariants,
java.util.Map<LocationVariable,Term> freeInvariants,
java.util.Map<LocationVariable,Term> modifies,
java.util.Map<LocationVariable,ImmutableList<InfFlowSpec>> infFlowSpecs,
Term variant,
Term selfTerm,
ImmutableList<Term> localIns,
ImmutableList<Term> localOuts,
java.util.Map<LocationVariable,Term> atPres)
Create and return a new loop specification element from the existing one
where the arguments given are replaced.
|
LoopSpecification |
LoopSpecification.create(LoopStatement loop,
IProgramMethod pm,
KeYJavaType kjt,
java.util.Map<LocationVariable,Term> invariants,
java.util.Map<LocationVariable,Term> freeInvariants,
java.util.Map<LocationVariable,Term> modifies,
java.util.Map<LocationVariable,ImmutableList<InfFlowSpec>> infFlowSpecs,
Term variant,
Term selfTerm,
ImmutableList<Term> localIns,
ImmutableList<Term> localOuts,
java.util.Map<LocationVariable,Term> atPres)
Create and return a new loop specification element from the existing one
where the arguments given are replaced.
|
LoopSpecification |
LoopSpecImpl.create(LoopStatement loop,
IProgramMethod pm,
KeYJavaType kjt,
java.util.Map<LocationVariable,Term> invariants,
java.util.Map<LocationVariable,Term> freeInvariants,
java.util.Map<LocationVariable,Term> modifies,
java.util.Map<LocationVariable,ImmutableList<InfFlowSpec>> infFlowSpecs,
Term variant,
Term selfTerm,
ImmutableList<Term> localIns,
ImmutableList<Term> localOuts,
java.util.Map<LocationVariable,Term> atPres) |
LoopSpecification |
LoopSpecImpl.create(LoopStatement loop,
IProgramMethod pm,
KeYJavaType kjt,
java.util.Map<LocationVariable,Term> invariants,
java.util.Map<LocationVariable,Term> freeInvariants,
java.util.Map<LocationVariable,Term> modifies,
java.util.Map<LocationVariable,ImmutableList<InfFlowSpec>> infFlowSpecs,
Term variant,
Term selfTerm,
ImmutableList<Term> localIns,
ImmutableList<Term> localOuts,
java.util.Map<LocationVariable,Term> atPres) |
LoopSpecification |
LoopSpecImpl.create(LoopStatement loop,
IProgramMethod pm,
KeYJavaType kjt,
java.util.Map<LocationVariable,Term> invariants,
java.util.Map<LocationVariable,Term> freeInvariants,
java.util.Map<LocationVariable,Term> modifies,
java.util.Map<LocationVariable,ImmutableList<InfFlowSpec>> infFlowSpecs,
Term variant,
Term selfTerm,
ImmutableList<Term> localIns,
ImmutableList<Term> localOuts,
java.util.Map<LocationVariable,Term> atPres) |
LoopSpecification |
LoopSpecImpl.create(LoopStatement loop,
IProgramMethod pm,
KeYJavaType kjt,
java.util.Map<LocationVariable,Term> invariants,
java.util.Map<LocationVariable,Term> freeInvariants,
java.util.Map<LocationVariable,Term> modifies,
java.util.Map<LocationVariable,ImmutableList<InfFlowSpec>> infFlowSpecs,
Term variant,
Term selfTerm,
ImmutableList<Term> localIns,
ImmutableList<Term> localOuts,
java.util.Map<LocationVariable,Term> atPres) |
LoopSpecification |
LoopSpecImpl.create(LoopStatement loop,
IProgramMethod pm,
KeYJavaType kjt,
java.util.Map<LocationVariable,Term> invariants,
java.util.Map<LocationVariable,Term> freeInvariants,
java.util.Map<LocationVariable,Term> modifies,
java.util.Map<LocationVariable,ImmutableList<InfFlowSpec>> infFlowSpecs,
Term variant,
Term selfTerm,
ImmutableList<Term> localIns,
ImmutableList<Term> localOuts,
java.util.Map<LocationVariable,Term> atPres) |
LoopSpecification |
LoopSpecification.create(LoopStatement loop,
java.util.Map<LocationVariable,Term> invariants,
java.util.Map<LocationVariable,Term> freeInvariants,
java.util.Map<LocationVariable,Term> modifies,
java.util.Map<LocationVariable,ImmutableList<InfFlowSpec>> infFlowSpecs,
Term variant,
Term selfTerm,
ImmutableList<Term> localIns,
ImmutableList<Term> localOuts,
java.util.Map<LocationVariable,Term> atPres)
Create and return a new loop specification element from the existing one
where the arguments given are replaced.
|
LoopSpecification |
LoopSpecification.create(LoopStatement loop,
java.util.Map<LocationVariable,Term> invariants,
java.util.Map<LocationVariable,Term> freeInvariants,
java.util.Map<LocationVariable,Term> modifies,
java.util.Map<LocationVariable,ImmutableList<InfFlowSpec>> infFlowSpecs,
Term variant,
Term selfTerm,
ImmutableList<Term> localIns,
ImmutableList<Term> localOuts,
java.util.Map<LocationVariable,Term> atPres)
Create and return a new loop specification element from the existing one
where the arguments given are replaced.
|
LoopSpecification |
LoopSpecification.create(LoopStatement loop,
java.util.Map<LocationVariable,Term> invariants,
java.util.Map<LocationVariable,Term> freeInvariants,
java.util.Map<LocationVariable,Term> modifies,
java.util.Map<LocationVariable,ImmutableList<InfFlowSpec>> infFlowSpecs,
Term variant,
Term selfTerm,
ImmutableList<Term> localIns,
ImmutableList<Term> localOuts,
java.util.Map<LocationVariable,Term> atPres)
Create and return a new loop specification element from the existing one
where the arguments given are replaced.
|
LoopSpecification |
LoopSpecification.create(LoopStatement loop,
java.util.Map<LocationVariable,Term> invariants,
java.util.Map<LocationVariable,Term> freeInvariants,
java.util.Map<LocationVariable,Term> modifies,
java.util.Map<LocationVariable,ImmutableList<InfFlowSpec>> infFlowSpecs,
Term variant,
Term selfTerm,
ImmutableList<Term> localIns,
ImmutableList<Term> localOuts,
java.util.Map<LocationVariable,Term> atPres)
Create and return a new loop specification element from the existing one
where the arguments given are replaced.
|
LoopSpecification |
LoopSpecification.create(LoopStatement loop,
java.util.Map<LocationVariable,Term> invariants,
java.util.Map<LocationVariable,Term> freeInvariants,
java.util.Map<LocationVariable,Term> modifies,
java.util.Map<LocationVariable,ImmutableList<InfFlowSpec>> infFlowSpecs,
Term variant,
Term selfTerm,
ImmutableList<Term> localIns,
ImmutableList<Term> localOuts,
java.util.Map<LocationVariable,Term> atPres)
Create and return a new loop specification element from the existing one
where the arguments given are replaced.
|
LoopSpecification |
LoopSpecImpl.create(LoopStatement loop,
java.util.Map<LocationVariable,Term> invariants,
java.util.Map<LocationVariable,Term> freeInvariants,
java.util.Map<LocationVariable,Term> modifies,
java.util.Map<LocationVariable,ImmutableList<InfFlowSpec>> infFlowSpecs,
Term variant,
Term selfTerm,
ImmutableList<Term> localIns,
ImmutableList<Term> localOuts,
java.util.Map<LocationVariable,Term> atPres) |
LoopSpecification |
LoopSpecImpl.create(LoopStatement loop,
java.util.Map<LocationVariable,Term> invariants,
java.util.Map<LocationVariable,Term> freeInvariants,
java.util.Map<LocationVariable,Term> modifies,
java.util.Map<LocationVariable,ImmutableList<InfFlowSpec>> infFlowSpecs,
Term variant,
Term selfTerm,
ImmutableList<Term> localIns,
ImmutableList<Term> localOuts,
java.util.Map<LocationVariable,Term> atPres) |
LoopSpecification |
LoopSpecImpl.create(LoopStatement loop,
java.util.Map<LocationVariable,Term> invariants,
java.util.Map<LocationVariable,Term> freeInvariants,
java.util.Map<LocationVariable,Term> modifies,
java.util.Map<LocationVariable,ImmutableList<InfFlowSpec>> infFlowSpecs,
Term variant,
Term selfTerm,
ImmutableList<Term> localIns,
ImmutableList<Term> localOuts,
java.util.Map<LocationVariable,Term> atPres) |
LoopSpecification |
LoopSpecImpl.create(LoopStatement loop,
java.util.Map<LocationVariable,Term> invariants,
java.util.Map<LocationVariable,Term> freeInvariants,
java.util.Map<LocationVariable,Term> modifies,
java.util.Map<LocationVariable,ImmutableList<InfFlowSpec>> infFlowSpecs,
Term variant,
Term selfTerm,
ImmutableList<Term> localIns,
ImmutableList<Term> localOuts,
java.util.Map<LocationVariable,Term> atPres) |
LoopSpecification |
LoopSpecImpl.create(LoopStatement loop,
java.util.Map<LocationVariable,Term> invariants,
java.util.Map<LocationVariable,Term> freeInvariants,
java.util.Map<LocationVariable,Term> modifies,
java.util.Map<LocationVariable,ImmutableList<InfFlowSpec>> infFlowSpecs,
Term variant,
Term selfTerm,
ImmutableList<Term> localIns,
ImmutableList<Term> localOuts,
java.util.Map<LocationVariable,Term> atPres) |
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) |
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,
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,
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,
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,
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,
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,
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,
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,
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,
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,
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,
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,
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.
|
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.
|
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.
|
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.
|
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.
|
java.util.ArrayList<AbstractionPredicate> |
PredicateAbstractionMergeContract.getAbstractionPredicates(java.util.Map<LocationVariable,Term> atPres,
Services services)
TODO
|
static java.util.Map<LocationVariable,Term> |
HeapContext.getAtPres(java.util.Map<LocationVariable,LocationVariable> atPreVars,
Services services) |
static java.util.Map<LocationVariable,Term> |
HeapContext.getAtPres(java.util.Map<LocationVariable,LocationVariable> atPreVars,
Services services) |
static java.util.Map<LocationVariable,LocationVariable> |
HeapContext.getBeforeAtPreVars(java.util.List<LocationVariable> heaps,
TermServices services,
java.lang.String contextName) |
Term |
FunctionalAuxiliaryContract.getDep(LocationVariable heap,
boolean atPre,
ProgramVariable selfVar,
ImmutableList<ProgramVariable> paramVars,
java.util.Map<LocationVariable,? extends ProgramVariable> atPreVars,
Services services) |
Term |
FunctionalOperationContractImpl.getDep(LocationVariable heap,
boolean atPre,
ProgramVariable selfVar,
ImmutableList<ProgramVariable> paramVars,
java.util.Map<LocationVariable,? extends ProgramVariable> atPreVars,
Services services) |
Term |
InformationFlowContractImpl.getDep(LocationVariable heap,
boolean atPre,
ProgramVariable selfVar,
ImmutableList<ProgramVariable> paramVars,
java.util.Map<LocationVariable,? extends ProgramVariable> atPreVars,
Services services) |
Term |
DependencyContractImpl.getDep(LocationVariable heap,
boolean atPre,
ProgramVariable selfVar,
ImmutableList<ProgramVariable> paramVars,
java.util.Map<LocationVariable,? extends ProgramVariable> atPreVars,
Services services) |
Term |
WellDefinednessCheck.getDep(LocationVariable heap,
boolean atPre,
ProgramVariable selfVar,
ImmutableList<ProgramVariable> paramVars,
java.util.Map<LocationVariable,? extends ProgramVariable> atPreVars,
Services services)
Deprecated.
|
Term |
Contract.getDep(LocationVariable heap,
boolean atPre,
ProgramVariable selfVar,
ImmutableList<ProgramVariable> paramVars,
java.util.Map<LocationVariable,? extends ProgramVariable> atPreVars,
Services services)
Returns the dependency set of the contract.
|
Term |
FunctionalAuxiliaryContract.getDep(LocationVariable heap,
boolean atPre,
Term heapTerm,
Term selfTerm,
ImmutableList<Term> paramTerms,
java.util.Map<LocationVariable,Term> atPres,
Services services) |
Term |
FunctionalOperationContractImpl.getDep(LocationVariable heap,
boolean atPre,
Term heapTerm,
Term selfTerm,
ImmutableList<Term> paramTerms,
java.util.Map<LocationVariable,Term> atPres,
Services services) |
Term |
InformationFlowContractImpl.getDep(LocationVariable heap,
boolean atPre,
Term heapTerm,
Term selfTerm,
ImmutableList<Term> paramTerms,
java.util.Map<LocationVariable,Term> atPres,
Services services) |
Term |
DependencyContractImpl.getDep(LocationVariable heap,
boolean atPre,
Term heapTerm,
Term selfTerm,
ImmutableList<Term> paramTerms,
java.util.Map<LocationVariable,Term> atPres,
Services services) |
Term |
WellDefinednessCheck.getDep(LocationVariable heap,
boolean atPre,
Term heapTerm,
Term selfTerm,
ImmutableList<Term> paramTerms,
java.util.Map<LocationVariable,Term> atPres,
Services services)
Deprecated.
|
Term |
Contract.getDep(LocationVariable heap,
boolean atPre,
Term heapTerm,
Term selfTerm,
ImmutableList<Term> paramTerms,
java.util.Map<LocationVariable,Term> atPres,
Services services)
Returns the dependency set of the contract.
|
Term |
LoopSpecification.getFreeInvariant(LocationVariable heap,
Term selfTerm,
java.util.Map<LocationVariable,Term> atPres,
Services services)
Returns the free invariant formula.
|
Term |
LoopSpecImpl.getFreeInvariant(LocationVariable heap,
Term selfTerm,
java.util.Map<LocationVariable,Term> atPres,
Services services) |
Term |
FunctionalOperationContractImpl.getFreePost(java.util.List<LocationVariable> heapContext,
java.util.Map<LocationVariable,Term> heapTerms,
Term selfTerm,
ImmutableList<Term> paramTerms,
Term resultTerm,
Term excTerm,
java.util.Map<LocationVariable,Term> atPres,
Services services) |
Term |
FunctionalOperationContractImpl.getFreePost(java.util.List<LocationVariable> heapContext,
java.util.Map<LocationVariable,Term> heapTerms,
Term selfTerm,
ImmutableList<Term> paramTerms,
Term resultTerm,
Term excTerm,
java.util.Map<LocationVariable,Term> atPres,
Services services) |
Term |
FunctionalOperationContractImpl.getFreePost(java.util.List<LocationVariable> heapContext,
java.util.Map<LocationVariable,Term> heapTerms,
Term selfTerm,
ImmutableList<Term> paramTerms,
Term resultTerm,
Term excTerm,
java.util.Map<LocationVariable,Term> atPres,
Services services) |
Term |
FunctionalOperationContract.getFreePost(java.util.List<LocationVariable> heapContext,
java.util.Map<LocationVariable,Term> heapTerms,
Term selfTerm,
ImmutableList<Term> paramTerms,
Term resultTerm,
Term excTerm,
java.util.Map<LocationVariable,Term> atPres,
Services services) |
Term |
FunctionalOperationContract.getFreePost(java.util.List<LocationVariable> heapContext,
java.util.Map<LocationVariable,Term> heapTerms,
Term selfTerm,
ImmutableList<Term> paramTerms,
Term resultTerm,
Term excTerm,
java.util.Map<LocationVariable,Term> atPres,
Services services) |
Term |
FunctionalOperationContract.getFreePost(java.util.List<LocationVariable> heapContext,
java.util.Map<LocationVariable,Term> heapTerms,
Term selfTerm,
ImmutableList<Term> paramTerms,
Term resultTerm,
Term excTerm,
java.util.Map<LocationVariable,Term> atPres,
Services services) |
Term |
FunctionalOperationContractImpl.getFreePost(LocationVariable heap,
ProgramVariable selfVar,
ImmutableList<ProgramVariable> paramVars,
ProgramVariable resultVar,
ProgramVariable excVar,
java.util.Map<LocationVariable,? extends ProgramVariable> atPreVars,
Services services) |
Term |
FunctionalOperationContract.getFreePost(LocationVariable heap,
ProgramVariable selfVar,
ImmutableList<ProgramVariable> paramVars,
ProgramVariable resultVar,
ProgramVariable excVar,
java.util.Map<LocationVariable,? extends ProgramVariable> atPreVars,
Services services) |
Term |
FunctionalOperationContractImpl.getFreePost(LocationVariable heap,
Term heapTerm,
Term selfTerm,
ImmutableList<Term> paramTerms,
Term resultTerm,
Term excTerm,
java.util.Map<LocationVariable,Term> atPres,
Services services) |
Term |
FunctionalOperationContract.getFreePost(LocationVariable heap,
Term heapTerm,
Term selfTerm,
ImmutableList<Term> paramTerms,
Term resultTerm,
Term excTerm,
java.util.Map<LocationVariable,Term> atPres,
Services services) |
Term |
FunctionalOperationContractImpl.getFreePre(java.util.List<LocationVariable> heapContext,
ProgramVariable selfVar,
ImmutableList<ProgramVariable> paramVars,
java.util.Map<LocationVariable,? extends ProgramVariable> atPreVars,
Services services) |
Term |
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 |
OperationContract.getFreePre(LocationVariable heap,
ProgramVariable selfVar,
ImmutableList<ProgramVariable> paramVars,
java.util.Map<LocationVariable,? extends ProgramVariable> atPreVars,
Services services) |
Term |
FunctionalOperationContractImpl.getFreePre(LocationVariable heap,
Term heapTerm,
Term selfTerm,
ImmutableList<Term> paramTerms,
java.util.Map<LocationVariable,Term> atPres,
Services services) |
Term |
OperationContract.getFreePre(LocationVariable heap,
Term heapTerm,
Term selfTerm,
ImmutableList<Term> paramTerms,
java.util.Map<LocationVariable,Term> atPres,
Services services) |
Term |
AbstractAuxiliaryContractImpl.getFreePrecondition(LocationVariable heap,
ProgramVariable self,
java.util.Map<LocationVariable,LocationVariable> atPres,
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 |
AuxiliaryContract.getFreePrecondition(LocationVariable heap,
ProgramVariable self,
java.util.Map<LocationVariable,LocationVariable> atPres,
Services services) |
Term |
AbstractAuxiliaryContractImpl.getFreePrecondition(LocationVariable heapVariable,
Term heap,
Term self,
java.util.Map<LocationVariable,Term> atPres,
Services services) |
Term |
AuxiliaryContract.getFreePrecondition(LocationVariable heapVariable,
Term heap,
Term self,
java.util.Map<LocationVariable,Term> atPres,
Services services) |
ImmutableList<InfFlowSpec> |
LoopSpecification.getInfFlowSpecs(LocationVariable heap,
Term selfTerm,
java.util.Map<LocationVariable,Term> atPres,
Services services) |
ImmutableList<InfFlowSpec> |
LoopSpecImpl.getInfFlowSpecs(LocationVariable heap,
Term selfTerm,
java.util.Map<LocationVariable,Term> atPres,
Services services) |
Term |
LoopSpecification.getInvariant(LocationVariable heap,
Term selfTerm,
java.util.Map<LocationVariable,Term> atPres,
Services services)
Returns the invariant formula.
|
Term |
LoopSpecImpl.getInvariant(LocationVariable heap,
Term selfTerm,
java.util.Map<LocationVariable,Term> atPres,
Services services) |
Term |
FunctionalAuxiliaryContract.getMby(java.util.Map<LocationVariable,Term> heapTerms,
Term selfTerm,
ImmutableList<Term> paramTerms,
java.util.Map<LocationVariable,Term> atPres,
Services services) |
Term |
FunctionalAuxiliaryContract.getMby(java.util.Map<LocationVariable,Term> heapTerms,
Term selfTerm,
ImmutableList<Term> paramTerms,
java.util.Map<LocationVariable,Term> atPres,
Services services) |
Term |
FunctionalOperationContractImpl.getMby(java.util.Map<LocationVariable,Term> heapTerms,
Term selfTerm,
ImmutableList<Term> paramTerms,
java.util.Map<LocationVariable,Term> atPres,
Services services) |
Term |
FunctionalOperationContractImpl.getMby(java.util.Map<LocationVariable,Term> heapTerms,
Term selfTerm,
ImmutableList<Term> paramTerms,
java.util.Map<LocationVariable,Term> atPres,
Services services) |
Term |
InformationFlowContractImpl.getMby(java.util.Map<LocationVariable,Term> heapTerms,
Term selfTerm,
ImmutableList<Term> paramTerms,
java.util.Map<LocationVariable,Term> atPres,
Services services)
Deprecated.
|
Term |
InformationFlowContractImpl.getMby(java.util.Map<LocationVariable,Term> heapTerms,
Term selfTerm,
ImmutableList<Term> paramTerms,
java.util.Map<LocationVariable,Term> atPres,
Services services)
Deprecated.
|
Term |
DependencyContractImpl.getMby(java.util.Map<LocationVariable,Term> heapTerms,
Term selfTerm,
ImmutableList<Term> paramTerms,
java.util.Map<LocationVariable,Term> atPres,
Services services) |
Term |
DependencyContractImpl.getMby(java.util.Map<LocationVariable,Term> heapTerms,
Term selfTerm,
ImmutableList<Term> paramTerms,
java.util.Map<LocationVariable,Term> atPres,
Services services) |
Term |
WellDefinednessCheck.getMby(java.util.Map<LocationVariable,Term> heapTerms,
Term selfTerm,
ImmutableList<Term> paramTerms,
java.util.Map<LocationVariable,Term> atPres,
Services services)
Deprecated.
|
Term |
WellDefinednessCheck.getMby(java.util.Map<LocationVariable,Term> heapTerms,
Term selfTerm,
ImmutableList<Term> paramTerms,
java.util.Map<LocationVariable,Term> atPres,
Services services)
Deprecated.
|
Term |
Contract.getMby(java.util.Map<LocationVariable,Term> heapTerms,
Term selfTerm,
ImmutableList<Term> paramTerms,
java.util.Map<LocationVariable,Term> atPres,
Services services)
Returns the measured_by clause of the contract.
|
Term |
Contract.getMby(java.util.Map<LocationVariable,Term> heapTerms,
Term selfTerm,
ImmutableList<Term> paramTerms,
java.util.Map<LocationVariable,Term> atPres,
Services services)
Returns the measured_by clause of the contract.
|
Term |
AbstractAuxiliaryContractImpl.getMby(java.util.Map<LocationVariable,Term> heapTerms,
Term selfTerm,
java.util.Map<LocationVariable,Term> atPres,
Services services) |
Term |
AbstractAuxiliaryContractImpl.getMby(java.util.Map<LocationVariable,Term> heapTerms,
Term selfTerm,
java.util.Map<LocationVariable,Term> atPres,
Services services) |
Term |
AuxiliaryContract.getMby(java.util.Map<LocationVariable,Term> heapTerms,
Term selfTerm,
java.util.Map<LocationVariable,Term> atPres,
Services services) |
Term |
AuxiliaryContract.getMby(java.util.Map<LocationVariable,Term> heapTerms,
Term selfTerm,
java.util.Map<LocationVariable,Term> atPres,
Services services) |
Term |
LoopSpecification.getModifies(LocationVariable heap,
Term selfTerm,
java.util.Map<LocationVariable,Term> atPres,
Services services)
Returns the modifies clause.
|
Term |
LoopSpecImpl.getModifies(LocationVariable heap,
Term selfTerm,
java.util.Map<LocationVariable,Term> atPres,
Services services) |
Term |
LoopSpecification.getModifies(Term selfTerm,
java.util.Map<LocationVariable,Term> atPres,
Services services)
Returns the modifies clause.
|
Term |
LoopSpecImpl.getModifies(Term selfTerm,
java.util.Map<LocationVariable,Term> atPres,
Services services) |
java.lang.String |
LoopSpecification.getPlainText(Services services,
java.lang.Iterable<LocationVariable> heapContext,
boolean usePrettyPrinting,
boolean useUnicodeSymbols)
Returns the invariant in pretty plain text format.
|
java.lang.String |
LoopSpecImpl.getPlainText(Services services,
java.lang.Iterable<LocationVariable> heapContext,
boolean usePrettyPrinting,
boolean useUnicodeSymbols) |
Term |
FunctionalOperationContractImpl.getPost(java.util.List<LocationVariable> heapContext,
java.util.Map<LocationVariable,Term> heapTerms,
Term selfTerm,
ImmutableList<Term> paramTerms,
Term resultTerm,
Term excTerm,
java.util.Map<LocationVariable,Term> atPres,
Services services) |
Term |
FunctionalOperationContractImpl.getPost(java.util.List<LocationVariable> heapContext,
java.util.Map<LocationVariable,Term> heapTerms,
Term selfTerm,
ImmutableList<Term> paramTerms,
Term resultTerm,
Term excTerm,
java.util.Map<LocationVariable,Term> atPres,
Services services) |
Term |
FunctionalOperationContractImpl.getPost(java.util.List<LocationVariable> heapContext,
java.util.Map<LocationVariable,Term> heapTerms,
Term selfTerm,
ImmutableList<Term> paramTerms,
Term resultTerm,
Term excTerm,
java.util.Map<LocationVariable,Term> atPres,
Services services) |
Term |
FunctionalOperationContract.getPost(java.util.List<LocationVariable> heapContext,
java.util.Map<LocationVariable,Term> heapTerms,
Term selfTerm,
ImmutableList<Term> paramTerms,
Term resultTerm,
Term excTerm,
java.util.Map<LocationVariable,Term> atPres,
Services services) |
Term |
FunctionalOperationContract.getPost(java.util.List<LocationVariable> heapContext,
java.util.Map<LocationVariable,Term> heapTerms,
Term selfTerm,
ImmutableList<Term> paramTerms,
Term resultTerm,
Term excTerm,
java.util.Map<LocationVariable,Term> atPres,
Services services) |
Term |
FunctionalOperationContract.getPost(java.util.List<LocationVariable> heapContext,
java.util.Map<LocationVariable,Term> heapTerms,
Term selfTerm,
ImmutableList<Term> paramTerms,
Term resultTerm,
Term excTerm,
java.util.Map<LocationVariable,Term> atPres,
Services services) |
Term |
FunctionalOperationContractImpl.getPost(java.util.List<LocationVariable> heapContext,
ProgramVariable selfVar,
ImmutableList<ProgramVariable> paramVars,
ProgramVariable resultVar,
ProgramVariable excVar,
java.util.Map<LocationVariable,? extends ProgramVariable> atPreVars,
Services services) |
Term |
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 |
FunctionalOperationContract.getPost(LocationVariable heap,
ProgramVariable selfVar,
ImmutableList<ProgramVariable> paramVars,
ProgramVariable resultVar,
ProgramVariable excVar,
java.util.Map<LocationVariable,? extends ProgramVariable> atPreVars,
Services services)
Returns the postcondition of the contract.
|
Term |
FunctionalOperationContractImpl.getPost(LocationVariable heap,
Term heapTerm,
Term selfTerm,
ImmutableList<Term> paramTerms,
Term resultTerm,
Term excTerm,
java.util.Map<LocationVariable,Term> atPres,
Services services) |
Term |
FunctionalOperationContract.getPost(LocationVariable heap,
Term heapTerm,
Term selfTerm,
ImmutableList<Term> paramTerms,
Term resultTerm,
Term excTerm,
java.util.Map<LocationVariable,Term> atPres,
Services services)
Returns the postcondition of the contract.
|
Term |
FunctionalAuxiliaryContract.getPre(java.util.List<LocationVariable> heapContext,
java.util.Map<LocationVariable,Term> heapTerms,
Term selfTerm,
ImmutableList<Term> paramTerms,
java.util.Map<LocationVariable,Term> atPres,
Services services) |
Term |
FunctionalAuxiliaryContract.getPre(java.util.List<LocationVariable> heapContext,
java.util.Map<LocationVariable,Term> heapTerms,
Term selfTerm,
ImmutableList<Term> paramTerms,
java.util.Map<LocationVariable,Term> atPres,
Services services) |
Term |
FunctionalAuxiliaryContract.getPre(java.util.List<LocationVariable> heapContext,
java.util.Map<LocationVariable,Term> heapTerms,
Term selfTerm,
ImmutableList<Term> paramTerms,
java.util.Map<LocationVariable,Term> atPres,
Services services) |
Term |
FunctionalOperationContractImpl.getPre(java.util.List<LocationVariable> heapContext,
java.util.Map<LocationVariable,Term> heapTerms,
Term selfTerm,
ImmutableList<Term> paramTerms,
java.util.Map<LocationVariable,Term> atPres,
Services services) |
Term |
FunctionalOperationContractImpl.getPre(java.util.List<LocationVariable> heapContext,
java.util.Map<LocationVariable,Term> heapTerms,
Term selfTerm,
ImmutableList<Term> paramTerms,
java.util.Map<LocationVariable,Term> atPres,
Services services) |
Term |
FunctionalOperationContractImpl.getPre(java.util.List<LocationVariable> heapContext,
java.util.Map<LocationVariable,Term> heapTerms,
Term selfTerm,
ImmutableList<Term> paramTerms,
java.util.Map<LocationVariable,Term> atPres,
Services services) |
Term |
InformationFlowContractImpl.getPre(java.util.List<LocationVariable> heapContext,
java.util.Map<LocationVariable,Term> heapTerms,
Term selfTerm,
ImmutableList<Term> paramTerms,
java.util.Map<LocationVariable,Term> atPres,
Services services)
Deprecated.
|
Term |
InformationFlowContractImpl.getPre(java.util.List<LocationVariable> heapContext,
java.util.Map<LocationVariable,Term> heapTerms,
Term selfTerm,
ImmutableList<Term> paramTerms,
java.util.Map<LocationVariable,Term> atPres,
Services services)
Deprecated.
|
Term |
InformationFlowContractImpl.getPre(java.util.List<LocationVariable> heapContext,
java.util.Map<LocationVariable,Term> heapTerms,
Term selfTerm,
ImmutableList<Term> paramTerms,
java.util.Map<LocationVariable,Term> atPres,
Services services)
Deprecated.
|
Term |
DependencyContractImpl.getPre(java.util.List<LocationVariable> heapContext,
java.util.Map<LocationVariable,Term> heapTerms,
Term selfTerm,
ImmutableList<Term> paramTerms,
java.util.Map<LocationVariable,Term> atPres,
Services services) |
Term |
DependencyContractImpl.getPre(java.util.List<LocationVariable> heapContext,
java.util.Map<LocationVariable,Term> heapTerms,
Term selfTerm,
ImmutableList<Term> paramTerms,
java.util.Map<LocationVariable,Term> atPres,
Services services) |
Term |
DependencyContractImpl.getPre(java.util.List<LocationVariable> heapContext,
java.util.Map<LocationVariable,Term> heapTerms,
Term selfTerm,
ImmutableList<Term> paramTerms,
java.util.Map<LocationVariable,Term> atPres,
Services services) |
Term |
WellDefinednessCheck.getPre(java.util.List<LocationVariable> heapContext,
java.util.Map<LocationVariable,Term> heapTerms,
Term selfTerm,
ImmutableList<Term> paramTerms,
java.util.Map<LocationVariable,Term> atPres,
Services services)
Deprecated.
|
Term |
WellDefinednessCheck.getPre(java.util.List<LocationVariable> heapContext,
java.util.Map<LocationVariable,Term> heapTerms,
Term selfTerm,
ImmutableList<Term> paramTerms,
java.util.Map<LocationVariable,Term> atPres,
Services services)
Deprecated.
|
Term |
WellDefinednessCheck.getPre(java.util.List<LocationVariable> heapContext,
java.util.Map<LocationVariable,Term> heapTerms,
Term selfTerm,
ImmutableList<Term> paramTerms,
java.util.Map<LocationVariable,Term> atPres,
Services services)
Deprecated.
|
Term |
Contract.getPre(java.util.List<LocationVariable> heapContext,
java.util.Map<LocationVariable,Term> heapTerms,
Term selfTerm,
ImmutableList<Term> paramTerms,
java.util.Map<LocationVariable,Term> atPres,
Services services)
Returns the precondition of the contract.
|
Term |
Contract.getPre(java.util.List<LocationVariable> heapContext,
java.util.Map<LocationVariable,Term> heapTerms,
Term selfTerm,
ImmutableList<Term> paramTerms,
java.util.Map<LocationVariable,Term> atPres,
Services services)
Returns the precondition of the contract.
|
Term |
Contract.getPre(java.util.List<LocationVariable> heapContext,
java.util.Map<LocationVariable,Term> heapTerms,
Term selfTerm,
ImmutableList<Term> paramTerms,
java.util.Map<LocationVariable,Term> atPres,
Services services)
Returns the precondition of the contract.
|
Term |
FunctionalAuxiliaryContract.getPre(java.util.List<LocationVariable> heapContext,
ProgramVariable selfVar,
ImmutableList<ProgramVariable> paramVars,
java.util.Map<LocationVariable,? extends ProgramVariable> atPreVars,
Services services) |
Term |
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 |
FunctionalOperationContractImpl.getPre(LocationVariable heap,
ProgramVariable selfVar,
ImmutableList<ProgramVariable> paramVars,
java.util.Map<LocationVariable,? extends ProgramVariable> atPreVars,
Services services) |
Term |
InformationFlowContractImpl.getPre(LocationVariable heap,
ProgramVariable selfVar,
ImmutableList<ProgramVariable> paramVars,
java.util.Map<LocationVariable,? extends ProgramVariable> atPreVars,
Services services)
Deprecated.
|
Term |
DependencyContractImpl.getPre(LocationVariable heap,
ProgramVariable selfVar,
ImmutableList<ProgramVariable> paramVars,
java.util.Map<LocationVariable,? extends ProgramVariable> atPreVars,
Services services) |
Term |
WellDefinednessCheck.getPre(LocationVariable heap,
ProgramVariable selfVar,
ImmutableList<ProgramVariable> paramVars,
java.util.Map<LocationVariable,? extends ProgramVariable> atPreVars,
Services services)
Deprecated.
|
Term |
Contract.getPre(LocationVariable heap,
ProgramVariable selfVar,
ImmutableList<ProgramVariable> paramVars,
java.util.Map<LocationVariable,? extends ProgramVariable> atPreVars,
Services services)
Returns the precondition of the contract.
|
Term |
FunctionalAuxiliaryContract.getPre(LocationVariable heap,
Term heapTerm,
Term selfTerm,
ImmutableList<Term> paramTerms,
java.util.Map<LocationVariable,Term> atPres,
Services services) |
Term |
FunctionalOperationContractImpl.getPre(LocationVariable heap,
Term heapTerm,
Term selfTerm,
ImmutableList<Term> paramTerms,
java.util.Map<LocationVariable,Term> atPres,
Services services) |
Term |
InformationFlowContractImpl.getPre(LocationVariable heap,
Term heapTerm,
Term selfTerm,
ImmutableList<Term> paramTerms,
java.util.Map<LocationVariable,Term> atPres,
Services services)
Deprecated.
|
Term |
DependencyContractImpl.getPre(LocationVariable heap,
Term heapTerm,
Term selfTerm,
ImmutableList<Term> paramTerms,
java.util.Map<LocationVariable,Term> atPres,
Services services) |
Term |
WellDefinednessCheck.getPre(LocationVariable heap,
Term heapTerm,
Term selfTerm,
ImmutableList<Term> paramTerms,
java.util.Map<LocationVariable,Term> atPres,
Services services)
Deprecated.
|
Term |
Contract.getPre(LocationVariable heap,
Term heapTerm,
Term selfTerm,
ImmutableList<Term> paramTerms,
java.util.Map<LocationVariable,Term> atPres,
Services services)
Returns the precondition of the contract.
|
Term |
AbstractAuxiliaryContractImpl.getPrecondition(LocationVariable heap,
ProgramVariable self,
java.util.Map<LocationVariable,LocationVariable> atPres,
Services services) |
Term |
AbstractAuxiliaryContractImpl.getPrecondition(LocationVariable heap,
ProgramVariable self,
java.util.Map<LocationVariable,LocationVariable> atPres,
Services services) |
Term |
AuxiliaryContract.getPrecondition(LocationVariable heap,
ProgramVariable self,
java.util.Map<LocationVariable,LocationVariable> atPres,
Services services) |
Term |
AuxiliaryContract.getPrecondition(LocationVariable heap,
ProgramVariable self,
java.util.Map<LocationVariable,LocationVariable> atPres,
Services services) |
Term |
AbstractAuxiliaryContractImpl.getPrecondition(LocationVariable heapVariable,
Term heap,
Term self,
java.util.Map<LocationVariable,Term> atPres,
Services services) |
Term |
AuxiliaryContract.getPrecondition(LocationVariable heapVariable,
Term heap,
Term self,
java.util.Map<LocationVariable,Term> atPres,
Services services) |
protected java.util.Map<Term,Term> |
FunctionalOperationContractImpl.getReplaceMap(java.util.Map<LocationVariable,Term> heapTerms,
Term selfTerm,
ImmutableList<Term> paramTerms,
Term resultTerm,
Term excTerm,
java.util.Map<LocationVariable,Term> atPres,
Services services)
Get the according replace map for the given variable terms.
|
protected java.util.Map<Term,Term> |
FunctionalOperationContractImpl.getReplaceMap(java.util.Map<LocationVariable,Term> heapTerms,
Term selfTerm,
ImmutableList<Term> paramTerms,
Term resultTerm,
Term excTerm,
java.util.Map<LocationVariable,Term> atPres,
Services services)
Get the according replace map for the given variable terms.
|
protected java.util.Map<ProgramVariable,ProgramVariable> |
FunctionalOperationContractImpl.getReplaceMap(ProgramVariable selfVar,
ImmutableList<ProgramVariable> paramVars,
ProgramVariable resultVar,
ProgramVariable excVar,
java.util.Map<LocationVariable,? extends ProgramVariable> atPreVars,
Services services)
Get the according replace map for the given variables.
|
Term |
FunctionalOperationContractImpl.getRepresentsAxiom(LocationVariable heap,
ProgramVariable selfVar,
ImmutableList<ProgramVariable> paramVars,
ProgramVariable resultVar,
java.util.Map<LocationVariable,? extends ProgramVariable> atPreVars,
Services services) |
Term |
FunctionalOperationContract.getRepresentsAxiom(LocationVariable heap,
ProgramVariable selfVar,
ImmutableList<ProgramVariable> paramVars,
ProgramVariable resultVar,
java.util.Map<LocationVariable,? extends ProgramVariable> atPreVars,
Services services)
Returns the model method definition for model method contracts
|
Term |
FunctionalOperationContractImpl.getRepresentsAxiom(LocationVariable heap,
Term heapTerm,
Term selfTerm,
ImmutableList<Term> paramTerms,
Term resultTerm,
Term excTerm,
java.util.Map<LocationVariable,Term> atPres,
Services services) |
Term |
FunctionalOperationContract.getRepresentsAxiom(LocationVariable heap,
Term heapTerm,
Term selfTerm,
ImmutableList<Term> paramTerms,
Term resultTerm,
Term excTerm,
java.util.Map<LocationVariable,Term> atPres,
Services services) |
static java.lang.String |
FunctionalOperationContractImpl.getText(FunctionalOperationContract contract,
ImmutableList<Term> contractParams,
Term resultTerm,
Term contractSelf,
Term excTerm,
LocationVariable baseHeap,
Term baseHeapTerm,
java.util.List<LocationVariable> heapContext,
java.util.Map<LocationVariable,Term> atPres,
boolean includeHtmlMarkup,
Services services,
boolean usePrettyPrinting,
boolean useUnicodeSymbols) |
static java.lang.String |
FunctionalOperationContractImpl.getText(FunctionalOperationContract contract,
ImmutableList<Term> contractParams,
Term resultTerm,
Term contractSelf,
Term excTerm,
LocationVariable baseHeap,
Term baseHeapTerm,
java.util.List<LocationVariable> heapContext,
java.util.Map<LocationVariable,Term> atPres,
boolean includeHtmlMarkup,
Services services,
boolean usePrettyPrinting,
boolean useUnicodeSymbols) |
Term |
LoopSpecification.getVariant(Term selfTerm,
java.util.Map<LocationVariable,Term> atPres,
Services services)
Returns the variant term.
|
Term |
LoopSpecImpl.getVariant(Term selfTerm,
java.util.Map<LocationVariable,Term> atPres,
Services services) |
LoopSpecification |
LoopSpecification.instantiate(java.util.Map<LocationVariable,Term> invariants,
java.util.Map<LocationVariable,Term> freeInvariants,
Term variant)
Instantiate a (raw) loop specification with loop invariant clauses and
a loop variant, possibly together with (if any) "free" loop invariant
clauses.
|
LoopSpecification |
LoopSpecification.instantiate(java.util.Map<LocationVariable,Term> invariants,
java.util.Map<LocationVariable,Term> freeInvariants,
Term variant)
Instantiate a (raw) loop specification with loop invariant clauses and
a loop variant, possibly together with (if any) "free" loop invariant
clauses.
|
LoopSpecification |
LoopSpecImpl.instantiate(java.util.Map<LocationVariable,Term> invariants,
java.util.Map<LocationVariable,Term> freeInvariants,
Term variant) |
LoopSpecification |
LoopSpecImpl.instantiate(java.util.Map<LocationVariable,Term> invariants,
java.util.Map<LocationVariable,Term> freeInvariants,
Term variant) |
LoopSpecification |
LoopSpecification.setInvariant(java.util.Map<LocationVariable,Term> invariants,
java.util.Map<LocationVariable,Term> freeInvariants,
Term selfTerm,
java.util.Map<LocationVariable,Term> atPres,
Services services)
Returns a new loop invariant where the invariant formula has been
replaced with the passed one.
|
LoopSpecification |
LoopSpecification.setInvariant(java.util.Map<LocationVariable,Term> invariants,
java.util.Map<LocationVariable,Term> freeInvariants,
Term selfTerm,
java.util.Map<LocationVariable,Term> atPres,
Services services)
Returns a new loop invariant where the invariant formula has been
replaced with the passed one.
|
LoopSpecification |
LoopSpecification.setInvariant(java.util.Map<LocationVariable,Term> invariants,
java.util.Map<LocationVariable,Term> freeInvariants,
Term selfTerm,
java.util.Map<LocationVariable,Term> atPres,
Services services)
Returns a new loop invariant where the invariant formula has been
replaced with the passed one.
|
LoopSpecification |
LoopSpecImpl.setInvariant(java.util.Map<LocationVariable,Term> invariants,
java.util.Map<LocationVariable,Term> freeInvariants,
Term selfTerm,
java.util.Map<LocationVariable,Term> atPres,
Services services) |
LoopSpecification |
LoopSpecImpl.setInvariant(java.util.Map<LocationVariable,Term> invariants,
java.util.Map<LocationVariable,Term> freeInvariants,
Term selfTerm,
java.util.Map<LocationVariable,Term> atPres,
Services services) |
LoopSpecification |
LoopSpecImpl.setInvariant(java.util.Map<LocationVariable,Term> invariants,
java.util.Map<LocationVariable,Term> freeInvariants,
Term selfTerm,
java.util.Map<LocationVariable,Term> atPres,
Services services) |
LoopContract |
LoopContract.update(LoopStatement newLoop,
java.util.Map<LocationVariable,Term> newPreconditions,
java.util.Map<LocationVariable,Term> newFreePreconditions,
java.util.Map<LocationVariable,Term> newPostconditions,
java.util.Map<LocationVariable,Term> newFreePostconditions,
java.util.Map<LocationVariable,Term> newModifiesClauses,
ImmutableList<InfFlowSpec> newinfFlowSpecs,
AuxiliaryContract.Variables newVariables,
Term newMeasuredBy,
Term newDecreases) |
LoopContract |
LoopContract.update(LoopStatement newLoop,
java.util.Map<LocationVariable,Term> newPreconditions,
java.util.Map<LocationVariable,Term> newFreePreconditions,
java.util.Map<LocationVariable,Term> newPostconditions,
java.util.Map<LocationVariable,Term> newFreePostconditions,
java.util.Map<LocationVariable,Term> newModifiesClauses,
ImmutableList<InfFlowSpec> newinfFlowSpecs,
AuxiliaryContract.Variables newVariables,
Term newMeasuredBy,
Term newDecreases) |
LoopContract |
LoopContract.update(LoopStatement newLoop,
java.util.Map<LocationVariable,Term> newPreconditions,
java.util.Map<LocationVariable,Term> newFreePreconditions,
java.util.Map<LocationVariable,Term> newPostconditions,
java.util.Map<LocationVariable,Term> newFreePostconditions,
java.util.Map<LocationVariable,Term> newModifiesClauses,
ImmutableList<InfFlowSpec> newinfFlowSpecs,
AuxiliaryContract.Variables newVariables,
Term newMeasuredBy,
Term newDecreases) |
LoopContract |
LoopContract.update(LoopStatement newLoop,
java.util.Map<LocationVariable,Term> newPreconditions,
java.util.Map<LocationVariable,Term> newFreePreconditions,
java.util.Map<LocationVariable,Term> newPostconditions,
java.util.Map<LocationVariable,Term> newFreePostconditions,
java.util.Map<LocationVariable,Term> newModifiesClauses,
ImmutableList<InfFlowSpec> newinfFlowSpecs,
AuxiliaryContract.Variables newVariables,
Term newMeasuredBy,
Term newDecreases) |
LoopContract |
LoopContract.update(LoopStatement newLoop,
java.util.Map<LocationVariable,Term> newPreconditions,
java.util.Map<LocationVariable,Term> newFreePreconditions,
java.util.Map<LocationVariable,Term> newPostconditions,
java.util.Map<LocationVariable,Term> newFreePostconditions,
java.util.Map<LocationVariable,Term> newModifiesClauses,
ImmutableList<InfFlowSpec> newinfFlowSpecs,
AuxiliaryContract.Variables newVariables,
Term newMeasuredBy,
Term newDecreases) |
LoopContract |
LoopContractImpl.update(LoopStatement newLoop,
java.util.Map<LocationVariable,Term> newPreconditions,
java.util.Map<LocationVariable,Term> newFreePreconditions,
java.util.Map<LocationVariable,Term> newPostconditions,
java.util.Map<LocationVariable,Term> newFreePostconditions,
java.util.Map<LocationVariable,Term> newModifiesClauses,
ImmutableList<InfFlowSpec> newinfFlowSpecs,
AuxiliaryContract.Variables newVariables,
Term newMeasuredBy,
Term newDecreases) |
LoopContract |
LoopContractImpl.update(LoopStatement newLoop,
java.util.Map<LocationVariable,Term> newPreconditions,
java.util.Map<LocationVariable,Term> newFreePreconditions,
java.util.Map<LocationVariable,Term> newPostconditions,
java.util.Map<LocationVariable,Term> newFreePostconditions,
java.util.Map<LocationVariable,Term> newModifiesClauses,
ImmutableList<InfFlowSpec> newinfFlowSpecs,
AuxiliaryContract.Variables newVariables,
Term newMeasuredBy,
Term newDecreases) |
LoopContract |
LoopContractImpl.update(LoopStatement newLoop,
java.util.Map<LocationVariable,Term> newPreconditions,
java.util.Map<LocationVariable,Term> newFreePreconditions,
java.util.Map<LocationVariable,Term> newPostconditions,
java.util.Map<LocationVariable,Term> newFreePostconditions,
java.util.Map<LocationVariable,Term> newModifiesClauses,
ImmutableList<InfFlowSpec> newinfFlowSpecs,
AuxiliaryContract.Variables newVariables,
Term newMeasuredBy,
Term newDecreases) |
LoopContract |
LoopContractImpl.update(LoopStatement newLoop,
java.util.Map<LocationVariable,Term> newPreconditions,
java.util.Map<LocationVariable,Term> newFreePreconditions,
java.util.Map<LocationVariable,Term> newPostconditions,
java.util.Map<LocationVariable,Term> newFreePostconditions,
java.util.Map<LocationVariable,Term> newModifiesClauses,
ImmutableList<InfFlowSpec> newinfFlowSpecs,
AuxiliaryContract.Variables newVariables,
Term newMeasuredBy,
Term newDecreases) |
LoopContract |
LoopContractImpl.update(LoopStatement newLoop,
java.util.Map<LocationVariable,Term> newPreconditions,
java.util.Map<LocationVariable,Term> newFreePreconditions,
java.util.Map<LocationVariable,Term> newPostconditions,
java.util.Map<LocationVariable,Term> newFreePostconditions,
java.util.Map<LocationVariable,Term> newModifiesClauses,
ImmutableList<InfFlowSpec> newinfFlowSpecs,
AuxiliaryContract.Variables newVariables,
Term newMeasuredBy,
Term newDecreases) |
BlockContract |
BlockContractImpl.update(StatementBlock newBlock,
java.util.Map<LocationVariable,Term> newPreconditions,
java.util.Map<LocationVariable,Term> newFreePreconditions,
java.util.Map<LocationVariable,Term> newPostconditions,
java.util.Map<LocationVariable,Term> newFreePostconditions,
java.util.Map<LocationVariable,Term> newModifiesClauses,
ImmutableList<InfFlowSpec> newinfFlowSpecs,
AuxiliaryContract.Variables newVariables,
Term newMeasuredBy) |
BlockContract |
BlockContractImpl.update(StatementBlock newBlock,
java.util.Map<LocationVariable,Term> newPreconditions,
java.util.Map<LocationVariable,Term> newFreePreconditions,
java.util.Map<LocationVariable,Term> newPostconditions,
java.util.Map<LocationVariable,Term> newFreePostconditions,
java.util.Map<LocationVariable,Term> newModifiesClauses,
ImmutableList<InfFlowSpec> newinfFlowSpecs,
AuxiliaryContract.Variables newVariables,
Term newMeasuredBy) |
BlockContract |
BlockContractImpl.update(StatementBlock newBlock,
java.util.Map<LocationVariable,Term> newPreconditions,
java.util.Map<LocationVariable,Term> newFreePreconditions,
java.util.Map<LocationVariable,Term> newPostconditions,
java.util.Map<LocationVariable,Term> newFreePostconditions,
java.util.Map<LocationVariable,Term> newModifiesClauses,
ImmutableList<InfFlowSpec> newinfFlowSpecs,
AuxiliaryContract.Variables newVariables,
Term newMeasuredBy) |
BlockContract |
BlockContractImpl.update(StatementBlock newBlock,
java.util.Map<LocationVariable,Term> newPreconditions,
java.util.Map<LocationVariable,Term> newFreePreconditions,
java.util.Map<LocationVariable,Term> newPostconditions,
java.util.Map<LocationVariable,Term> newFreePostconditions,
java.util.Map<LocationVariable,Term> newModifiesClauses,
ImmutableList<InfFlowSpec> newinfFlowSpecs,
AuxiliaryContract.Variables newVariables,
Term newMeasuredBy) |
BlockContract |
BlockContractImpl.update(StatementBlock newBlock,
java.util.Map<LocationVariable,Term> newPreconditions,
java.util.Map<LocationVariable,Term> newFreePreconditions,
java.util.Map<LocationVariable,Term> newPostconditions,
java.util.Map<LocationVariable,Term> newFreePostconditions,
java.util.Map<LocationVariable,Term> newModifiesClauses,
ImmutableList<InfFlowSpec> newinfFlowSpecs,
AuxiliaryContract.Variables newVariables,
Term newMeasuredBy) |
BlockContract |
BlockContract.update(StatementBlock newBlock,
java.util.Map<LocationVariable,Term> newPreconditions,
java.util.Map<LocationVariable,Term> newFreePreconditions,
java.util.Map<LocationVariable,Term> newPostconditions,
java.util.Map<LocationVariable,Term> newFreePostconditions,
java.util.Map<LocationVariable,Term> newModifiesClauses,
ImmutableList<InfFlowSpec> newInfFlowSpecs,
AuxiliaryContract.Variables newVariables,
Term newMeasuredBy) |
BlockContract |
BlockContract.update(StatementBlock newBlock,
java.util.Map<LocationVariable,Term> newPreconditions,
java.util.Map<LocationVariable,Term> newFreePreconditions,
java.util.Map<LocationVariable,Term> newPostconditions,
java.util.Map<LocationVariable,Term> newFreePostconditions,
java.util.Map<LocationVariable,Term> newModifiesClauses,
ImmutableList<InfFlowSpec> newInfFlowSpecs,
AuxiliaryContract.Variables newVariables,
Term newMeasuredBy) |
BlockContract |
BlockContract.update(StatementBlock newBlock,
java.util.Map<LocationVariable,Term> newPreconditions,
java.util.Map<LocationVariable,Term> newFreePreconditions,
java.util.Map<LocationVariable,Term> newPostconditions,
java.util.Map<LocationVariable,Term> newFreePostconditions,
java.util.Map<LocationVariable,Term> newModifiesClauses,
ImmutableList<InfFlowSpec> newInfFlowSpecs,
AuxiliaryContract.Variables newVariables,
Term newMeasuredBy) |
BlockContract |
BlockContract.update(StatementBlock newBlock,
java.util.Map<LocationVariable,Term> newPreconditions,
java.util.Map<LocationVariable,Term> newFreePreconditions,
java.util.Map<LocationVariable,Term> newPostconditions,
java.util.Map<LocationVariable,Term> newFreePostconditions,
java.util.Map<LocationVariable,Term> newModifiesClauses,
ImmutableList<InfFlowSpec> newInfFlowSpecs,
AuxiliaryContract.Variables newVariables,
Term newMeasuredBy) |
BlockContract |
BlockContract.update(StatementBlock newBlock,
java.util.Map<LocationVariable,Term> newPreconditions,
java.util.Map<LocationVariable,Term> newFreePreconditions,
java.util.Map<LocationVariable,Term> newPostconditions,
java.util.Map<LocationVariable,Term> newFreePostconditions,
java.util.Map<LocationVariable,Term> newModifiesClauses,
ImmutableList<InfFlowSpec> newInfFlowSpecs,
AuxiliaryContract.Variables newVariables,
Term newMeasuredBy) |
LoopContract |
LoopContract.update(StatementBlock newBlock,
java.util.Map<LocationVariable,Term> newPreconditions,
java.util.Map<LocationVariable,Term> newFreePreconditions,
java.util.Map<LocationVariable,Term> newPostconditions,
java.util.Map<LocationVariable,Term> newFreePostconditions,
java.util.Map<LocationVariable,Term> newModifiesClauses,
ImmutableList<InfFlowSpec> newinfFlowSpecs,
AuxiliaryContract.Variables newVariables,
Term newMeasuredBy,
Term newDecreases) |
LoopContract |
LoopContract.update(StatementBlock newBlock,
java.util.Map<LocationVariable,Term> newPreconditions,
java.util.Map<LocationVariable,Term> newFreePreconditions,
java.util.Map<LocationVariable,Term> newPostconditions,
java.util.Map<LocationVariable,Term> newFreePostconditions,
java.util.Map<LocationVariable,Term> newModifiesClauses,
ImmutableList<InfFlowSpec> newinfFlowSpecs,
AuxiliaryContract.Variables newVariables,
Term newMeasuredBy,
Term newDecreases) |
LoopContract |
LoopContract.update(StatementBlock newBlock,
java.util.Map<LocationVariable,Term> newPreconditions,
java.util.Map<LocationVariable,Term> newFreePreconditions,
java.util.Map<LocationVariable,Term> newPostconditions,
java.util.Map<LocationVariable,Term> newFreePostconditions,
java.util.Map<LocationVariable,Term> newModifiesClauses,
ImmutableList<InfFlowSpec> newinfFlowSpecs,
AuxiliaryContract.Variables newVariables,
Term newMeasuredBy,
Term newDecreases) |
LoopContract |
LoopContract.update(StatementBlock newBlock,
java.util.Map<LocationVariable,Term> newPreconditions,
java.util.Map<LocationVariable,Term> newFreePreconditions,
java.util.Map<LocationVariable,Term> newPostconditions,
java.util.Map<LocationVariable,Term> newFreePostconditions,
java.util.Map<LocationVariable,Term> newModifiesClauses,
ImmutableList<InfFlowSpec> newinfFlowSpecs,
AuxiliaryContract.Variables newVariables,
Term newMeasuredBy,
Term newDecreases) |
LoopContract |
LoopContract.update(StatementBlock newBlock,
java.util.Map<LocationVariable,Term> newPreconditions,
java.util.Map<LocationVariable,Term> newFreePreconditions,
java.util.Map<LocationVariable,Term> newPostconditions,
java.util.Map<LocationVariable,Term> newFreePostconditions,
java.util.Map<LocationVariable,Term> newModifiesClauses,
ImmutableList<InfFlowSpec> newinfFlowSpecs,
AuxiliaryContract.Variables newVariables,
Term newMeasuredBy,
Term newDecreases) |
LoopContract |
LoopContractImpl.update(StatementBlock newBlock,
java.util.Map<LocationVariable,Term> newPreconditions,
java.util.Map<LocationVariable,Term> newFreePreconditions,
java.util.Map<LocationVariable,Term> newPostconditions,
java.util.Map<LocationVariable,Term> newFreePostconditions,
java.util.Map<LocationVariable,Term> newModifiesClauses,
ImmutableList<InfFlowSpec> newinfFlowSpecs,
AuxiliaryContract.Variables newVariables,
Term newMeasuredBy,
Term newDecreases) |
LoopContract |
LoopContractImpl.update(StatementBlock newBlock,
java.util.Map<LocationVariable,Term> newPreconditions,
java.util.Map<LocationVariable,Term> newFreePreconditions,
java.util.Map<LocationVariable,Term> newPostconditions,
java.util.Map<LocationVariable,Term> newFreePostconditions,
java.util.Map<LocationVariable,Term> newModifiesClauses,
ImmutableList<InfFlowSpec> newinfFlowSpecs,
AuxiliaryContract.Variables newVariables,
Term newMeasuredBy,
Term newDecreases) |
LoopContract |
LoopContractImpl.update(StatementBlock newBlock,
java.util.Map<LocationVariable,Term> newPreconditions,
java.util.Map<LocationVariable,Term> newFreePreconditions,
java.util.Map<LocationVariable,Term> newPostconditions,
java.util.Map<LocationVariable,Term> newFreePostconditions,
java.util.Map<LocationVariable,Term> newModifiesClauses,
ImmutableList<InfFlowSpec> newinfFlowSpecs,
AuxiliaryContract.Variables newVariables,
Term newMeasuredBy,
Term newDecreases) |
LoopContract |
LoopContractImpl.update(StatementBlock newBlock,
java.util.Map<LocationVariable,Term> newPreconditions,
java.util.Map<LocationVariable,Term> newFreePreconditions,
java.util.Map<LocationVariable,Term> newPostconditions,
java.util.Map<LocationVariable,Term> newFreePostconditions,
java.util.Map<LocationVariable,Term> newModifiesClauses,
ImmutableList<InfFlowSpec> newinfFlowSpecs,
AuxiliaryContract.Variables newVariables,
Term newMeasuredBy,
Term newDecreases) |
LoopContract |
LoopContractImpl.update(StatementBlock newBlock,
java.util.Map<LocationVariable,Term> newPreconditions,
java.util.Map<LocationVariable,Term> newFreePreconditions,
java.util.Map<LocationVariable,Term> newPostconditions,
java.util.Map<LocationVariable,Term> newFreePostconditions,
java.util.Map<LocationVariable,Term> newModifiesClauses,
ImmutableList<InfFlowSpec> newinfFlowSpecs,
AuxiliaryContract.Variables newVariables,
Term newMeasuredBy,
Term newDecreases) |
Constructor and Description |
---|
AbstractAuxiliaryContractImpl(java.lang.String baseName,
StatementBlock block,
java.util.List<Label> labels,
IProgramMethod method,
Modality modality,
java.util.Map<LocationVariable,Term> preconditions,
java.util.Map<LocationVariable,Term> freePreconditions,
Term measuredBy,
java.util.Map<LocationVariable,Term> postconditions,
java.util.Map<LocationVariable,Term> freePostconditions,
java.util.Map<LocationVariable,Term> modifiesClauses,
ImmutableList<InfFlowSpec> infFlowSpecs,
AuxiliaryContract.Variables variables,
boolean transactionApplicable,
java.util.Map<LocationVariable,java.lang.Boolean> hasMod,
ImmutableSet<FunctionalAuxiliaryContract<?>> functionalContracts) |
AbstractAuxiliaryContractImpl(java.lang.String baseName,
StatementBlock block,
java.util.List<Label> labels,
IProgramMethod method,
Modality modality,
java.util.Map<LocationVariable,Term> preconditions,
java.util.Map<LocationVariable,Term> freePreconditions,
Term measuredBy,
java.util.Map<LocationVariable,Term> postconditions,
java.util.Map<LocationVariable,Term> freePostconditions,
java.util.Map<LocationVariable,Term> modifiesClauses,
ImmutableList<InfFlowSpec> infFlowSpecs,
AuxiliaryContract.Variables variables,
boolean transactionApplicable,
java.util.Map<LocationVariable,java.lang.Boolean> hasMod,
ImmutableSet<FunctionalAuxiliaryContract<?>> functionalContracts) |
AbstractAuxiliaryContractImpl(java.lang.String baseName,
StatementBlock block,
java.util.List<Label> labels,
IProgramMethod method,
Modality modality,
java.util.Map<LocationVariable,Term> preconditions,
java.util.Map<LocationVariable,Term> freePreconditions,
Term measuredBy,
java.util.Map<LocationVariable,Term> postconditions,
java.util.Map<LocationVariable,Term> freePostconditions,
java.util.Map<LocationVariable,Term> modifiesClauses,
ImmutableList<InfFlowSpec> infFlowSpecs,
AuxiliaryContract.Variables variables,
boolean transactionApplicable,
java.util.Map<LocationVariable,java.lang.Boolean> hasMod,
ImmutableSet<FunctionalAuxiliaryContract<?>> functionalContracts) |
AbstractAuxiliaryContractImpl(java.lang.String baseName,
StatementBlock block,
java.util.List<Label> labels,
IProgramMethod method,
Modality modality,
java.util.Map<LocationVariable,Term> preconditions,
java.util.Map<LocationVariable,Term> freePreconditions,
Term measuredBy,
java.util.Map<LocationVariable,Term> postconditions,
java.util.Map<LocationVariable,Term> freePostconditions,
java.util.Map<LocationVariable,Term> modifiesClauses,
ImmutableList<InfFlowSpec> infFlowSpecs,
AuxiliaryContract.Variables variables,
boolean transactionApplicable,
java.util.Map<LocationVariable,java.lang.Boolean> hasMod,
ImmutableSet<FunctionalAuxiliaryContract<?>> functionalContracts) |
AbstractAuxiliaryContractImpl(java.lang.String baseName,
StatementBlock block,
java.util.List<Label> labels,
IProgramMethod method,
Modality modality,
java.util.Map<LocationVariable,Term> preconditions,
java.util.Map<LocationVariable,Term> freePreconditions,
Term measuredBy,
java.util.Map<LocationVariable,Term> postconditions,
java.util.Map<LocationVariable,Term> freePostconditions,
java.util.Map<LocationVariable,Term> modifiesClauses,
ImmutableList<InfFlowSpec> infFlowSpecs,
AuxiliaryContract.Variables variables,
boolean transactionApplicable,
java.util.Map<LocationVariable,java.lang.Boolean> hasMod,
ImmutableSet<FunctionalAuxiliaryContract<?>> functionalContracts) |
AbstractAuxiliaryContractImpl(java.lang.String baseName,
StatementBlock block,
java.util.List<Label> labels,
IProgramMethod method,
Modality modality,
java.util.Map<LocationVariable,Term> preconditions,
java.util.Map<LocationVariable,Term> freePreconditions,
Term measuredBy,
java.util.Map<LocationVariable,Term> postconditions,
java.util.Map<LocationVariable,Term> freePostconditions,
java.util.Map<LocationVariable,Term> modifiesClauses,
ImmutableList<InfFlowSpec> infFlowSpecs,
AuxiliaryContract.Variables variables,
boolean transactionApplicable,
java.util.Map<LocationVariable,java.lang.Boolean> hasMod,
ImmutableSet<FunctionalAuxiliaryContract<?>> functionalContracts) |
BlockContractImpl(java.lang.String baseName,
StatementBlock block,
java.util.List<Label> labels,
IProgramMethod method,
Modality modality,
java.util.Map<LocationVariable,Term> preconditions,
java.util.Map<LocationVariable,Term> freePreconditions,
Term measuredBy,
java.util.Map<LocationVariable,Term> postconditions,
java.util.Map<LocationVariable,Term> freePostconditions,
java.util.Map<LocationVariable,Term> modifiesClauses,
ImmutableList<InfFlowSpec> infFlowSpecs,
AuxiliaryContract.Variables variables,
boolean transactionApplicable,
java.util.Map<LocationVariable,java.lang.Boolean> hasMod,
ImmutableSet<FunctionalAuxiliaryContract<?>> functionalContracts) |
BlockContractImpl(java.lang.String baseName,
StatementBlock block,
java.util.List<Label> labels,
IProgramMethod method,
Modality modality,
java.util.Map<LocationVariable,Term> preconditions,
java.util.Map<LocationVariable,Term> freePreconditions,
Term measuredBy,
java.util.Map<LocationVariable,Term> postconditions,
java.util.Map<LocationVariable,Term> freePostconditions,
java.util.Map<LocationVariable,Term> modifiesClauses,
ImmutableList<InfFlowSpec> infFlowSpecs,
AuxiliaryContract.Variables variables,
boolean transactionApplicable,
java.util.Map<LocationVariable,java.lang.Boolean> hasMod,
ImmutableSet<FunctionalAuxiliaryContract<?>> functionalContracts) |
BlockContractImpl(java.lang.String baseName,
StatementBlock block,
java.util.List<Label> labels,
IProgramMethod method,
Modality modality,
java.util.Map<LocationVariable,Term> preconditions,
java.util.Map<LocationVariable,Term> freePreconditions,
Term measuredBy,
java.util.Map<LocationVariable,Term> postconditions,
java.util.Map<LocationVariable,Term> freePostconditions,
java.util.Map<LocationVariable,Term> modifiesClauses,
ImmutableList<InfFlowSpec> infFlowSpecs,
AuxiliaryContract.Variables variables,
boolean transactionApplicable,
java.util.Map<LocationVariable,java.lang.Boolean> hasMod,
ImmutableSet<FunctionalAuxiliaryContract<?>> functionalContracts) |
BlockContractImpl(java.lang.String baseName,
StatementBlock block,
java.util.List<Label> labels,
IProgramMethod method,
Modality modality,
java.util.Map<LocationVariable,Term> preconditions,
java.util.Map<LocationVariable,Term> freePreconditions,
Term measuredBy,
java.util.Map<LocationVariable,Term> postconditions,
java.util.Map<LocationVariable,Term> freePostconditions,
java.util.Map<LocationVariable,Term> modifiesClauses,
ImmutableList<InfFlowSpec> infFlowSpecs,
AuxiliaryContract.Variables variables,
boolean transactionApplicable,
java.util.Map<LocationVariable,java.lang.Boolean> hasMod,
ImmutableSet<FunctionalAuxiliaryContract<?>> functionalContracts) |
BlockContractImpl(java.lang.String baseName,
StatementBlock block,
java.util.List<Label> labels,
IProgramMethod method,
Modality modality,
java.util.Map<LocationVariable,Term> preconditions,
java.util.Map<LocationVariable,Term> freePreconditions,
Term measuredBy,
java.util.Map<LocationVariable,Term> postconditions,
java.util.Map<LocationVariable,Term> freePostconditions,
java.util.Map<LocationVariable,Term> modifiesClauses,
ImmutableList<InfFlowSpec> infFlowSpecs,
AuxiliaryContract.Variables variables,
boolean transactionApplicable,
java.util.Map<LocationVariable,java.lang.Boolean> hasMod,
ImmutableSet<FunctionalAuxiliaryContract<?>> functionalContracts) |
BlockContractImpl(java.lang.String baseName,
StatementBlock block,
java.util.List<Label> labels,
IProgramMethod method,
Modality modality,
java.util.Map<LocationVariable,Term> preconditions,
java.util.Map<LocationVariable,Term> freePreconditions,
Term measuredBy,
java.util.Map<LocationVariable,Term> postconditions,
java.util.Map<LocationVariable,Term> freePostconditions,
java.util.Map<LocationVariable,Term> modifiesClauses,
ImmutableList<InfFlowSpec> infFlowSpecs,
AuxiliaryContract.Variables variables,
boolean transactionApplicable,
java.util.Map<LocationVariable,java.lang.Boolean> hasMod,
ImmutableSet<FunctionalAuxiliaryContract<?>> functionalContracts) |
ContractAxiom(java.lang.String name,
IObserverFunction target,
KeYJavaType kjt,
VisibilityModifier visibility,
Term pre,
Term post,
Term mby,
java.util.Map<LocationVariable,ProgramVariable> atPreVars,
ProgramVariable selfVar,
ProgramVariable resultVar,
ImmutableList<ProgramVariable> paramVars) |
ContractAxiom(java.lang.String name,
java.lang.String displayName,
IObserverFunction target,
KeYJavaType kjt,
VisibilityModifier visibility,
Term originalPre,
Term originalPost,
Term originalMby,
java.util.Map<LocationVariable,ProgramVariable> atPreVars,
ProgramVariable selfVar,
ProgramVariable resultVar,
ImmutableList<ProgramVariable> paramVars) |
Creator(java.lang.String baseName,
LoopStatement loop,
java.util.List<Label> labels,
IProgramMethod method,
Behavior behavior,
AuxiliaryContract.Variables variables,
java.util.Map<LocationVariable,Term> requires,
java.util.Map<LocationVariable,Term> requiresFree,
Term measuredBy,
java.util.Map<LocationVariable,Term> ensures,
java.util.Map<LocationVariable,Term> ensuresFree,
ImmutableList<InfFlowSpec> infFlowSpecs,
java.util.Map<Label,Term> breaks,
java.util.Map<Label,Term> continues,
Term returns,
Term signals,
Term signalsOnly,
Term diverges,
java.util.Map<LocationVariable,Term> assignables,
java.util.Map<LocationVariable,java.lang.Boolean> hasMod,
Term decreases,
Services services)
Creates loop contract for a loop.
|
Creator(java.lang.String baseName,
LoopStatement loop,
java.util.List<Label> labels,
IProgramMethod method,
Behavior behavior,
AuxiliaryContract.Variables variables,
java.util.Map<LocationVariable,Term> requires,
java.util.Map<LocationVariable,Term> requiresFree,
Term measuredBy,
java.util.Map<LocationVariable,Term> ensures,
java.util.Map<LocationVariable,Term> ensuresFree,
ImmutableList<InfFlowSpec> infFlowSpecs,
java.util.Map<Label,Term> breaks,
java.util.Map<Label,Term> continues,
Term returns,
Term signals,
Term signalsOnly,
Term diverges,
java.util.Map<LocationVariable,Term> assignables,
java.util.Map<LocationVariable,java.lang.Boolean> hasMod,
Term decreases,
Services services)
Creates loop contract for a loop.
|
Creator(java.lang.String baseName,
LoopStatement loop,
java.util.List<Label> labels,
IProgramMethod method,
Behavior behavior,
AuxiliaryContract.Variables variables,
java.util.Map<LocationVariable,Term> requires,
java.util.Map<LocationVariable,Term> requiresFree,
Term measuredBy,
java.util.Map<LocationVariable,Term> ensures,
java.util.Map<LocationVariable,Term> ensuresFree,
ImmutableList<InfFlowSpec> infFlowSpecs,
java.util.Map<Label,Term> breaks,
java.util.Map<Label,Term> continues,
Term returns,
Term signals,
Term signalsOnly,
Term diverges,
java.util.Map<LocationVariable,Term> assignables,
java.util.Map<LocationVariable,java.lang.Boolean> hasMod,
Term decreases,
Services services)
Creates loop contract for a loop.
|
Creator(java.lang.String baseName,
LoopStatement loop,
java.util.List<Label> labels,
IProgramMethod method,
Behavior behavior,
AuxiliaryContract.Variables variables,
java.util.Map<LocationVariable,Term> requires,
java.util.Map<LocationVariable,Term> requiresFree,
Term measuredBy,
java.util.Map<LocationVariable,Term> ensures,
java.util.Map<LocationVariable,Term> ensuresFree,
ImmutableList<InfFlowSpec> infFlowSpecs,
java.util.Map<Label,Term> breaks,
java.util.Map<Label,Term> continues,
Term returns,
Term signals,
Term signalsOnly,
Term diverges,
java.util.Map<LocationVariable,Term> assignables,
java.util.Map<LocationVariable,java.lang.Boolean> hasMod,
Term decreases,
Services services)
Creates loop contract for a loop.
|
Creator(java.lang.String baseName,
LoopStatement loop,
java.util.List<Label> labels,
IProgramMethod method,
Behavior behavior,
AuxiliaryContract.Variables variables,
java.util.Map<LocationVariable,Term> requires,
java.util.Map<LocationVariable,Term> requiresFree,
Term measuredBy,
java.util.Map<LocationVariable,Term> ensures,
java.util.Map<LocationVariable,Term> ensuresFree,
ImmutableList<InfFlowSpec> infFlowSpecs,
java.util.Map<Label,Term> breaks,
java.util.Map<Label,Term> continues,
Term returns,
Term signals,
Term signalsOnly,
Term diverges,
java.util.Map<LocationVariable,Term> assignables,
java.util.Map<LocationVariable,java.lang.Boolean> hasMod,
Term decreases,
Services services)
Creates loop contract for a loop.
|
Creator(java.lang.String baseName,
LoopStatement loop,
java.util.List<Label> labels,
IProgramMethod method,
Behavior behavior,
AuxiliaryContract.Variables variables,
java.util.Map<LocationVariable,Term> requires,
java.util.Map<LocationVariable,Term> requiresFree,
Term measuredBy,
java.util.Map<LocationVariable,Term> ensures,
java.util.Map<LocationVariable,Term> ensuresFree,
ImmutableList<InfFlowSpec> infFlowSpecs,
java.util.Map<Label,Term> breaks,
java.util.Map<Label,Term> continues,
Term returns,
Term signals,
Term signalsOnly,
Term diverges,
java.util.Map<LocationVariable,Term> assignables,
java.util.Map<LocationVariable,java.lang.Boolean> hasMod,
Term decreases,
Services services)
Creates loop contract for a loop.
|
Creator(java.lang.String baseName,
StatementBlock block,
java.util.List<Label> labels,
IProgramMethod method,
Behavior behavior,
AuxiliaryContract.Variables variables,
java.util.Map<LocationVariable,Term> requires,
java.util.Map<LocationVariable,Term> requiresFree,
Term measuredBy,
java.util.Map<LocationVariable,Term> ensures,
java.util.Map<LocationVariable,Term> ensuresFree,
ImmutableList<InfFlowSpec> infFlowSpecs,
java.util.Map<Label,Term> breaks,
java.util.Map<Label,Term> continues,
Term returns,
Term signals,
Term signalsOnly,
Term diverges,
java.util.Map<LocationVariable,Term> assignables,
java.util.Map<LocationVariable,java.lang.Boolean> hasMod,
Services services) |
Creator(java.lang.String baseName,
StatementBlock block,
java.util.List<Label> labels,
IProgramMethod method,
Behavior behavior,
AuxiliaryContract.Variables variables,
java.util.Map<LocationVariable,Term> requires,
java.util.Map<LocationVariable,Term> requiresFree,
Term measuredBy,
java.util.Map<LocationVariable,Term> ensures,
java.util.Map<LocationVariable,Term> ensuresFree,
ImmutableList<InfFlowSpec> infFlowSpecs,
java.util.Map<Label,Term> breaks,
java.util.Map<Label,Term> continues,
Term returns,
Term signals,
Term signalsOnly,
Term diverges,
java.util.Map<LocationVariable,Term> assignables,
java.util.Map<LocationVariable,java.lang.Boolean> hasMod,
Services services) |
Creator(java.lang.String baseName,
StatementBlock block,
java.util.List<Label> labels,
IProgramMethod method,
Behavior behavior,
AuxiliaryContract.Variables variables,
java.util.Map<LocationVariable,Term> requires,
java.util.Map<LocationVariable,Term> requiresFree,
Term measuredBy,
java.util.Map<LocationVariable,Term> ensures,
java.util.Map<LocationVariable,Term> ensuresFree,
ImmutableList<InfFlowSpec> infFlowSpecs,
java.util.Map<Label,Term> breaks,
java.util.Map<Label,Term> continues,
Term returns,
Term signals,
Term signalsOnly,
Term diverges,
java.util.Map<LocationVariable,Term> assignables,
java.util.Map<LocationVariable,java.lang.Boolean> hasMod,
Services services) |
Creator(java.lang.String baseName,
StatementBlock block,
java.util.List<Label> labels,
IProgramMethod method,
Behavior behavior,
AuxiliaryContract.Variables variables,
java.util.Map<LocationVariable,Term> requires,
java.util.Map<LocationVariable,Term> requiresFree,
Term measuredBy,
java.util.Map<LocationVariable,Term> ensures,
java.util.Map<LocationVariable,Term> ensuresFree,
ImmutableList<InfFlowSpec> infFlowSpecs,
java.util.Map<Label,Term> breaks,
java.util.Map<Label,Term> continues,
Term returns,
Term signals,
Term signalsOnly,
Term diverges,
java.util.Map<LocationVariable,Term> assignables,
java.util.Map<LocationVariable,java.lang.Boolean> hasMod,
Services services) |
Creator(java.lang.String baseName,
StatementBlock block,
java.util.List<Label> labels,
IProgramMethod method,
Behavior behavior,
AuxiliaryContract.Variables variables,
java.util.Map<LocationVariable,Term> requires,
java.util.Map<LocationVariable,Term> requiresFree,
Term measuredBy,
java.util.Map<LocationVariable,Term> ensures,
java.util.Map<LocationVariable,Term> ensuresFree,
ImmutableList<InfFlowSpec> infFlowSpecs,
java.util.Map<Label,Term> breaks,
java.util.Map<Label,Term> continues,
Term returns,
Term signals,
Term signalsOnly,
Term diverges,
java.util.Map<LocationVariable,Term> assignables,
java.util.Map<LocationVariable,java.lang.Boolean> hasMod,
Services services) |
Creator(java.lang.String baseName,
StatementBlock block,
java.util.List<Label> labels,
IProgramMethod method,
Behavior behavior,
AuxiliaryContract.Variables variables,
java.util.Map<LocationVariable,Term> requires,
java.util.Map<LocationVariable,Term> requiresFree,
Term measuredBy,
java.util.Map<LocationVariable,Term> ensures,
java.util.Map<LocationVariable,Term> ensuresFree,
ImmutableList<InfFlowSpec> infFlowSpecs,
java.util.Map<Label,Term> breaks,
java.util.Map<Label,Term> continues,
Term returns,
Term signals,
Term signalsOnly,
Term diverges,
java.util.Map<LocationVariable,Term> assignables,
java.util.Map<LocationVariable,java.lang.Boolean> hasMod,
Services services) |
Creator(java.lang.String baseName,
StatementBlock block,
java.util.List<Label> labels,
IProgramMethod method,
Behavior behavior,
AuxiliaryContract.Variables variables,
java.util.Map<LocationVariable,Term> requires,
java.util.Map<LocationVariable,Term> requiresFree,
Term measuredBy,
java.util.Map<LocationVariable,Term> ensures,
java.util.Map<LocationVariable,Term> ensuresFree,
ImmutableList<InfFlowSpec> infFlowSpecs,
java.util.Map<Label,Term> breaks,
java.util.Map<Label,Term> continues,
Term returns,
Term signals,
Term signalsOnly,
Term diverges,
java.util.Map<LocationVariable,Term> assignables,
java.util.Map<LocationVariable,java.lang.Boolean> hasMod,
Services services) |
Creator(java.lang.String baseName,
StatementBlock block,
java.util.List<Label> labels,
IProgramMethod method,
Behavior behavior,
AuxiliaryContract.Variables variables,
java.util.Map<LocationVariable,Term> requires,
java.util.Map<LocationVariable,Term> requiresFree,
Term measuredBy,
java.util.Map<LocationVariable,Term> ensures,
java.util.Map<LocationVariable,Term> ensuresFree,
ImmutableList<InfFlowSpec> infFlowSpecs,
java.util.Map<Label,Term> breaks,
java.util.Map<Label,Term> continues,
Term returns,
Term signals,
Term signalsOnly,
Term diverges,
java.util.Map<LocationVariable,Term> assignables,
java.util.Map<LocationVariable,java.lang.Boolean> hasMod,
Services services) |
Creator(java.lang.String baseName,
StatementBlock block,
java.util.List<Label> labels,
IProgramMethod method,
Behavior behavior,
AuxiliaryContract.Variables variables,
java.util.Map<LocationVariable,Term> requires,
java.util.Map<LocationVariable,Term> requiresFree,
Term measuredBy,
java.util.Map<LocationVariable,Term> ensures,
java.util.Map<LocationVariable,Term> ensuresFree,
ImmutableList<InfFlowSpec> infFlowSpecs,
java.util.Map<Label,Term> breaks,
java.util.Map<Label,Term> continues,
Term returns,
Term signals,
Term signalsOnly,
Term diverges,
java.util.Map<LocationVariable,Term> assignables,
java.util.Map<LocationVariable,java.lang.Boolean> hasMod,
Services services) |
Creator(java.lang.String baseName,
StatementBlock block,
java.util.List<Label> labels,
IProgramMethod method,
Behavior behavior,
AuxiliaryContract.Variables variables,
java.util.Map<LocationVariable,Term> requires,
java.util.Map<LocationVariable,Term> requiresFree,
Term measuredBy,
java.util.Map<LocationVariable,Term> ensures,
java.util.Map<LocationVariable,Term> ensuresFree,
ImmutableList<InfFlowSpec> infFlowSpecs,
java.util.Map<Label,Term> breaks,
java.util.Map<Label,Term> continues,
Term returns,
Term signals,
Term signalsOnly,
Term diverges,
java.util.Map<LocationVariable,Term> assignables,
java.util.Map<LocationVariable,java.lang.Boolean> hasMod,
Services services) |
Creator(java.lang.String baseName,
StatementBlock block,
java.util.List<Label> labels,
IProgramMethod method,
Behavior behavior,
AuxiliaryContract.Variables variables,
java.util.Map<LocationVariable,Term> requires,
java.util.Map<LocationVariable,Term> requiresFree,
Term measuredBy,
java.util.Map<LocationVariable,Term> ensures,
java.util.Map<LocationVariable,Term> ensuresFree,
ImmutableList<InfFlowSpec> infFlowSpecs,
java.util.Map<Label,Term> breaks,
java.util.Map<Label,Term> continues,
Term returns,
Term signals,
Term signalsOnly,
Term diverges,
java.util.Map<LocationVariable,Term> assignables,
java.util.Map<LocationVariable,java.lang.Boolean> hasMod,
Services services) |
Creator(java.lang.String baseName,
StatementBlock block,
java.util.List<Label> labels,
IProgramMethod method,
Behavior behavior,
AuxiliaryContract.Variables variables,
java.util.Map<LocationVariable,Term> requires,
java.util.Map<LocationVariable,Term> requiresFree,
Term measuredBy,
java.util.Map<LocationVariable,Term> ensures,
java.util.Map<LocationVariable,Term> ensuresFree,
ImmutableList<InfFlowSpec> infFlowSpecs,
java.util.Map<Label,Term> breaks,
java.util.Map<Label,Term> continues,
Term returns,
Term signals,
Term signalsOnly,
Term diverges,
java.util.Map<LocationVariable,Term> assignables,
java.util.Map<LocationVariable,java.lang.Boolean> hasMod,
Services services) |
Creator(java.lang.String baseName,
StatementBlock block,
java.util.List<Label> labels,
IProgramMethod method,
Behavior behavior,
AuxiliaryContract.Variables variables,
java.util.Map<LocationVariable,Term> requires,
java.util.Map<LocationVariable,Term> requiresFree,
Term measuredBy,
java.util.Map<LocationVariable,Term> ensures,
java.util.Map<LocationVariable,Term> ensuresFree,
ImmutableList<InfFlowSpec> infFlowSpecs,
java.util.Map<Label,Term> breaks,
java.util.Map<Label,Term> continues,
Term returns,
Term signals,
Term signalsOnly,
Term diverges,
java.util.Map<LocationVariable,Term> assignables,
java.util.Map<LocationVariable,java.lang.Boolean> hasMod,
Term decreases,
Services services)
Creates loop contract for a block that starts with a loop.
|
Creator(java.lang.String baseName,
StatementBlock block,
java.util.List<Label> labels,
IProgramMethod method,
Behavior behavior,
AuxiliaryContract.Variables variables,
java.util.Map<LocationVariable,Term> requires,
java.util.Map<LocationVariable,Term> requiresFree,
Term measuredBy,
java.util.Map<LocationVariable,Term> ensures,
java.util.Map<LocationVariable,Term> ensuresFree,
ImmutableList<InfFlowSpec> infFlowSpecs,
java.util.Map<Label,Term> breaks,
java.util.Map<Label,Term> continues,
Term returns,
Term signals,
Term signalsOnly,
Term diverges,
java.util.Map<LocationVariable,Term> assignables,
java.util.Map<LocationVariable,java.lang.Boolean> hasMod,
Term decreases,
Services services)
Creates loop contract for a block that starts with a loop.
|
Creator(java.lang.String baseName,
StatementBlock block,
java.util.List<Label> labels,
IProgramMethod method,
Behavior behavior,
AuxiliaryContract.Variables variables,
java.util.Map<LocationVariable,Term> requires,
java.util.Map<LocationVariable,Term> requiresFree,
Term measuredBy,
java.util.Map<LocationVariable,Term> ensures,
java.util.Map<LocationVariable,Term> ensuresFree,
ImmutableList<InfFlowSpec> infFlowSpecs,
java.util.Map<Label,Term> breaks,
java.util.Map<Label,Term> continues,
Term returns,
Term signals,
Term signalsOnly,
Term diverges,
java.util.Map<LocationVariable,Term> assignables,
java.util.Map<LocationVariable,java.lang.Boolean> hasMod,
Term decreases,
Services services)
Creates loop contract for a block that starts with a loop.
|
Creator(java.lang.String baseName,
StatementBlock block,
java.util.List<Label> labels,
IProgramMethod method,
Behavior behavior,
AuxiliaryContract.Variables variables,
java.util.Map<LocationVariable,Term> requires,
java.util.Map<LocationVariable,Term> requiresFree,
Term measuredBy,
java.util.Map<LocationVariable,Term> ensures,
java.util.Map<LocationVariable,Term> ensuresFree,
ImmutableList<InfFlowSpec> infFlowSpecs,
java.util.Map<Label,Term> breaks,
java.util.Map<Label,Term> continues,
Term returns,
Term signals,
Term signalsOnly,
Term diverges,
java.util.Map<LocationVariable,Term> assignables,
java.util.Map<LocationVariable,java.lang.Boolean> hasMod,
Term decreases,
Services services)
Creates loop contract for a block that starts with a loop.
|
Creator(java.lang.String baseName,
StatementBlock block,
java.util.List<Label> labels,
IProgramMethod method,
Behavior behavior,
AuxiliaryContract.Variables variables,
java.util.Map<LocationVariable,Term> requires,
java.util.Map<LocationVariable,Term> requiresFree,
Term measuredBy,
java.util.Map<LocationVariable,Term> ensures,
java.util.Map<LocationVariable,Term> ensuresFree,
ImmutableList<InfFlowSpec> infFlowSpecs,
java.util.Map<Label,Term> breaks,
java.util.Map<Label,Term> continues,
Term returns,
Term signals,
Term signalsOnly,
Term diverges,
java.util.Map<LocationVariable,Term> assignables,
java.util.Map<LocationVariable,java.lang.Boolean> hasMod,
Term decreases,
Services services)
Creates loop contract for a block that starts with a loop.
|
Creator(java.lang.String baseName,
StatementBlock block,
java.util.List<Label> labels,
IProgramMethod method,
Behavior behavior,
AuxiliaryContract.Variables variables,
java.util.Map<LocationVariable,Term> requires,
java.util.Map<LocationVariable,Term> requiresFree,
Term measuredBy,
java.util.Map<LocationVariable,Term> ensures,
java.util.Map<LocationVariable,Term> ensuresFree,
ImmutableList<InfFlowSpec> infFlowSpecs,
java.util.Map<Label,Term> breaks,
java.util.Map<Label,Term> continues,
Term returns,
Term signals,
Term signalsOnly,
Term diverges,
java.util.Map<LocationVariable,Term> assignables,
java.util.Map<LocationVariable,java.lang.Boolean> hasMod,
Term decreases,
Services services)
Creates loop contract for a block that starts with a loop.
|
LoopContractImpl(java.lang.String baseName,
LoopStatement loop,
java.util.List<Label> labels,
IProgramMethod method,
Modality modality,
java.util.Map<LocationVariable,Term> preconditions,
java.util.Map<LocationVariable,Term> freePreconditions,
Term measuredBy,
java.util.Map<LocationVariable,Term> postconditions,
java.util.Map<LocationVariable,Term> freePostconditions,
java.util.Map<LocationVariable,Term> modifiesClauses,
ImmutableList<InfFlowSpec> infFlowSpecs,
AuxiliaryContract.Variables variables,
boolean transactionApplicable,
java.util.Map<LocationVariable,java.lang.Boolean> hasMod,
Term decreases,
ImmutableSet<FunctionalAuxiliaryContract<?>> functionalContracts,
Services services)
Construct a loop contract for a loop.
|
LoopContractImpl(java.lang.String baseName,
LoopStatement loop,
java.util.List<Label> labels,
IProgramMethod method,
Modality modality,
java.util.Map<LocationVariable,Term> preconditions,
java.util.Map<LocationVariable,Term> freePreconditions,
Term measuredBy,
java.util.Map<LocationVariable,Term> postconditions,
java.util.Map<LocationVariable,Term> freePostconditions,
java.util.Map<LocationVariable,Term> modifiesClauses,
ImmutableList<InfFlowSpec> infFlowSpecs,
AuxiliaryContract.Variables variables,
boolean transactionApplicable,
java.util.Map<LocationVariable,java.lang.Boolean> hasMod,
Term decreases,
ImmutableSet<FunctionalAuxiliaryContract<?>> functionalContracts,
Services services)
Construct a loop contract for a loop.
|
LoopContractImpl(java.lang.String baseName,
LoopStatement loop,
java.util.List<Label> labels,
IProgramMethod method,
Modality modality,
java.util.Map<LocationVariable,Term> preconditions,
java.util.Map<LocationVariable,Term> freePreconditions,
Term measuredBy,
java.util.Map<LocationVariable,Term> postconditions,
java.util.Map<LocationVariable,Term> freePostconditions,
java.util.Map<LocationVariable,Term> modifiesClauses,
ImmutableList<InfFlowSpec> infFlowSpecs,
AuxiliaryContract.Variables variables,
boolean transactionApplicable,
java.util.Map<LocationVariable,java.lang.Boolean> hasMod,
Term decreases,
ImmutableSet<FunctionalAuxiliaryContract<?>> functionalContracts,
Services services)
Construct a loop contract for a loop.
|
LoopContractImpl(java.lang.String baseName,
LoopStatement loop,
java.util.List<Label> labels,
IProgramMethod method,
Modality modality,
java.util.Map<LocationVariable,Term> preconditions,
java.util.Map<LocationVariable,Term> freePreconditions,
Term measuredBy,
java.util.Map<LocationVariable,Term> postconditions,
java.util.Map<LocationVariable,Term> freePostconditions,
java.util.Map<LocationVariable,Term> modifiesClauses,
ImmutableList<InfFlowSpec> infFlowSpecs,
AuxiliaryContract.Variables variables,
boolean transactionApplicable,
java.util.Map<LocationVariable,java.lang.Boolean> hasMod,
Term decreases,
ImmutableSet<FunctionalAuxiliaryContract<?>> functionalContracts,
Services services)
Construct a loop contract for a loop.
|
LoopContractImpl(java.lang.String baseName,
LoopStatement loop,
java.util.List<Label> labels,
IProgramMethod method,
Modality modality,
java.util.Map<LocationVariable,Term> preconditions,
java.util.Map<LocationVariable,Term> freePreconditions,
Term measuredBy,
java.util.Map<LocationVariable,Term> postconditions,
java.util.Map<LocationVariable,Term> freePostconditions,
java.util.Map<LocationVariable,Term> modifiesClauses,
ImmutableList<InfFlowSpec> infFlowSpecs,
AuxiliaryContract.Variables variables,
boolean transactionApplicable,
java.util.Map<LocationVariable,java.lang.Boolean> hasMod,
Term decreases,
ImmutableSet<FunctionalAuxiliaryContract<?>> functionalContracts,
Services services)
Construct a loop contract for a loop.
|
LoopContractImpl(java.lang.String baseName,
LoopStatement loop,
java.util.List<Label> labels,
IProgramMethod method,
Modality modality,
java.util.Map<LocationVariable,Term> preconditions,
java.util.Map<LocationVariable,Term> freePreconditions,
Term measuredBy,
java.util.Map<LocationVariable,Term> postconditions,
java.util.Map<LocationVariable,Term> freePostconditions,
java.util.Map<LocationVariable,Term> modifiesClauses,
ImmutableList<InfFlowSpec> infFlowSpecs,
AuxiliaryContract.Variables variables,
boolean transactionApplicable,
java.util.Map<LocationVariable,java.lang.Boolean> hasMod,
Term decreases,
ImmutableSet<FunctionalAuxiliaryContract<?>> functionalContracts,
Services services)
Construct a loop contract for a loop.
|
LoopContractImpl(java.lang.String baseName,
StatementBlock block,
java.util.List<Label> labels,
IProgramMethod method,
Modality modality,
java.util.Map<LocationVariable,Term> preconditions,
java.util.Map<LocationVariable,Term> freePreconditions,
Term measuredBy,
java.util.Map<LocationVariable,Term> postconditions,
java.util.Map<LocationVariable,Term> freePostconditions,
java.util.Map<LocationVariable,Term> modifiesClauses,
ImmutableList<InfFlowSpec> infFlowSpecs,
AuxiliaryContract.Variables variables,
boolean transactionApplicable,
java.util.Map<LocationVariable,java.lang.Boolean> hasMod,
Term decreases,
ImmutableSet<FunctionalAuxiliaryContract<?>> functionalContracts,
Services services)
Construct a loop contract for a block that starts with a loop.
|
LoopContractImpl(java.lang.String baseName,
StatementBlock block,
java.util.List<Label> labels,
IProgramMethod method,
Modality modality,
java.util.Map<LocationVariable,Term> preconditions,
java.util.Map<LocationVariable,Term> freePreconditions,
Term measuredBy,
java.util.Map<LocationVariable,Term> postconditions,
java.util.Map<LocationVariable,Term> freePostconditions,
java.util.Map<LocationVariable,Term> modifiesClauses,
ImmutableList<InfFlowSpec> infFlowSpecs,
AuxiliaryContract.Variables variables,
boolean transactionApplicable,
java.util.Map<LocationVariable,java.lang.Boolean> hasMod,
Term decreases,
ImmutableSet<FunctionalAuxiliaryContract<?>> functionalContracts,
Services services)
Construct a loop contract for a block that starts with a loop.
|
LoopContractImpl(java.lang.String baseName,
StatementBlock block,
java.util.List<Label> labels,
IProgramMethod method,
Modality modality,
java.util.Map<LocationVariable,Term> preconditions,
java.util.Map<LocationVariable,Term> freePreconditions,
Term measuredBy,
java.util.Map<LocationVariable,Term> postconditions,
java.util.Map<LocationVariable,Term> freePostconditions,
java.util.Map<LocationVariable,Term> modifiesClauses,
ImmutableList<InfFlowSpec> infFlowSpecs,
AuxiliaryContract.Variables variables,
boolean transactionApplicable,
java.util.Map<LocationVariable,java.lang.Boolean> hasMod,
Term decreases,
ImmutableSet<FunctionalAuxiliaryContract<?>> functionalContracts,
Services services)
Construct a loop contract for a block that starts with a loop.
|
LoopContractImpl(java.lang.String baseName,
StatementBlock block,
java.util.List<Label> labels,
IProgramMethod method,
Modality modality,
java.util.Map<LocationVariable,Term> preconditions,
java.util.Map<LocationVariable,Term> freePreconditions,
Term measuredBy,
java.util.Map<LocationVariable,Term> postconditions,
java.util.Map<LocationVariable,Term> freePostconditions,
java.util.Map<LocationVariable,Term> modifiesClauses,
ImmutableList<InfFlowSpec> infFlowSpecs,
AuxiliaryContract.Variables variables,
boolean transactionApplicable,
java.util.Map<LocationVariable,java.lang.Boolean> hasMod,
Term decreases,
ImmutableSet<FunctionalAuxiliaryContract<?>> functionalContracts,
Services services)
Construct a loop contract for a block that starts with a loop.
|
LoopContractImpl(java.lang.String baseName,
StatementBlock block,
java.util.List<Label> labels,
IProgramMethod method,
Modality modality,
java.util.Map<LocationVariable,Term> preconditions,
java.util.Map<LocationVariable,Term> freePreconditions,
Term measuredBy,
java.util.Map<LocationVariable,Term> postconditions,
java.util.Map<LocationVariable,Term> freePostconditions,
java.util.Map<LocationVariable,Term> modifiesClauses,
ImmutableList<InfFlowSpec> infFlowSpecs,
AuxiliaryContract.Variables variables,
boolean transactionApplicable,
java.util.Map<LocationVariable,java.lang.Boolean> hasMod,
Term decreases,
ImmutableSet<FunctionalAuxiliaryContract<?>> functionalContracts,
Services services)
Construct a loop contract for a block that starts with a loop.
|
LoopContractImpl(java.lang.String baseName,
StatementBlock block,
java.util.List<Label> labels,
IProgramMethod method,
Modality modality,
java.util.Map<LocationVariable,Term> preconditions,
java.util.Map<LocationVariable,Term> freePreconditions,
Term measuredBy,
java.util.Map<LocationVariable,Term> postconditions,
java.util.Map<LocationVariable,Term> freePostconditions,
java.util.Map<LocationVariable,Term> modifiesClauses,
ImmutableList<InfFlowSpec> infFlowSpecs,
AuxiliaryContract.Variables variables,
boolean transactionApplicable,
java.util.Map<LocationVariable,java.lang.Boolean> hasMod,
Term decreases,
ImmutableSet<FunctionalAuxiliaryContract<?>> functionalContracts,
Services services)
Construct a loop contract for a block that starts with a loop.
|
LoopSpecImpl(LoopStatement loop,
IProgramMethod pm,
KeYJavaType kjt,
java.util.Map<LocationVariable,Term> invariants,
java.util.Map<LocationVariable,Term> freeInvariants,
java.util.Map<LocationVariable,Term> modifies,
java.util.Map<LocationVariable,ImmutableList<InfFlowSpec>> infFlowSpecs,
Term variant,
Term selfTerm,
ImmutableList<Term> localIns,
ImmutableList<Term> localOuts,
java.util.Map<LocationVariable,Term> atPres)
Creates a loop invariant.
|
LoopSpecImpl(LoopStatement loop,
IProgramMethod pm,
KeYJavaType kjt,
java.util.Map<LocationVariable,Term> invariants,
java.util.Map<LocationVariable,Term> freeInvariants,
java.util.Map<LocationVariable,Term> modifies,
java.util.Map<LocationVariable,ImmutableList<InfFlowSpec>> infFlowSpecs,
Term variant,
Term selfTerm,
ImmutableList<Term> localIns,
ImmutableList<Term> localOuts,
java.util.Map<LocationVariable,Term> atPres)
Creates a loop invariant.
|
LoopSpecImpl(LoopStatement loop,
IProgramMethod pm,
KeYJavaType kjt,
java.util.Map<LocationVariable,Term> invariants,
java.util.Map<LocationVariable,Term> freeInvariants,
java.util.Map<LocationVariable,Term> modifies,
java.util.Map<LocationVariable,ImmutableList<InfFlowSpec>> infFlowSpecs,
Term variant,
Term selfTerm,
ImmutableList<Term> localIns,
ImmutableList<Term> localOuts,
java.util.Map<LocationVariable,Term> atPres)
Creates a loop invariant.
|
LoopSpecImpl(LoopStatement loop,
IProgramMethod pm,
KeYJavaType kjt,
java.util.Map<LocationVariable,Term> invariants,
java.util.Map<LocationVariable,Term> freeInvariants,
java.util.Map<LocationVariable,Term> modifies,
java.util.Map<LocationVariable,ImmutableList<InfFlowSpec>> infFlowSpecs,
Term variant,
Term selfTerm,
ImmutableList<Term> localIns,
ImmutableList<Term> localOuts,
java.util.Map<LocationVariable,Term> atPres)
Creates a loop invariant.
|
LoopSpecImpl(LoopStatement loop,
IProgramMethod pm,
KeYJavaType kjt,
java.util.Map<LocationVariable,Term> invariants,
java.util.Map<LocationVariable,Term> freeInvariants,
java.util.Map<LocationVariable,Term> modifies,
java.util.Map<LocationVariable,ImmutableList<InfFlowSpec>> infFlowSpecs,
Term variant,
Term selfTerm,
ImmutableList<Term> localIns,
ImmutableList<Term> localOuts,
java.util.Map<LocationVariable,Term> atPres)
Creates a loop invariant.
|
LoopSpecImpl(LoopStatement loop,
IProgramMethod pm,
KeYJavaType kjt,
Term selfTerm,
java.util.Map<LocationVariable,Term> atPres)
Creates an empty, default loop invariant for the passed loop.
|
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
|
PredicateAbstractionMergeContract(MergePointStatement mps,
java.util.Map<LocationVariable,Term> atPres,
KeYJavaType kjt,
java.lang.String latticeType,
java.util.List<AbstractionPredicate> abstractionPredicates) |
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) |
Terms(Term self,
java.util.Map<Label,Term> breakFlags,
java.util.Map<Label,Term> continueFlags,
Term returnFlag,
Term result,
Term exception,
java.util.Map<LocationVariable,Term> remembranceHeaps,
java.util.Map<LocationVariable,Term> remembranceLocalVariables,
java.util.Map<LocationVariable,Term> outerRemembranceHeaps,
java.util.Map<LocationVariable,Term> outerRemembranceVariables)
Creates a new instance.
|
Terms(Term self,
java.util.Map<Label,Term> breakFlags,
java.util.Map<Label,Term> continueFlags,
Term returnFlag,
Term result,
Term exception,
java.util.Map<LocationVariable,Term> remembranceHeaps,
java.util.Map<LocationVariable,Term> remembranceLocalVariables,
java.util.Map<LocationVariable,Term> outerRemembranceHeaps,
java.util.Map<LocationVariable,Term> outerRemembranceVariables)
Creates a new instance.
|
Terms(Term self,
java.util.Map<Label,Term> breakFlags,
java.util.Map<Label,Term> continueFlags,
Term returnFlag,
Term result,
Term exception,
java.util.Map<LocationVariable,Term> remembranceHeaps,
java.util.Map<LocationVariable,Term> remembranceLocalVariables,
java.util.Map<LocationVariable,Term> outerRemembranceHeaps,
java.util.Map<LocationVariable,Term> outerRemembranceVariables)
Creates a new instance.
|
Terms(Term self,
java.util.Map<Label,Term> breakFlags,
java.util.Map<Label,Term> continueFlags,
Term returnFlag,
Term result,
Term exception,
java.util.Map<LocationVariable,Term> remembranceHeaps,
java.util.Map<LocationVariable,Term> remembranceLocalVariables,
java.util.Map<LocationVariable,Term> outerRemembranceHeaps,
java.util.Map<LocationVariable,Term> outerRemembranceVariables)
Creates a new instance.
|
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. |
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. |
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. |
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 | Field and Description |
---|---|
java.util.Map<LocationVariable,Term> |
JMLSpecFactory.ContractClauses.assignables |
java.util.Map<LocationVariable,Term> |
ProgramVariableCollection.atBefores
A map from every variable
var to \before(var) (if applicable). |
java.util.Map<LocationVariable,LocationVariable> |
ProgramVariableCollection.atBeforeVars
A map from every variable
var to \before(var) (if applicable). |
java.util.Map<LocationVariable,LocationVariable> |
ProgramVariableCollection.atBeforeVars
A map from every variable
var to \before(var) (if applicable). |
java.util.Map<LocationVariable,Term> |
ProgramVariableCollection.atPres
A map from every variable
var to \old(var) . |
java.util.Map<LocationVariable,LocationVariable> |
ProgramVariableCollection.atPreVars
A map from every variable
var to \old(var) . |
java.util.Map<LocationVariable,LocationVariable> |
ProgramVariableCollection.atPreVars
A map from every variable
var to \old(var) . |
java.util.Map<LocationVariable,Term> |
JMLSpecFactory.ContractClauses.axioms |
java.util.Map<LocationVariable,Term> |
JMLSpecFactory.ContractClauses.ensures |
java.util.Map<LocationVariable,Term> |
JMLSpecFactory.ContractClauses.ensuresFree |
java.util.Map<LocationVariable,java.lang.Boolean> |
JMLSpecFactory.ContractClauses.hasMod |
java.util.Map<LocationVariable,Term> |
JMLSpecFactory.ContractClauses.requires |
java.util.Map<LocationVariable,Term> |
JMLSpecFactory.ContractClauses.requiresFree |
Modifier and Type | Method and Description |
---|---|
Contract |
JMLSpecFactory.createJMLDependencyContract(KeYJavaType kjt,
LocationVariable targetHeap,
LabeledParserRuleContext originalDep) |
Modifier and Type | Method and Description |
---|---|
ImmutableSet<Contract> |
JMLSpecFactory.createFunctionalOperationContracts(java.lang.String name,
IProgramMethod pm,
ProgramVariableCollection progVars,
JMLSpecFactory.ContractClauses clauses,
java.util.Map<LocationVariable,Term> posts,
java.util.Map<LocationVariable,Term> axioms)
Generate functional operation contracts.
|
ImmutableSet<Contract> |
JMLSpecFactory.createFunctionalOperationContracts(java.lang.String name,
IProgramMethod pm,
ProgramVariableCollection progVars,
JMLSpecFactory.ContractClauses clauses,
java.util.Map<LocationVariable,Term> posts,
java.util.Map<LocationVariable,Term> axioms)
Generate functional operation contracts.
|
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)
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)
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.
|
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.
|
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.
|
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.
|
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.
|
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 |
---|---|
JmlIO |
JmlIO.atBefore(java.util.Map<LocationVariable,Term> atBefores) |
JmlIO |
JmlIO.atPres(java.util.Map<LocationVariable,Term> atPres) |
SLExpression |
JmlTermFactory.fresh(ImmutableList<SLExpression> list,
java.util.Map<LocationVariable,Term> atPres) |
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.
|
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 |
---|---|
protected LocationVariable |
AbstractUpdateExtractor.ExtractLocationParameter.createLocationVariable(java.lang.String name,
Sort sort)
Creates a new
LocationVariable with the given name and Sort . |
LocationVariable |
AbstractUpdateExtractor.ExtractLocationParameter.getPreVariable()
Returns the pre variable.
|
Modifier and Type | Method and Description |
---|---|
protected static LocationVariable |
ExecutionOperationContract.extractResultVariableFromPostBranch(Node node,
Services services)
Extracts the result variable from the given post branch.
|
Modifier and Type | Method and Description |
---|---|
protected void |
ExecutionAuxiliaryContract.collectRemembranceVariables(Term term,
java.util.Map<LocationVariable,Term> remembranceHeaps,
java.util.Map<LocationVariable,Term> remembranceLocalVariables)
Collects recursive all remembrance variables.
|
protected void |
ExecutionAuxiliaryContract.collectRemembranceVariables(Term term,
java.util.Map<LocationVariable,Term> remembranceHeaps,
java.util.Map<LocationVariable,Term> remembranceLocalVariables)
Collects recursive all remembrance variables.
|
Modifier and Type | Method and Description |
---|---|
protected Term |
ProgramMethodPO.getGlobalDefs(LocationVariable heap,
Term heapTerm,
Term selfTerm,
ImmutableList<Term> paramTerms,
Services services) |
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 static ImmutableList<ProgramVariable> |
ProgramMethodSubsetPO.convert(java.util.Collection<LocationVariable> c)
Converts the given
Collection into an ImmutableList . |
protected Term |
ProgramMethodSubsetPO.ensureUninterpretedPredicateExists(ImmutableList<ProgramVariable> paramVars,
ImmutableList<LocationVariable> formalParamVars,
ProgramVariable exceptionVar,
java.lang.String name,
Services proofServices)
|
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.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.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 |
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 |
ProgramMethodPO.getPre(java.util.List<LocationVariable> modHeaps,
ProgramVariable selfVar,
ImmutableList<ProgramVariable> paramVars,
java.util.Map<LocationVariable,LocationVariable> atPreVars,
Services services)
Creates the precondition.
|
protected Term |
ProgramMethodSubsetPO.getPre(java.util.List<LocationVariable> modHeaps,
ProgramVariable selfVar,
ImmutableList<ProgramVariable> paramVars,
java.util.Map<LocationVariable,LocationVariable> atPreVars,
Services services)
Creates the precondition.
|
protected Term |
ProgramMethodSubsetPO.getPre(java.util.List<LocationVariable> modHeaps,
ProgramVariable selfVar,
ImmutableList<ProgramVariable> paramVars,
java.util.Map<LocationVariable,LocationVariable> atPreVars,
Services services)
Creates the precondition.
|
protected Term |
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 |
---|---|
java.util.Set<LocationVariable> |
AbstractConditionalBreakpoint.getToKeep()
Returns the variables KeY should keep to evaluate the condition.
|
Modifier and Type | Method and Description |
---|---|
static java.util.List<LocationVariable> |
MiscTools.applicableHeapContexts(Modality modality,
Services services)
Returns the applicable heap contexts out of the currently available set
of three contexts: The normal heap, the saved heap (transaction), and the
permission heap.
|
Modifier and Type | Method and Description |
---|---|
static LocationVariable |
MergeRuleUtils.getBranchUniqueLocVar(LocationVariable var,
Node startLeaf)
Find a location variable for the given one that is unique for the branch
corresponding to the given goal, but not necessarily globally unique.
|
static LocationVariable |
MergeRuleUtils.getFreshLocVariableForPrefix(java.lang.String prefix,
Sort sort,
Services services)
Computes and registers a fresh location variable with the given prefix in
its name of the given sort.
|
LocationVariable |
MergeParamsSpec.getPlaceholder() |
Modifier and Type | Method and Description |
---|---|
static ImmutableSet<LocationVariable> |
MergeRuleUtils.getLocationVariables(Term term,
Services services)
Returns all program variables in the given term.
|
static java.util.HashSet<LocationVariable> |
MergeRuleUtils.getLocationVariablesHashSet(Sequent sequent,
Services services)
Returns all program variables in the given sequent.
|
static java.util.HashSet<LocationVariable> |
MergeRuleUtils.getLocationVariablesHashSet(Term term,
Services services)
Returns all program variables in the given term.
|
static ImmutableSet<LocationVariable> |
MergeRuleUtils.getUpdateLeftSideLocations(Term u) |
Modifier and Type | Method and Description |
---|---|
static LocationVariable |
MergeRuleUtils.getBranchUniqueLocVar(LocationVariable var,
Node startLeaf)
Find a location variable for the given one that is unique for the branch
corresponding to the given goal, but not necessarily globally unique.
|
static Node |
MergeRuleUtils.getIntroducingNodeforLocVar(LocationVariable var,
Node node)
Finds the node, from the given leaf on, where the variable was
introduced.
|
static Term |
MergeRuleUtils.getUpdateRightSideFor(Term update,
LocationVariable leftSide)
Returns the right side for a given location variable in an update (in
normal form).
|
static MergeRuleUtils.Option<Term> |
MergeRuleUtils.getUpdateRightSideForSafe(Term update,
LocationVariable leftSide)
Returns the right side for a given location variable in an update (in
normal form).
|
Constructor and Description |
---|
MergeParamsSpec(java.lang.String latticeType,
LocationVariable placeholder,
ImmutableList<Term> predicates) |
Copyright © 2003-2019 The KeY-Project.