All Methods Static Methods Instance Methods Concrete Methods
Modifier and Type |
Method and Description |
private ImmutableList<ProgramVariable> |
append(ImmutableList<ProgramVariable> localVars,
ImmutableList<LocationVariable> paramVars) |
private ImmutableList<ProgramVariable> |
collectLocalVariables(StatementContainer sc,
LoopStatement loop)
Collects local variables of the passed statement that are visible for the passed loop.
|
protected ImmutableList<ProgramVariable> |
collectLocalVariablesVisibleTo(Statement statement,
IProgramMethod method) |
private ImmutableList<ProgramVariable> |
collectLocalVariablesVisibleTo(Statement statement,
StatementContainer container) |
private static java.util.Map<LocationVariable,Term> |
createAtPres(ImmutableList<LocationVariable> paramVars,
ImmutableList<LocationVariable> allHeaps,
TermBuilder tb) |
private ImmutableSet<Contract> |
createDependencyOperationContract(IProgramMethod pm,
ProgramVariableCollection progVars,
JMLSpecFactory.ContractClauses clauses)
Generate dependency operation contract out of the JML accessible clause.
|
private 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.
|
private ImmutableSet<Contract> |
createInformationFlowContracts(JMLSpecFactory.ContractClauses clauses,
IProgramMethod pm,
ProgramVariableCollection progVars) |
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,
PositionedString originalInv) |
Contract |
createJMLDependencyContract(KeYJavaType kjt,
LocationVariable targetHeap,
PositionedString originalDep) |
Contract |
createJMLDependencyContract(KeYJavaType kjt,
TextualJMLDepends textualDep) |
InitiallyClause |
createJMLInitiallyClause(KeYJavaType kjt,
TextualJMLInitially textualInv) |
InitiallyClause |
createJMLInitiallyClause(KeYJavaType kjt,
VisibilityModifier visibility,
PositionedString 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.
|
private LoopSpecification |
createJMLLoopInvariant(IProgramMethod pm,
LoopStatement loop,
java.util.Map<java.lang.String,ImmutableList<PositionedString>> originalInvariants,
java.util.Map<java.lang.String,ImmutableList<PositionedString>> originalFreeInvariants,
java.util.Map<java.lang.String,ImmutableList<PositionedString>> originalAssignables,
ImmutableList<PositionedString> originalInfFlowSpecs,
PositionedString originalVariant) |
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,
PositionedString originalRep,
boolean isStatic) |
private ImmutableList<PositionedString> |
createPrecond(IProgramMethod pm,
PositionedString originalSpec) |
private ProgramVariableCollection |
createProgramVariables(IProgramMethod pm) |
private ProgramVariableCollection |
createProgramVariables(IProgramMethod method,
JavaStatement block,
AuxiliaryContract.Variables variables)
Creates a program variable collection for a specified block.
|
private java.lang.String |
generateName(IProgramMethod pm,
TextualJMLSpecCase textualSpecCase,
Behavior originalBehavior) |
private java.util.Map<LocationVariable,Term> |
generatePostCondition(ProgramVariableCollection progVars,
JMLSpecFactory.ContractClauses clauses,
Behavior originalBehavior) |
private java.util.Map<LocationVariable,Term> |
generateRepresentsAxioms(ProgramVariableCollection progVars,
JMLSpecFactory.ContractClauses clauses,
Behavior originalBehavior) |
private java.lang.String |
getContractName(IProgramMethod programMethod,
Behavior behavior) |
private java.lang.String |
getDefaultInvName(java.lang.String name,
KeYJavaType kjt) |
private java.lang.String |
getInicName() |
private VisibilityModifier |
getVisibility(TextualJMLConstruct textualConstruct) |
FunctionalOperationContract |
initiallyClauseToContract(InitiallyClause ini,
IProgramMethod pm)
Translate initially clause to a contract for the given constructor.
|
private ImmutableList<Term> |
registerAbbreviationVariables(TextualJMLSpecCase textualSpecCase,
KeYJavaType inClass,
ProgramVariableCollection progVars,
JMLSpecFactory.ContractClauses clauses)
register abbreviations in contracts (aka. old clauses). creates update terms.
|
private java.util.Map<LocationVariable,Term> |
termify(java.util.Map<LocationVariable,LocationVariable> remembranceVariables) |
private void |
translateAccessible(IProgramMethod pm,
ProgramVariableCollection progVars,
LocationVariable heap,
ProgramVariable heapAtPre,
LocationVariable savedHeap,
ImmutableList<PositionedString> accessible,
ImmutableList<PositionedString> accessiblePre,
JMLSpecFactory.ContractClauses clauses) |
private Term |
translateAccessible(IProgramMethod pm,
ProgramVariable selfVar,
ImmutableList<ProgramVariable> paramVars,
java.util.Map<LocationVariable,Term> atPres,
java.util.Map<LocationVariable,Term> atBefores,
ImmutableList<PositionedString> originalClauses) |
private Term |
translateAndClauses(IProgramMethod pm,
ProgramVariable selfVar,
ImmutableList<ProgramVariable> paramVars,
ProgramVariable resultVar,
ProgramVariable excVar,
java.util.Map<LocationVariable,Term> atPres,
java.util.Map<LocationVariable,Term> atBefores,
ImmutableList<PositionedString> originalClauses)
Clauses are expected to be conjoined in a right-associative way, i.e.
|
private void |
translateAssignable(IProgramMethod pm,
ProgramVariableCollection progVars,
LocationVariable heap,
LocationVariable savedHeap,
ImmutableList<PositionedString> mod,
JMLSpecFactory.ContractClauses clauses) |
private Term |
translateAssignable(IProgramMethod pm,
ProgramVariable selfVar,
ImmutableList<ProgramVariable> paramVars,
java.util.Map<LocationVariable,Term> atPres,
java.util.Map<LocationVariable,Term> atBefores,
ImmutableList<PositionedString> originalClauses) |
private void |
translateAxioms(IProgramMethod pm,
ProgramVariableCollection progVars,
LocationVariable heap,
ImmutableList<PositionedString> axioms,
JMLSpecFactory.ContractClauses clauses,
Behavior originalBehavior) |
private java.util.Map<Label,Term> |
translateBreaks(IProgramMethod pm,
ProgramVariable selfVar,
ImmutableList<ProgramVariable> paramVars,
ProgramVariable resultVar,
ProgramVariable excVar,
java.util.Map<LocationVariable,Term> atPres,
java.util.Map<LocationVariable,Term> atBefores,
Behavior originalBehavior,
ImmutableList<PositionedString> originalClauses) |
private java.util.Map<Label,Term> |
translateContinues(IProgramMethod pm,
ProgramVariable selfVar,
ImmutableList<ProgramVariable> paramVars,
ProgramVariable resultVar,
ProgramVariable excVar,
java.util.Map<LocationVariable,Term> atPres,
java.util.Map<LocationVariable,Term> atBefores,
Behavior originalBehavior,
ImmutableList<PositionedString> originalClauses) |
private Term |
translateDecreases(IProgramMethod pm,
ProgramVariable selfVar,
ImmutableList<ProgramVariable> paramVars,
java.util.Map<LocationVariable,Term> atPres,
java.util.Map<LocationVariable,Term> atBefores,
ImmutableList<PositionedString> originalDecreases) |
private void |
translateEnsures(IProgramMethod pm,
ProgramVariableCollection progVars,
LocationVariable heap,
LocationVariable savedHeap,
ImmutableList<PositionedString> ensures,
ImmutableList<PositionedString> ensuresFree,
JMLSpecFactory.ContractClauses clauses,
Behavior originalBehavior) |
private Term |
translateEnsures(IProgramMethod pm,
ProgramVariable selfVar,
ImmutableList<ProgramVariable> paramVars,
ProgramVariable resultVar,
ProgramVariable excVar,
java.util.Map<LocationVariable,Term> atPres,
java.util.Map<LocationVariable,Term> atBefores,
Behavior originalBehavior,
ImmutableList<PositionedString> originalClauses) |
private ImmutableList<InfFlowSpec> |
translateInfFlowSpecClauses(IProgramMethod pm,
ProgramVariable selfVar,
ImmutableList<ProgramVariable> paramVars,
ProgramVariable resultVar,
ProgramVariable excVar,
ImmutableList<PositionedString> originalClauses) |
private JMLSpecFactory.ContractClauses |
translateJMLClauses(IProgramMethod pm,
TextualJMLSpecCase textualSpecCase,
ProgramVariableCollection progVars,
Behavior originalBehavior) |
private Term |
translateMeasuredBy(IProgramMethod pm,
ProgramVariable selfVar,
ImmutableList<ProgramVariable> paramVars,
ImmutableList<PositionedString> originalMeasuredBy) |
private Term |
translateOrClauses(IProgramMethod pm,
ProgramVariable selfVar,
ImmutableList<ProgramVariable> paramVars,
ImmutableList<PositionedString> originalClauses) |
private void |
translateRequires(IProgramMethod pm,
ProgramVariableCollection progVars,
LocationVariable heap,
LocationVariable savedHeap,
ImmutableList<PositionedString> requires,
ImmutableList<PositionedString> requiresFree,
JMLSpecFactory.ContractClauses clauses) |
private Term |
translateReturns(IProgramMethod pm,
ProgramVariable selfVar,
ImmutableList<ProgramVariable> paramVars,
ProgramVariable resultVar,
ProgramVariable excVar,
java.util.Map<LocationVariable,Term> atPres,
java.util.Map<LocationVariable,Term> atBefores,
Behavior originalBehavior,
ImmutableList<PositionedString> originalClauses) |
private Term |
translateSignals(IProgramMethod pm,
ProgramVariable selfVar,
ImmutableList<ProgramVariable> paramVars,
ProgramVariable resultVar,
ProgramVariable excVar,
java.util.Map<LocationVariable,Term> atPres,
java.util.Map<LocationVariable,Term> atBefores,
Behavior originalBehavior,
ImmutableList<PositionedString> originalClauses) |
private Term |
translateSignalsOnly(IProgramMethod pm,
ProgramVariable excVar,
Behavior originalBehavior,
ImmutableList<PositionedString> originalClauses) |
private boolean |
translateStrictlyPure(IProgramMethod pm,
ProgramVariable selfVar,
ImmutableList<ProgramVariable> paramVars,
ImmutableList<PositionedString> assignableClauses) |
private java.util.Map<LocationVariable,Term> |
translateToTermAsssignable(IProgramMethod pm,
ProgramVariable selfVar,
java.util.Map<LocationVariable,Term> atPres,
ImmutableList<ProgramVariable> allVars,
java.util.Map<java.lang.String,ImmutableList<PositionedString>> originalAssignables) |
private static java.util.Map<LocationVariable,Term> |
translateToTermFreeInvariants(IProgramMethod pm,
java.util.Map<java.lang.String,ImmutableList<PositionedString>> originalFreeInvariants,
ProgramVariable selfVar,
ImmutableList<ProgramVariable> allVars,
ImmutableList<LocationVariable> allHeaps,
java.util.Map<LocationVariable,Term> atPres,
Services services,
TermBuilder tb) |
private java.util.Map<LocationVariable,ImmutableList<InfFlowSpec>> |
translateToTermInfFlowSpecs(IProgramMethod pm,
ProgramVariable selfVar,
ProgramVariable resultVar,
ProgramVariable excVar,
ImmutableList<ProgramVariable> allVars,
ImmutableList<LocationVariable> allHeaps,
ImmutableList<PositionedString> originalInfFlowSpecs) |
private static java.util.Map<LocationVariable,Term> |
translateToTermInvariants(IProgramMethod pm,
java.util.Map<java.lang.String,ImmutableList<PositionedString>> originalInvariants,
ProgramVariable selfVar,
ImmutableList<ProgramVariable> allVars,
ImmutableList<LocationVariable> allHeaps,
java.util.Map<LocationVariable,Term> atPres,
Services services,
TermBuilder tb) |
private Term |
translateToTermVariant(IProgramMethod pm,
ProgramVariable selfVar,
java.util.Map<LocationVariable,Term> atPres,
ImmutableList<ProgramVariable> allVars,
PositionedString originalVariant) |
private Term |
translateUnionClauses(IProgramMethod pm,
ProgramVariable selfVar,
ImmutableList<ProgramVariable> paramVars,
java.util.Map<LocationVariable,Term> atPres,
java.util.Map<LocationVariable,Term> atBefores,
ImmutableList<PositionedString> originalClauses) |