Package | Description |
---|---|
de.uka.ilkd.key.informationflow.po | |
de.uka.ilkd.key.java |
This package contains classes that cover the Java programming language.
|
de.uka.ilkd.key.java.declaration |
Elements of the Java syntax tree representing declarations.
|
de.uka.ilkd.key.java.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.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.init |
This package contains classes handling prover initialisation.
|
de.uka.ilkd.key.proof.mgt |
This package contains classes for proof environments and proof management.
|
de.uka.ilkd.key.rule |
This package contains classes for implementing rules.
|
de.uka.ilkd.key.rule.metaconstruct |
contains classes representing the meta constructs of
Taclet s. |
de.uka.ilkd.key.speclang |
This package contains the specification language frontends of KeY.
|
de.uka.ilkd.key.speclang.jml | |
de.uka.ilkd.key.speclang.jml.translation | |
de.uka.ilkd.key.symbolic_execution | |
de.uka.ilkd.key.symbolic_execution.model | |
de.uka.ilkd.key.symbolic_execution.model.impl | |
de.uka.ilkd.key.symbolic_execution.po | |
de.uka.ilkd.key.symbolic_execution.strategy.breakpoint |
Modifier and Type | Method and Description |
---|---|
protected ImmutableList<StatementBlock> |
LoopInvExecutionPO.buildOperationBlocks(ImmutableList<LocationVariable> formalParVars,
ProgramVariable selfVar,
ProgramVariable resultVar,
Services services)
Deprecated.
|
protected ImmutableList<StatementBlock> |
InfFlowContractPO.buildOperationBlocks(ImmutableList<LocationVariable> formalParVars,
ProgramVariable selfVar,
ProgramVariable resultVar,
Services services)
Deprecated.
|
protected ImmutableList<StatementBlock> |
BlockExecutionPO.buildOperationBlocks(ImmutableList<LocationVariable> formalParVars,
ProgramVariable selfVar,
ProgramVariable resultVar,
Services services)
Deprecated.
|
protected ImmutableList<StatementBlock> |
SymbolicExecutionPO.buildOperationBlocks(ImmutableList<LocationVariable> formalParVars,
ProgramVariable selfVar,
ProgramVariable resultVar,
Services services)
Deprecated.
|
Modifier and Type | Class and Description |
---|---|
class |
ContextStatementBlock
In the DL-formulae description of Taclets the program part can have
the following form < pi alpha;...; omega > Phi where pi is a prefix
consisting of open brackets, try's and so on and omega is the rest
of the program.
|
Modifier and Type | Method and Description |
---|---|
static StatementBlock |
KeYJavaASTFactory.block(ExtList statements)
Create a block from an arbitrary number of statements.
|
static StatementBlock |
KeYJavaASTFactory.block(java.util.List<Statement> statements)
Create a block from an arbitrary number of statements.
|
static StatementBlock |
KeYJavaASTFactory.block(Statement... statements)
Create a block from an arbitrary number of statements.
|
StatementBlock |
Recoder2KeYConverter.convert(StatementBlock block)
convert a statement block and remove all included anonymous classes.
|
protected StatementBlock |
CreateArrayMethodBuilder.getCreateArrayBody(TypeReference arrayRef,
ProgramVariable paramLength) |
protected StatementBlock |
CreateArrayMethodBuilder.getCreateArrayHelperBody(ProgramVariable length,
ImmutableList<Field> fields,
boolean createTransient,
ProgramVariable transientType)
creates the body of method
<createArrayHelper(int
paramLength)>
therefore it first adds the statements responsible to take the correct
one out of the list, then the arrays length attribute is set followed by
a call to <prepare>() setting the arrays fields on
their default value. |
static StatementBlock |
KeYJavaASTFactory.insertStatementInBlock(Statement[] stmnt,
StatementBlock b)
inserts the given statements at the begin of the block
|
static StatementBlock |
KeYJavaASTFactory.insertStatementInBlock(StatementBlock block,
Statement[] statements)
Create a block where the given statements come after the given block.
|
static StatementBlock |
KeYJavaASTFactory.insertStatementInBlock(StatementBlock stmnt,
StatementBlock b)
inserts the given statements at the begin of the block
|
static StatementBlock |
KeYJavaASTFactory.insertStatementInBlock(Statement statement,
StatementBlock block)
Insert a statement in a block of statements.
|
Modifier and Type | Method and Description |
---|---|
static Catch |
KeYJavaASTFactory.catchClause(JavaInfo javaInfo,
java.lang.String param,
KeYJavaType kjt,
StatementBlock body)
Create a catch clause.
|
static Catch |
KeYJavaASTFactory.catchClause(JavaInfo javaInfo,
java.lang.String param,
java.lang.String type,
StatementBlock body)
Create a catch clause.
|
static Catch |
KeYJavaASTFactory.catchClause(ParameterDeclaration param,
StatementBlock body)
create a catch clause
|
static Finally |
KeYJavaASTFactory.finallyBlock(StatementBlock body)
Create a finally block.
|
static StatementBlock |
KeYJavaASTFactory.insertStatementInBlock(Statement[] stmnt,
StatementBlock b)
inserts the given statements at the begin of the block
|
static StatementBlock |
KeYJavaASTFactory.insertStatementInBlock(StatementBlock block,
Statement[] statements)
Create a block where the given statements come after the given block.
|
static StatementBlock |
KeYJavaASTFactory.insertStatementInBlock(StatementBlock stmnt,
StatementBlock b)
inserts the given statements at the begin of the block
|
static StatementBlock |
KeYJavaASTFactory.insertStatementInBlock(Statement statement,
StatementBlock block)
Insert a statement in a block of statements.
|
static MethodFrame |
KeYJavaASTFactory.methodFrame(IExecutionContext executionContext,
StatementBlock block)
Create a method call substitution.
|
static MethodFrame |
KeYJavaASTFactory.methodFrame(IExecutionContext executionContext,
StatementBlock block,
PositionInfo position)
Create a method call substitution at a specific source position.
|
static MethodFrame |
KeYJavaASTFactory.methodFrame(IProgramVariable result,
IExecutionContext executionContext,
StatementBlock block)
Create a method call substitution with a return value assignment.
|
static MethodFrame |
KeYJavaASTFactory.methodFrame(IProgramVariable result,
IExecutionContext executionContext,
StatementBlock block,
PositionInfo position)
Create a method call substitution with a return value assignment at a
specific source position.
|
void |
PrettyPrinter.printStatementBlock(StatementBlock x) |
static Try |
KeYJavaASTFactory.tryBlock(StatementBlock body,
Branch[] branches)
Create a try block.
|
Modifier and Type | Field and Description |
---|---|
protected StatementBlock |
ClassInitializer.body |
protected StatementBlock |
MethodDeclaration.body |
Modifier and Type | Method and Description |
---|---|
StatementBlock |
ClassInitializer.getBody() |
StatementBlock |
MethodDeclaration.getBody() |
Constructor and Description |
---|
ClassInitializer(Static modifier,
StatementBlock body) |
ConstructorDeclaration(Modifier[] modifiers,
ProgramElementName name,
ParameterDeclaration[] parameters,
Throws exceptions,
StatementBlock body,
boolean parentIsInterfaceDeclaration)
Deprecated.
|
MethodDeclaration(Modifier[] modifiers,
TypeReference returnType,
ProgramElementName name,
ImmutableArray<ParameterDeclaration> parameters,
Throws exceptions,
StatementBlock body,
boolean parentIsInterfaceDeclaration)
Method declaration.
|
MethodDeclaration(Modifier[] modifiers,
TypeReference returnType,
ProgramElementName name,
ParameterDeclaration[] parameters,
Throws exceptions,
StatementBlock body,
boolean parentIsInterfaceDeclaration)
Method declaration.
|
Modifier and Type | Field and Description |
---|---|
protected StatementBlock |
Catch.body
Body.
|
protected StatementBlock |
LoopScopeBlock.body |
protected StatementBlock |
Finally.body
Body.
|
protected StatementBlock |
SynchronizedBlock.body
Body.
|
protected StatementBlock |
Ccatch.body
Body.
|
Modifier and Type | Method and Description |
---|---|
StatementBlock |
Exec.getBody()
Get body.
|
StatementBlock |
LoopScopeBlock.getBody()
Get body.
|
StatementBlock |
MethodFrame.getBody()
Get body.
|
StatementBlock |
Try.getBody()
Get body.
|
StatementBlock |
SynchronizedBlock.getBody()
Get body.
|
Modifier and Type | Method and Description |
---|---|
protected StatementBlock |
ProgramContextAdder.createStatementBlockWrapper(StatementBlock wrapper,
JavaNonTerminalProgramElement replacement)
Replaces the first statement in the wrapper block.
|
StatementBlock |
OuterBreakContinueAndReturnReplacer.getResult() |
StatementBlock |
InnerBreakAndContinueReplacer.getResult() |
StatementBlock |
OuterBreakContinueAndReturnReplacer.replace() |
StatementBlock |
InnerBreakAndContinueReplacer.replace()
Does the replacement and returns the result.
|
Modifier and Type | Method and Description |
---|---|
protected Exec |
ProgramContextAdder.createExecStatementWrapper(StatementBlock body,
Exec old) |
protected LoopScopeBlock |
ProgramContextAdder.createLoopScopeBlockWrapper(LoopScopeBlock old,
StatementBlock body) |
protected MethodFrame |
ProgramContextAdder.createMethodFrameWrapper(MethodFrame old,
StatementBlock body) |
protected StatementBlock |
ProgramContextAdder.createStatementBlockWrapper(StatementBlock wrapper,
JavaNonTerminalProgramElement replacement)
Replaces the first statement in the wrapper block.
|
protected SynchronizedBlock |
ProgramContextAdder.createSynchronizedBlockWrapper(SynchronizedBlock old,
StatementBlock body) |
protected Try |
ProgramContextAdder.createTryStatementWrapper(StatementBlock body,
Try old) |
void |
ProgVarReplaceVisitor.performActionOnBlockContract(StatementBlock oldBlock,
StatementBlock newBlock) |
void |
Visitor.performActionOnBlockContract(StatementBlock oldBlock,
StatementBlock newBlock)
Adds block contract for new statement block to block contract
of old block statement.
|
void |
JavaASTVisitor.performActionOnBlockContract(StatementBlock oldBlock,
StatementBlock newBlock) |
void |
ProgVarReplaceVisitor.performActionOnLoopContract(StatementBlock oldBlock,
StatementBlock newBlock) |
void |
Visitor.performActionOnLoopContract(StatementBlock oldBlock,
StatementBlock newBlock)
Adds block contract for new statement block to block contract
of old block statement.
|
void |
JavaASTVisitor.performActionOnLoopContract(StatementBlock oldBlock,
StatementBlock newBlock) |
void |
Visitor.performActionOnStatementBlock(StatementBlock x) |
void |
OuterBreakContinueAndReturnReplacer.performActionOnStatementBlock(StatementBlock x) |
void |
InnerBreakAndContinueReplacer.performActionOnStatementBlock(StatementBlock x) |
void |
CreatingASTVisitor.performActionOnStatementBlock(StatementBlock x) |
void |
JavaASTVisitor.performActionOnStatementBlock(StatementBlock x) |
JavaNonTerminalProgramElement |
ProgramContextAdder.start(JavaNonTerminalProgramElement context,
StatementBlock putIn,
ContextStatementBlockInstantiation ct)
wraps the context around the statements found in the putIn block
|
protected JavaNonTerminalProgramElement |
ProgramContextAdder.wrap(JavaNonTerminalProgramElement context,
StatementBlock putIn,
IntIterator prefixPos,
int prefixDepth,
PosInProgram prefix,
PosInProgram suffix) |
Constructor and Description |
---|
InnerBreakAndContinueReplacer(StatementBlock block,
java.lang.Iterable<Label> loopLabels,
Label breakLabel,
Label continueLabel,
Services services) |
OuterBreakContinueAndReturnReplacer(StatementBlock block,
java.lang.Iterable<Label> alwaysInnerLabels,
Label breakOutLabel,
java.util.Map<Label,ProgramVariable> breakFlags,
java.util.Map<Label,ProgramVariable> continueFlags,
ProgramVariable returnFlag,
ProgramVariable returnValue,
ProgramVariable exception,
Services services) |
Modifier and Type | Method and Description |
---|---|
static JavaBlock |
JavaBlock.createJavaBlock(StatementBlock prg)
create a new JavaBlock
|
Modifier and Type | Method and Description |
---|---|
StatementBlock |
ProgramMethod.getBody() |
StatementBlock |
IProgramMethod.getBody() |
StatementBlock |
ProgramSV.getBody() |
Modifier and Type | Method and Description |
---|---|
StatementBlock |
FunctionalBlockContractPO.getBlock() |
StatementBlock |
FunctionalLoopContractPO.getBlock() |
Modifier and Type | Method and Description |
---|---|
protected abstract ImmutableList<StatementBlock> |
AbstractOperationPO.buildOperationBlocks(ImmutableList<LocationVariable> formalParVars,
ProgramVariable selfVar,
ProgramVariable resultVar,
Services services)
Builds the code to execute in different statement blocks.
|
protected ImmutableList<StatementBlock> |
FunctionalOperationContractPO.buildOperationBlocks(ImmutableList<LocationVariable> formalParVars,
ProgramVariable selfVar,
ProgramVariable resultVar,
Services services)
Builds the code to execute in different statement blocks.
|
Modifier and Type | Method and Description |
---|---|
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 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. |
Modifier and Type | Method and Description |
---|---|
ImmutableSet<BlockContract> |
SpecificationRepository.getBlockContracts(StatementBlock block)
Returns all block contracts for the specified block.
|
ImmutableSet<BlockContract> |
SpecificationRepository.getBlockContracts(StatementBlock block,
Modality modality)
Returns block contracts for according block statement
and modality.
|
ImmutableSet<LoopContract> |
SpecificationRepository.getLoopContracts(StatementBlock block)
Returns all loop contracts for the specified block.
|
ImmutableSet<LoopContract> |
SpecificationRepository.getLoopContracts(StatementBlock block,
Modality modality) |
Modifier and Type | Method and Description |
---|---|
StatementBlock |
AuxiliaryContractBuilders.ValidityProgramConstructor.construct() |
Constructor and Description |
---|
ValidityProgramConstructor(java.lang.Iterable<Label> labels,
StatementBlock block,
AuxiliaryContract.Variables variables,
ProgramVariable exceptionParameter,
Services services) |
ValidityProgramConstructor(java.lang.Iterable<Label> labels,
StatementBlock block,
AuxiliaryContract.Variables variables,
ProgramVariable exceptionParameter,
Services services,
AuxiliaryContract.Variables alreadyDeclared) |
Modifier and Type | Method and Description |
---|---|
StatementBlock |
EnhancedForElimination.getHead() |
Modifier and Type | Method and Description |
---|---|
protected JavaBlock |
WhileInvariantTransformer.addContext(JavaNonTerminalProgramElement root,
StatementBlock block) |
void |
WhileLoopTransformation.performActionOnStatementBlock(StatementBlock x) |
Modifier and Type | Method and Description |
---|---|
void |
IntroAtPreDefsOp.updateBlockAndLoopContracts(ImmutableSet<StatementBlock> blocks,
ImmutableSet<LoopStatement> loops,
java.util.Map<LocationVariable,LocationVariable> atPreVars,
java.util.Map<LocationVariable,LocationVariable> atPreHeapVars,
Services services)
Replace the placeholder variables
(see
AuxiliaryContract.getPlaceholderVariables() )
of all block contracts for blocks in blocks by
atPreVars and atPreHeapVars |
Constructor and Description |
---|
ReplaceWhileLoop(ProgramElement root,
StatementBlock toInsert,
Services services)
creates the WhileLoopTransformation for the transformation mode
|
ReplaceWhileLoop(ProgramElement root,
SVInstantiations inst,
StatementBlock toInsert,
Services services)
creates the WhileLoopTransformation for the check mode
|
Modifier and Type | Field and Description |
---|---|
protected StatementBlock |
AbstractAuxiliaryContractImpl.block |
Modifier and Type | Method and Description |
---|---|
StatementBlock |
AbstractAuxiliaryContractImpl.getBlock() |
StatementBlock |
FunctionalAuxiliaryContract.getBlock() |
StatementBlock |
AuxiliaryContract.getBlock() |
StatementBlock |
LoopContract.getBody() |
StatementBlock |
LoopContractImpl.getBody() |
StatementBlock |
LoopContract.getHead()
This contains any statements that are executed before the loop.
|
StatementBlock |
LoopContractImpl.getHead() |
StatementBlock |
LoopContract.getTail() |
StatementBlock |
LoopContractImpl.getTail() |
Modifier and Type | Method and Description |
---|---|
protected abstract T |
AbstractAuxiliaryContractImpl.Creator.build(java.lang.String baseName,
StatementBlock block,
java.util.List<Label> labels,
IProgramMethod method,
Modality modality,
java.util.Map<LocationVariable,Term> preconditions,
java.util.Map<LocationVariable,Term> freePreconditions,
Term measuredBy,
java.util.Map<LocationVariable,Term> postconditions,
java.util.Map<LocationVariable,Term> freePostconditions,
java.util.Map<LocationVariable,Term> modifiesClauses,
ImmutableList<InfFlowSpec> infFlowSpecs,
AuxiliaryContract.Variables variables,
boolean transactionApplicable,
java.util.Map<LocationVariable,java.lang.Boolean> hasMod) |
protected BlockContract |
BlockContractImpl.Creator.build(java.lang.String baseName,
StatementBlock block,
java.util.List<Label> labels,
IProgramMethod method,
Modality modality,
java.util.Map<LocationVariable,Term> preconditions,
java.util.Map<LocationVariable,Term> freePreconditions,
Term measuredBy,
java.util.Map<LocationVariable,Term> postconditions,
java.util.Map<LocationVariable,Term> freePostconditions,
java.util.Map<LocationVariable,Term> modifiesClauses,
ImmutableList<InfFlowSpec> infFlowSpecs,
AuxiliaryContract.Variables variables,
boolean transactionApplicable,
java.util.Map<LocationVariable,java.lang.Boolean> hasMod) |
protected LoopContract |
LoopContractImpl.Creator.build(java.lang.String baseName,
StatementBlock block,
java.util.List<Label> labels,
IProgramMethod method,
Modality modality,
java.util.Map<LocationVariable,Term> preconditions,
java.util.Map<LocationVariable,Term> freePreconditions,
Term measuredBy,
java.util.Map<LocationVariable,Term> postconditions,
java.util.Map<LocationVariable,Term> freePostconditions,
java.util.Map<LocationVariable,Term> modifiesClauses,
ImmutableList<InfFlowSpec> infFlowSpecs,
AuxiliaryContract.Variables variables,
boolean transactionApplicable,
java.util.Map<LocationVariable,java.lang.Boolean> hasMod) |
static AuxiliaryContract.Variables |
AuxiliaryContract.Variables.create(StatementBlock block,
java.util.List<Label> labels,
IProgramMethod method,
Services services)
Creates a new instance.
|
ImmutableSet<BlockContract> |
SpecExtractor.extractBlockContracts(IProgramMethod method,
StatementBlock block)
Returns the block contracts for the passed block.
|
ImmutableSet<LoopContract> |
SpecExtractor.extractLoopContracts(IProgramMethod method,
StatementBlock block)
Returns the loop contracts for the passed block.
|
LoopContract |
LoopContract.replaceEnhancedForVariables(StatementBlock newBlock,
Services services)
Replaces
\index and \values with the proper variables in all terms of this
contract. |
LoopContract |
LoopContractImpl.replaceEnhancedForVariables(StatementBlock newBlock,
Services services) |
LoopContract |
LoopContract.setBlock(StatementBlock newBlock) |
BlockContract |
BlockContractImpl.setBlock(StatementBlock newBlock) |
BlockContract |
BlockContract.setBlock(StatementBlock newBlock) |
LoopContract |
LoopContractImpl.setBlock(StatementBlock newBlock) |
AuxiliaryContract |
AuxiliaryContract.setBlock(StatementBlock newBlock) |
BlockContract |
BlockContractImpl.update(StatementBlock newBlock,
java.util.Map<LocationVariable,Term> newPreconditions,
java.util.Map<LocationVariable,Term> newFreePreconditions,
java.util.Map<LocationVariable,Term> newPostconditions,
java.util.Map<LocationVariable,Term> newFreePostconditions,
java.util.Map<LocationVariable,Term> newModifiesClauses,
ImmutableList<InfFlowSpec> newinfFlowSpecs,
AuxiliaryContract.Variables newVariables,
Term newMeasuredBy) |
BlockContract |
BlockContract.update(StatementBlock newBlock,
java.util.Map<LocationVariable,Term> newPreconditions,
java.util.Map<LocationVariable,Term> newFreePreconditions,
java.util.Map<LocationVariable,Term> newPostconditions,
java.util.Map<LocationVariable,Term> newFreePostconditions,
java.util.Map<LocationVariable,Term> newModifiesClauses,
ImmutableList<InfFlowSpec> newInfFlowSpecs,
AuxiliaryContract.Variables newVariables,
Term newMeasuredBy) |
LoopContract |
LoopContract.update(StatementBlock newBlock,
java.util.Map<LocationVariable,Term> newPreconditions,
java.util.Map<LocationVariable,Term> newFreePreconditions,
java.util.Map<LocationVariable,Term> newPostconditions,
java.util.Map<LocationVariable,Term> newFreePostconditions,
java.util.Map<LocationVariable,Term> newModifiesClauses,
ImmutableList<InfFlowSpec> newinfFlowSpecs,
AuxiliaryContract.Variables newVariables,
Term newMeasuredBy,
Term newDecreases) |
LoopContract |
LoopContractImpl.update(StatementBlock newBlock,
java.util.Map<LocationVariable,Term> newPreconditions,
java.util.Map<LocationVariable,Term> newFreePreconditions,
java.util.Map<LocationVariable,Term> newPostconditions,
java.util.Map<LocationVariable,Term> newFreePostconditions,
java.util.Map<LocationVariable,Term> newModifiesClauses,
ImmutableList<InfFlowSpec> newinfFlowSpecs,
AuxiliaryContract.Variables newVariables,
Term newMeasuredBy,
Term newDecreases) |
Constructor and Description |
---|
AbstractAuxiliaryContractImpl(java.lang.String baseName,
StatementBlock block,
java.util.List<Label> labels,
IProgramMethod method,
Modality modality,
java.util.Map<LocationVariable,Term> preconditions,
java.util.Map<LocationVariable,Term> freePreconditions,
Term measuredBy,
java.util.Map<LocationVariable,Term> postconditions,
java.util.Map<LocationVariable,Term> freePostconditions,
java.util.Map<LocationVariable,Term> modifiesClauses,
ImmutableList<InfFlowSpec> infFlowSpecs,
AuxiliaryContract.Variables variables,
boolean transactionApplicable,
java.util.Map<LocationVariable,java.lang.Boolean> hasMod,
ImmutableSet<FunctionalAuxiliaryContract<?>> functionalContracts) |
BlockContractImpl(java.lang.String baseName,
StatementBlock block,
java.util.List<Label> labels,
IProgramMethod method,
Modality modality,
java.util.Map<LocationVariable,Term> preconditions,
java.util.Map<LocationVariable,Term> freePreconditions,
Term measuredBy,
java.util.Map<LocationVariable,Term> postconditions,
java.util.Map<LocationVariable,Term> freePostconditions,
java.util.Map<LocationVariable,Term> modifiesClauses,
ImmutableList<InfFlowSpec> infFlowSpecs,
AuxiliaryContract.Variables variables,
boolean transactionApplicable,
java.util.Map<LocationVariable,java.lang.Boolean> hasMod,
ImmutableSet<FunctionalAuxiliaryContract<?>> functionalContracts) |
Creator(java.lang.String baseName,
StatementBlock block,
java.util.List<Label> labels,
IProgramMethod method,
Behavior behavior,
AuxiliaryContract.Variables variables,
java.util.Map<LocationVariable,Term> requires,
java.util.Map<LocationVariable,Term> requiresFree,
Term measuredBy,
java.util.Map<LocationVariable,Term> ensures,
java.util.Map<LocationVariable,Term> ensuresFree,
ImmutableList<InfFlowSpec> infFlowSpecs,
java.util.Map<Label,Term> breaks,
java.util.Map<Label,Term> continues,
Term returns,
Term signals,
Term signalsOnly,
Term diverges,
java.util.Map<LocationVariable,Term> assignables,
java.util.Map<LocationVariable,java.lang.Boolean> hasMod,
Services services) |
Creator(java.lang.String baseName,
StatementBlock block,
java.util.List<Label> labels,
IProgramMethod method,
Behavior behavior,
AuxiliaryContract.Variables variables,
java.util.Map<LocationVariable,Term> requires,
java.util.Map<LocationVariable,Term> requiresFree,
Term measuredBy,
java.util.Map<LocationVariable,Term> ensures,
java.util.Map<LocationVariable,Term> ensuresFree,
ImmutableList<InfFlowSpec> infFlowSpecs,
java.util.Map<Label,Term> breaks,
java.util.Map<Label,Term> continues,
Term returns,
Term signals,
Term signalsOnly,
Term diverges,
java.util.Map<LocationVariable,Term> assignables,
java.util.Map<LocationVariable,java.lang.Boolean> hasMod,
Services services) |
Creator(java.lang.String baseName,
StatementBlock block,
java.util.List<Label> labels,
IProgramMethod method,
Behavior behavior,
AuxiliaryContract.Variables variables,
java.util.Map<LocationVariable,Term> requires,
java.util.Map<LocationVariable,Term> requiresFree,
Term measuredBy,
java.util.Map<LocationVariable,Term> ensures,
java.util.Map<LocationVariable,Term> ensuresFree,
ImmutableList<InfFlowSpec> infFlowSpecs,
java.util.Map<Label,Term> breaks,
java.util.Map<Label,Term> continues,
Term returns,
Term signals,
Term signalsOnly,
Term diverges,
java.util.Map<LocationVariable,Term> assignables,
java.util.Map<LocationVariable,java.lang.Boolean> hasMod,
Term decreases,
Services services)
Creates loop contract for a block that starts with a loop.
|
LoopContractImpl(java.lang.String baseName,
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.
|
Modifier and Type | Method and Description |
---|---|
ImmutableSet<BlockContract> |
JMLSpecExtractor.extractBlockContracts(IProgramMethod method,
StatementBlock block) |
ImmutableSet<LoopContract> |
JMLSpecExtractor.extractLoopContracts(IProgramMethod method,
StatementBlock block) |
Modifier and Type | Method and Description |
---|---|
ImmutableSet<BlockContract> |
JMLSpecFactory.createJMLBlockContracts(IProgramMethod method,
java.util.List<Label> labels,
StatementBlock block,
TextualJMLSpecCase specificationCase)
Creates a set of block contracts for a block from a textual specification case.
|
ImmutableSet<LoopContract> |
JMLSpecFactory.createJMLLoopContracts(IProgramMethod method,
java.util.List<Label> labels,
StatementBlock block,
TextualJMLSpecCase specificationCase)
Creates a set of loop contracts for a block from a textual specification case.
|
Modifier and Type | Method and Description |
---|---|
StatementBlock |
ExecutionNodeReader.KeYlessBlockContract.getBlock()
Returns the
StatementBlock at which the BlockContract is applied. |
Modifier and Type | Method and Description |
---|---|
StatementBlock |
IExecutionAuxiliaryContract.getBlock()
Returns the
StatementBlock at which the BlockContract is applied. |
Modifier and Type | Method and Description |
---|---|
StatementBlock |
ExecutionAuxiliaryContract.getBlock()
Returns the
StatementBlock at which the BlockContract is applied. |
Modifier and Type | Method and Description |
---|---|
protected Term |
ExecutionAuxiliaryContract.declaredVariableAsTerm(StatementBlock sb,
int statementIndex)
Returns the variable declared by the statement at the given index as
Term . |
Modifier and Type | Method and Description |
---|---|
protected ImmutableList<StatementBlock> |
ProgramMethodPO.buildOperationBlocks(ImmutableList<LocationVariable> formalParVars,
ProgramVariable selfVar,
ProgramVariable resultVar,
Services services)
Builds the code to execute in different statement blocks.
|
protected ImmutableList<StatementBlock> |
ProgramMethodSubsetPO.buildOperationBlocks(ImmutableList<LocationVariable> formalParVars,
ProgramVariable selfVar,
ProgramVariable resultVar,
Services services)
Builds the code to execute in different statement blocks.
|
Modifier and Type | Method and Description |
---|---|
protected abstract StatementBlock |
AbstractConditionalBreakpoint.getStatementBlock(StatementContainer statementContainer)
For a given
StatementContainer this method computes the StatementBlock that contains all lines before the line the Breakpoint is at, including the line itself. |
protected StatementBlock |
KeYWatchpoint.getStatementBlock(StatementContainer statementContainer) |
protected StatementBlock |
MethodBreakpoint.getStatementBlock(StatementContainer statementContainer) |
protected StatementBlock |
LineBreakpoint.getStatementBlock(StatementContainer statementContainer)
For a given
StatementContainer this method computes the StatementBlock that contains all lines before the line the Breakpoint is at, including the line itself. |
Copyright © 2003-2019 The KeY-Project.