All Methods Instance Methods Concrete Methods
Modifier and Type |
Method and Description |
protected ImmutableList<ProgramVariable> |
collectLocalVariablesVisibleTo(Statement statement,
IProgramMethod method) |
ImmutableSet<Contract> |
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<BlockContract> |
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.
|
ClassAxiom |
createJMLClassAxiom(KeYJavaType kjt,
TextualJMLClassAxiom textual)
Creates a class axiom from a textual JML representation.
|
ClassInvariant |
createJMLClassInvariant(KeYJavaType kjt,
TextualJMLClassInv textualInv) |
ClassInvariant |
createJMLClassInvariant(KeYJavaType kjt,
VisibilityModifier visibility,
boolean isStatic,
LabeledParserRuleContext originalInv) |
Contract |
createJMLDependencyContract(KeYJavaType kjt,
LocationVariable targetHeap,
LabeledParserRuleContext originalDep) |
Contract |
createJMLDependencyContract(KeYJavaType kjt,
TextualJMLDepends textualDep) |
InitiallyClause |
createJMLInitiallyClause(KeYJavaType kjt,
TextualJMLInitially textualInv) |
InitiallyClause |
createJMLInitiallyClause(KeYJavaType kjt,
VisibilityModifier visibility,
LabeledParserRuleContext original) |
ImmutableSet<LoopContract> |
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> |
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.
|
LoopSpecification |
createJMLLoopInvariant(IProgramMethod pm,
LoopStatement loop,
TextualJMLLoopSpec textualLoopSpec) |
ImmutableSet<MergeContract> |
createJMLMergeContracts(IProgramMethod method,
MergePointStatement mps,
TextualJMLMergePointDecl mergePointDecl,
ImmutableList<ProgramVariable> methodParams) |
ImmutableSet<Contract> |
createJMLOperationContracts(IProgramMethod pm,
TextualJMLSpecCase textualSpecCase)
Creates operation contracts out of the passed JML specification.
|
ClassAxiom |
createJMLRepresents(KeYJavaType kjt,
TextualJMLRepresents textualRep) |
ClassAxiom |
createJMLRepresents(KeYJavaType kjt,
VisibilityModifier visibility,
LabeledParserRuleContext originalRep,
boolean isStatic) |
ProgramVariableCollection |
createProgramVariables(IProgramMethod pm) |
java.lang.String |
generateName(IProgramMethod pm,
Behavior originalBehavior,
java.lang.String customName) |
java.lang.String |
generateName(IProgramMethod pm,
TextualJMLSpecCase textualSpecCase,
Behavior originalBehavior) |
protected java.lang.String |
getDefaultInvName(java.lang.String name,
KeYJavaType kjt) |
FunctionalOperationContract |
initiallyClauseToContract(InitiallyClause ini,
IProgramMethod pm)
Translate initially clause to a contract for the given constructor.
|