Package | Description |
---|---|
de.uka.ilkd.key.java |
This package contains classes that cover the Java programming language.
|
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.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.translation | |
de.uka.ilkd.key.speclang.njml |
This package provides the functionalities of parsing JML comments into KeY constructs.
|
Modifier and Type | Method and Description |
---|---|
Label |
CcatchContinueLabelParameterDeclaration.getLabel() |
Label |
CcatchBreakLabelParameterDeclaration.getLabel() |
Modifier and Type | Method and Description |
---|---|
static Break |
KeYJavaASTFactory.breakStatement(Label l)
Create a break statement.
|
static Statement |
KeYJavaASTFactory.breakStatement(Label label,
PositionInfo positionInfo) |
static Continue |
KeYJavaASTFactory.continueStatement(Label label) |
static LabeledStatement |
KeYJavaASTFactory.labeledStatement(ExtList parameters,
Label label,
PositionInfo position)
Create a labeled statement.
|
static Statement |
KeYJavaASTFactory.labeledStatement(Label label,
Statement[] statements,
PositionInfo pos)
Create a labeled block of statements.
|
static LabeledStatement |
KeYJavaASTFactory.labeledStatement(Label label,
Statement statement,
PositionInfo pos)
Create a labeled statement.
|
Modifier and Type | Field and Description |
---|---|
protected Label |
LabeledStatement.name
Name.
|
protected Label |
LabelJumpStatement.name
Name.
|
Modifier and Type | Method and Description |
---|---|
Label |
LabeledStatement.getLabel()
Get identifier.
|
Label |
LabelJumpStatement.getLabel()
Get Label.
|
Constructor and Description |
---|
Break(Label label)
Break.
|
Continue(Label label)
Continue.
|
LabeledStatement(ExtList children,
Label label,
PositionInfo pos)
Constructor for the transformation of COMPOST ASTs to KeY.
|
LabeledStatement(Label name)
Labeled statement.
|
LabeledStatement(Label id,
Statement statement,
PositionInfo pos)
Labeled statement.
|
LabelJumpStatement(Label label)
Label jump statement.
|
Modifier and Type | Method and Description |
---|---|
boolean |
LabelCollector.contains(Label l) |
boolean |
FreeLabelFinder.findLabel(Label label,
ProgramElement node) |
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) |
Constructor and Description |
---|
InnerBreakAndContinueReplacer(StatementBlock block,
java.lang.Iterable<Label> loopLabels,
Label breakLabel,
Label continueLabel,
Services services) |
OuterBreakContinueAndReturnCollector(ProgramElement root,
java.util.List<Label> alwaysInnerLabels,
Services services) |
OuterBreakContinueAndReturnReplacer(StatementBlock block,
java.lang.Iterable<Label> alwaysInnerLabels,
Label breakOutLabel,
java.util.Map<Label,ProgramVariable> breakFlags,
java.util.Map<Label,ProgramVariable> continueFlags,
ProgramVariable returnFlag,
ProgramVariable returnValue,
ProgramVariable exception,
Services services) |
OuterBreakContinueAndReturnReplacer(StatementBlock block,
java.lang.Iterable<Label> alwaysInnerLabels,
Label breakOutLabel,
java.util.Map<Label,ProgramVariable> breakFlags,
java.util.Map<Label,ProgramVariable> continueFlags,
ProgramVariable returnFlag,
ProgramVariable returnValue,
ProgramVariable exception,
Services services) |
OuterBreakContinueAndReturnReplacer(StatementBlock block,
java.lang.Iterable<Label> alwaysInnerLabels,
Label breakOutLabel,
java.util.Map<Label,ProgramVariable> breakFlags,
java.util.Map<Label,ProgramVariable> continueFlags,
ProgramVariable returnFlag,
ProgramVariable returnValue,
ProgramVariable exception,
Services services) |
Modifier and Type | Interface and Description |
---|---|
interface |
ProgramConstruct
A type that implement this interface can be used in all java
programs instead of an expression or statement.
|
Modifier and Type | Class and Description |
---|---|
class |
ProgramElementName |
static class |
VariableNamer.IndProgramElementName
ProgramElementName carrying an additional index
|
Modifier and Type | Class and Description |
---|---|
class |
ProgramSV
Objects of this class are schema variables matching program constructs within
modal operators.
|
Constructor and Description |
---|
GoalsConfigurator(AbstractAuxiliaryContractBuiltInRuleApp application,
TermLabelState termLabelState,
AbstractAuxiliaryContractRule.Instantiation instantiation,
java.util.List<Label> labels,
AuxiliaryContract.Variables variables,
PosInOccurrence occurrence,
Services services,
AbstractAuxiliaryContractRule rule) |
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 | Field and Description |
---|---|
protected java.util.Stack<Label> |
WhileLoopTransformation.labelStack |
Modifier and Type | Field and Description |
---|---|
java.util.Map<Label,ProgramVariable> |
AuxiliaryContract.Variables.breakFlags
Boolean flags that are set to
true when the block terminates by a
break label; statement with the specified label. |
java.util.Map<Label,Term> |
AuxiliaryContract.Terms.breakFlags |
java.util.Map<Label,ProgramVariable> |
AuxiliaryContract.Variables.continueFlags
Boolean flags that are set to
true when the block terminates by a
continue label; statement with the specified label. |
java.util.Map<Label,Term> |
AuxiliaryContract.Terms.continueFlags |
protected java.util.List<Label> |
AbstractAuxiliaryContractImpl.labels |
Modifier and Type | Method and Description |
---|---|
java.util.List<Label> |
AbstractAuxiliaryContractImpl.getLabels() |
java.util.List<Label> |
AuxiliaryContract.getLabels() |
java.util.List<Label> |
LoopContract.getLoopLabels() |
java.util.List<Label> |
LoopContractImpl.getLoopLabels() |
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(LoopStatement loop,
java.util.List<Label> labels,
IProgramMethod method,
Services services)
Creates a new instance.
|
static AuxiliaryContract.Variables |
AuxiliaryContract.Variables.create(StatementBlock block,
java.util.List<Label> labels,
IProgramMethod method,
Services services)
Creates a new instance.
|
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,
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,
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,
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.
|
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. |
VariablesCreator(JavaStatement statement,
java.util.List<Label> labels,
IProgramMethod method,
Services services)
Constructor.
|
Modifier and Type | Field and Description |
---|---|
java.util.Map<Label,Term> |
JMLSpecFactory.ContractClauses.breaks |
java.util.Map<Label,Term> |
JMLSpecFactory.ContractClauses.continues |
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,
LoopStatement loop,
TextualJMLSpecCase specificationCase)
Creates a set of loop contracts for a loop 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 |
---|---|
Pair<Label,Term> |
JmlTermFactory.createBreaks(Term term,
java.lang.String label) |
Pair<Label,Term> |
JmlTermFactory.createContinues(Term term,
java.lang.String label) |
Pair<Label,Term> |
JmlIO.translateLabeledClause(LabeledParserRuleContext parserRuleContext,
OriginTermLabel.SpecType type)
Interpret a labeled term (breaks clauses, continue clauses).
|
Copyright © 2003-2019 The KeY-Project.