Package | Description |
---|---|
de.uka.ilkd.key.informationflow.po | |
de.uka.ilkd.key.informationflow.proof.init | |
de.uka.ilkd.key.java |
This package contains classes that cover the Java programming language.
|
de.uka.ilkd.key.java.reference |
Elements of the Java syntax tree representing implicit or explicit (named)
references to other program elements.
|
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_references.analyst | |
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 | |
de.uka.ilkd.key.symbolic_execution.util | |
de.uka.ilkd.key.testgen | |
de.uka.ilkd.key.util |
This package is a grab bag of miscellaneous useful code fragments.
|
Modifier and Type | Method and Description |
---|---|
protected IProgramMethod |
LoopInvExecutionPO.getProgramMethod() |
protected IProgramMethod |
InfFlowContractPO.getProgramMethod()
Returns the
IProgramMethod to call. |
protected IProgramMethod |
BlockExecutionPO.getProgramMethod()
Returns the
IProgramMethod to call. |
protected IProgramMethod |
SymbolicExecutionPO.getProgramMethod()
Returns the
IProgramMethod to call. |
Modifier and Type | Method and Description |
---|---|
static StateVars |
StateVars.buildMethodContractPostVars(StateVars preVars,
IProgramMethod pm,
KeYJavaType kjt,
Services services) |
static StateVars |
StateVars.buildMethodContractPreVars(IProgramMethod pm,
KeYJavaType kjt,
Services services) |
Modifier and Type | Method and Description |
---|---|
IProgramMethod |
Recoder2KeYConverter.convert(ConstructorDeclaration cd)
convert a recoder ConstructorDeclaration to a KeY IProgramMethod
(especially the declaration type of its parent is determined and handed
over)
|
IProgramMethod |
Recoder2KeYConverter.convert(DefaultConstructor dc)
convert a recoder DefaultConstructor to a KeY IProgramMethod (especially
the declaration type of its parent is determined and handed over)
|
IProgramMethod |
Recoder2KeYConverter.convert(MethodDeclaration md)
convert a recoder MethodDeclaration to a KeY IProgramMethod (especially
the declaration type of its parent is determined and handed over)
|
IProgramMethod |
CreateArrayMethodBuilder.getArrayInstanceAllocatorMethod(TypeReference arrayTypeReference)
creates the implicit method
<allocate> which is a
stump and given meaning by a contract |
IProgramMethod |
JavaInfo.getConstructor(KeYJavaType kjt,
ImmutableList<KeYJavaType> signature) |
IProgramMethod |
KeYProgModelInfo.getConstructor(KeYJavaType ct,
ImmutableList<KeYJavaType> signature)
retrieves the most specific constructor declared in the given type with
respect to the given signature
|
IProgramMethod |
CreateArrayMethodBuilder.getCreateArrayHelperMethod(TypeReference arrayTypeReference,
ProgramVariable length,
ImmutableList<Field> fields)
create the method declaration of the
<createArrayHelper> method |
IProgramMethod |
CreateArrayMethodBuilder.getCreateArrayMethod(TypeReference arrayTypeReference,
IProgramMethod prepare,
ImmutableList<Field> fields)
creates the implicit method
<createArray> it
fulfills a similar purpose as <createObject> in
addition it sets the arrays length and calls the prepare method |
IProgramMethod |
CreateArrayMethodBuilder.getPrepareArrayMethod(TypeRef arrayRef,
ProgramVariable length,
Expression defaultValue,
ImmutableList<Field> fields)
returns the prepare method for arrays initialising all array fields with
their default value
|
IProgramMethod |
JavaInfo.getProgramMethod(KeYJavaType classType,
java.lang.String methodName,
ImmutableArray<? extends Type> signature,
KeYJavaType context) |
IProgramMethod |
JavaInfo.getProgramMethod(KeYJavaType classType,
java.lang.String methodName,
ImmutableList<? extends Type> signature,
KeYJavaType context)
returns the program methods defined in the given KeYJavaType with name
m and the list of types as signature of the method
|
IProgramMethod |
KeYProgModelInfo.getProgramMethod(KeYJavaType ct,
java.lang.String m,
ImmutableList<? extends Type> signature,
KeYJavaType context)
Returns the IProgramMethods with the given name that is defined
in the given type or in a supertype where it is visible for the
given type, and has a signature that is compatible to the given one.
|
IProgramMethod |
JavaInfo.getProgramMethod(KeYJavaType classType,
java.lang.String methodName,
java.util.List<java.util.List<KeYJavaType>> signature,
KeYJavaType context) |
IProgramMethod |
JavaInfo.getProgramMethod(KeYJavaType classType,
java.lang.String methodName,
ProgramVariable[] args,
KeYJavaType context)
returns the program method defined in the KeYJavaType of the program
variable clv, with the name m, and the KeYJavaTypes of the given array
of program variables as signatures.
|
IProgramMethod |
JavaInfo.getToplevelPM(KeYJavaType kjt,
IProgramMethod pm) |
IProgramMethod |
JavaInfo.getToplevelPM(KeYJavaType kjt,
java.lang.String methodName,
ImmutableList<KeYJavaType> sig) |
IProgramMethod |
Recoder2KeYConverter.processDefaultConstructor(DefaultConstructor df) |
Modifier and Type | Method and Description |
---|---|
ImmutableList<IProgramMethod> |
JavaInfo.getAllProgramMethods(KeYJavaType kjt)
returns all methods from the given Type as IProgramMethods
|
ImmutableList<IProgramMethod> |
KeYProgModelInfo.getAllProgramMethods(KeYJavaType kjt)
Returns all visible methods that are defined in this
class type or any of its supertypes.
|
ImmutableList<IProgramMethod> |
JavaInfo.getConstructors(KeYJavaType kjt) |
ImmutableList<IProgramMethod> |
KeYProgModelInfo.getConstructors(KeYJavaType ct)
Returns the constructors locally defined within the given
class type.
|
Modifier and Type | Method and Description |
---|---|
static ExecutionContext |
KeYJavaASTFactory.executionContext(KeYJavaType classType,
IProgramMethod method,
ReferencePrefix reference)
Create an execution context.
|
IProgramMethod |
CreateArrayMethodBuilder.getCreateArrayMethod(TypeReference arrayTypeReference,
IProgramMethod prepare,
ImmutableList<Field> fields)
creates the implicit method
<createArray> it
fulfills a similar purpose as <createObject> in
addition it sets the arrays length and calls the prepare method |
Term |
JavaInfo.getTermFromProgramMethod(IProgramMethod pm,
java.lang.String methodName,
java.lang.String className,
Term[] args,
Term prefix) |
IProgramMethod |
JavaInfo.getToplevelPM(KeYJavaType kjt,
IProgramMethod pm) |
boolean |
JavaInfo.isCanonicalProgramMethod(IProgramMethod method,
KeYJavaType context)
This is used for pretty printing observer terms.
|
static MethodBodyStatement |
KeYJavaASTFactory.methodBody(ProgramVariable result,
ReferencePrefix reference,
IProgramMethod method,
Expression[] arguments)
Create a method body shortcut.
|
static MethodBodyStatement |
KeYJavaASTFactory.methodBody(ProgramVariable result,
ReferencePrefix reference,
IProgramMethod method,
ImmutableArray<Expression> arguments)
Create a method body shortcut.
|
void |
PrettyPrinter.printFullMethodSignature(IProgramMethod x) |
void |
PrettyPrinter.printMethod(IProgramMethod x) |
void |
PrettyPrinter.printProgramMethod(IProgramMethod x) |
void |
KeYProgModelInfo.putImplicitMethod(IProgramMethod m,
KeYJavaType t) |
protected void |
PrettyPrinter.writeFullMethodSignature(IProgramMethod x) |
Modifier and Type | Method and Description |
---|---|
IProgramMethod |
ExecutionContext.getMethodContext()
returns the program method which is currently active
|
IProgramMethod |
IExecutionContext.getMethodContext()
returns the program method which is currently active
|
IProgramMethod |
MethodReference.method(Services services,
KeYJavaType refPrefixType,
ExecutionContext ec) |
IProgramMethod |
MethodReference.method(Services services,
KeYJavaType classType,
ImmutableList<KeYJavaType> signature,
KeYJavaType context) |
Constructor and Description |
---|
ExecutionContext(TypeReference classContext,
IProgramMethod methodContext,
ReferencePrefix runtimeInstance)
creates an execution context reference
|
Modifier and Type | Method and Description |
---|---|
IProgramMethod |
MethodFrame.getProgramMethod()
Get method.
|
IProgramMethod |
MethodBodyStatement.getProgramMethod(Services services) |
Constructor and Description |
---|
MethodBodyStatement(IProgramMethod method,
ReferencePrefix newContext,
IProgramVariable res,
ImmutableArray<Expression> args) |
MethodBodyStatement(IProgramMethod method,
ReferencePrefix newContext,
IProgramVariable res,
ImmutableArray<Expression> args,
boolean useSpecification) |
MethodBodyStatement(IProgramMethod method,
ReferencePrefix newContext,
IProgramVariable res,
ImmutableArray<Expression> args,
boolean useSpecification,
ProgramElement scope) |
MethodBodyStatement(IProgramMethod method,
ReferencePrefix newContext,
IProgramVariable res,
ImmutableArray<Expression> args,
ProgramElement scope) |
Modifier and Type | Method and Description |
---|---|
void |
Visitor.performActionOnMethod(IProgramMethod x) |
void |
JavaASTVisitor.performActionOnMethod(IProgramMethod x) |
void |
Visitor.performActionOnProgramMethod(IProgramMethod x) |
void |
JavaASTVisitor.performActionOnProgramMethod(IProgramMethod x) |
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 | Method and Description |
---|---|
ImmutableList<IProgramMethod> |
MethodStackInfo.getMethodStack()
returns the method call stack
|
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.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".
|
Modifier and Type | Class and Description |
---|---|
class |
ProgramMethod
The program method represents a (pure) method in the logic.
|
class |
ProgramSV
Objects of this class are schema variables matching program constructs within
modal operators.
|
Modifier and Type | Method and Description |
---|---|
IProgramMethod |
ProgramSV.getMethodContext() |
Modifier and Type | Method and Description |
---|---|
protected IProofReference<IProgramMethod> |
MethodCallProofReferencesAnalyst.createReference(Node node,
Services services,
ExecutionContext context,
MethodReference mr)
Creates an
IProofReference to the called IProgramMethod . |
Modifier and Type | Method and Description |
---|---|
IProgramMethod |
FunctionalBlockContractPO.getProgramMethod() |
IProgramMethod |
FunctionalLoopContractPO.getProgramMethod() |
protected abstract IProgramMethod |
AbstractOperationPO.getProgramMethod()
Returns the
IProgramMethod to call. |
protected IProgramMethod |
FunctionalOperationContractPO.getProgramMethod()
Returns the
IProgramMethod to call. |
Modifier and Type | Method and Description |
---|---|
protected Term |
AbstractPO.generateSelfCreated(java.util.List<LocationVariable> heaps,
IProgramMethod pm,
ProgramVariable selfVar,
Services services)
Generates the general assumption that self is created.
|
protected Term |
AbstractPO.generateSelfExactType(IProgramMethod pm,
ProgramVariable selfVar,
KeYJavaType selfKJT)
Generates the general assumption which defines the type of self.
|
protected Term |
AbstractPO.generateSelfExactType(IProgramMethod pm,
Term selfVar,
KeYJavaType selfKJT)
Generates the general assumption which defines the type of self.
|
protected Term |
AbstractPO.generateSelfNotNull(IProgramMethod pm,
ProgramVariable selfVar)
Generates the general assumption that self is not null.
|
Constructor and Description |
---|
ProofObligationVars(IProgramMethod pm,
KeYJavaType kjt,
Services services) |
Modifier and Type | Method and Description |
---|---|
ImmutableSet<FunctionalOperationContract> |
SpecificationRepository.getOperationContracts(KeYJavaType kjt,
IProgramMethod pm)
Returns all registered (atomic) operation contracts for the passed
operation.
|
ImmutableSet<FunctionalOperationContract> |
SpecificationRepository.getOperationContracts(KeYJavaType kjt,
IProgramMethod pm,
Modality modality)
Returns all registered (atomic) operation contracts for the passed
operation which refer to the passed modality.
|
Modifier and Type | Field and Description |
---|---|
IProgramMethod |
UseOperationContractRule.Instantiation.pm
The program method.
|
Modifier and Type | Method and Description |
---|---|
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) ) |
Constructor and Description |
---|
Instantiation(Term u,
Term progPost,
Modality mod,
Expression actualResult,
Term actualSelf,
KeYJavaType staticType,
MethodOrConstructorReference mr,
IProgramMethod pm,
ImmutableList<Term> actualParams,
boolean transaction)
Creates a new instantiation for the contract rule and the given variables.
|
Modifier and Type | Method and Description |
---|---|
protected IProgramMethod |
MethodCall.getMethod(KeYJavaType prefixType,
MethodReference mr,
Services services)
Returns the method.
|
Modifier and Type | Field and Description |
---|---|
protected IProgramMethod |
AbstractAuxiliaryContractImpl.method |
Modifier and Type | Method and Description |
---|---|
IProgramMethod |
AbstractAuxiliaryContractImpl.getMethod() |
IProgramMethod |
FunctionalAuxiliaryContract.getMethod() |
IProgramMethod |
AuxiliaryContract.getMethod() |
IProgramMethod |
AbstractAuxiliaryContractImpl.getTarget() |
IProgramMethod |
FunctionalAuxiliaryContract.getTarget() |
IProgramMethod |
FunctionalOperationContractImpl.getTarget() |
IProgramMethod |
InformationFlowContractImpl.getTarget() |
IProgramMethod |
InformationFlowContract.getTarget() |
IProgramMethod |
LoopSpecification.getTarget()
Returns the contracted function symbol.
|
IProgramMethod |
OperationContract.getTarget() |
IProgramMethod |
AuxiliaryContract.getTarget() |
IProgramMethod |
LoopSpecImpl.getTarget() |
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) |
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) |
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.
|
InformationFlowContract |
ContractFactory.createInformationFlowContract(KeYJavaType forClass,
IProgramMethod pm,
KeYJavaType specifiedIn,
Modality modality,
Term requires,
Term requiresFree,
Term measuredBy,
Term modifies,
boolean hasMod,
ProgramVariableCollection progVars,
Term accessible,
ImmutableList<InfFlowSpec> infFlowSpecs,
boolean toBeSaved) |
ImmutableSet<BlockContract> |
SpecExtractor.extractBlockContracts(IProgramMethod method,
LabeledStatement labeled)
Returns the block contracts for the passed labeled statement if it labels
a block.
|
ImmutableSet<BlockContract> |
SpecExtractor.extractBlockContracts(IProgramMethod method,
StatementBlock block)
Returns the block contracts for the passed block.
|
ImmutableSet<LoopContract> |
SpecExtractor.extractLoopContracts(IProgramMethod method,
LabeledStatement labeled)
Returns the loop contracts for the passed labeled statement if it labels
a block.
|
ImmutableSet<LoopContract> |
SpecExtractor.extractLoopContracts(IProgramMethod method,
LoopStatement loop)
Returns the loop contracts for the passed loop.
|
ImmutableSet<LoopContract> |
SpecExtractor.extractLoopContracts(IProgramMethod method,
StatementBlock block)
Returns the loop contracts for the passed block.
|
LoopSpecification |
SpecExtractor.extractLoopInvariant(IProgramMethod pm,
LoopStatement loop)
Returns the loop invariant for the passed loop (if any).
|
ImmutableSet<MergeContract> |
SpecExtractor.extractMergeContracts(IProgramMethod method,
MergePointStatement mps,
ImmutableList<ProgramVariable> methodParams)
Returns the
MergeContract s for the given
MergePointStatement . |
ImmutableSet<SpecificationElement> |
SpecExtractor.extractMethodSpecs(IProgramMethod pm)
Returns the operation contracts for the passed operation.
|
ImmutableSet<SpecificationElement> |
SpecExtractor.extractMethodSpecs(IProgramMethod pm,
boolean addInvariant) |
FunctionalOperationContract |
ContractFactory.func(IProgramMethod pm,
InitiallyClause ini)
|
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,
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.
|
LoopSpecification |
LoopSpecification.setTarget(IProgramMethod newPM) |
LoopSpecification |
LoopSpecImpl.setTarget(IProgramMethod newPM) |
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,
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.
|
InformationFlowContractImpl(java.lang.String baseName,
KeYJavaType forClass,
IProgramMethod pm,
KeYJavaType specifiedIn,
Modality modality,
Term pre,
Term freePre,
Term mby,
Term mod,
boolean hasRealMod,
Term self,
ImmutableList<Term> params,
Term result,
Term exc,
Term heapAtPre,
Term dep,
ImmutableList<InfFlowSpec> infFlowSpecs,
boolean toBeSaved) |
InformationFlowContractImpl(java.lang.String baseName,
java.lang.String name,
KeYJavaType forClass,
IProgramMethod pm,
KeYJavaType specifiedIn,
Modality modality,
Term pre,
Term freePre,
Term mby,
Term mod,
boolean hasRealMod,
Term self,
ImmutableList<Term> params,
Term result,
Term exc,
Term heapAtPre,
Term dep,
ImmutableList<InfFlowSpec> infFlowSpecs,
boolean toBeSaved,
int id) |
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.
|
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.
|
QueryAxiom(java.lang.String name,
IProgramMethod target,
KeYJavaType kjt) |
VariablesCreator(JavaStatement statement,
java.util.List<Label> labels,
IProgramMethod method,
Services services)
Constructor.
|
Modifier and Type | Method and Description |
---|---|
ImmutableSet<BlockContract> |
JMLSpecExtractor.extractBlockContracts(IProgramMethod method,
LabeledStatement labeled) |
ImmutableSet<BlockContract> |
JMLSpecExtractor.extractBlockContracts(IProgramMethod method,
StatementBlock block) |
ImmutableSet<LoopContract> |
JMLSpecExtractor.extractLoopContracts(IProgramMethod method,
LabeledStatement labeled) |
ImmutableSet<LoopContract> |
JMLSpecExtractor.extractLoopContracts(IProgramMethod method,
LoopStatement loop) |
ImmutableSet<LoopContract> |
JMLSpecExtractor.extractLoopContracts(IProgramMethod method,
StatementBlock block) |
LoopSpecification |
JMLSpecExtractor.extractLoopInvariant(IProgramMethod pm,
LoopStatement loop) |
ImmutableSet<MergeContract> |
JMLSpecExtractor.extractMergeContracts(IProgramMethod method,
MergePointStatement mps,
ImmutableList<ProgramVariable> methodParams) |
ImmutableSet<SpecificationElement> |
JMLSpecExtractor.extractMethodSpecs(IProgramMethod pm) |
ImmutableSet<SpecificationElement> |
JMLSpecExtractor.extractMethodSpecs(IProgramMethod pm,
boolean addInvariant)
Extracts method specifications (i.e., contracts) from Java+JML input.
|
static boolean |
JMLInfoExtractor.isHelper(IProgramMethod pm)
Returns true iff the given method is specified "helper".
|
static boolean |
JMLInfoExtractor.isPure(IProgramMethod pm)
Returns true iff the given method is specified "pure".
|
static boolean |
JMLInfoExtractor.isStrictlyPure(IProgramMethod pm)
Returns true iff the given method is specified "strictly_pure"
or the containing type is specified so.
|
static boolean |
JMLInfoExtractor.parameterIsNullable(IProgramMethod pm,
int pos)
Returns true iff the
pos -th parameter of the given method
is declared "nullable" (implicitly or explicitly). |
static boolean |
JMLInfoExtractor.parameterIsNullable(IProgramMethod pm,
ParameterDeclaration pd)
Returns true iff the parameter of the given method
is declared "nullable" (implicitly or explicitly).
|
static boolean |
JMLInfoExtractor.resultIsNullable(IProgramMethod pm) |
Modifier and Type | Method and Description |
---|---|
protected ImmutableList<ProgramVariable> |
JMLSpecFactory.collectLocalVariablesVisibleTo(Statement statement,
IProgramMethod method) |
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<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.
|
LoopSpecification |
JMLSpecFactory.createJMLLoopInvariant(IProgramMethod pm,
LoopStatement loop,
TextualJMLLoopSpec textualLoopSpec) |
ImmutableSet<MergeContract> |
JMLSpecFactory.createJMLMergeContracts(IProgramMethod method,
MergePointStatement mps,
TextualJMLMergePointDecl mergePointDecl,
ImmutableList<ProgramVariable> methodParams) |
ImmutableSet<Contract> |
JMLSpecFactory.createJMLOperationContracts(IProgramMethod pm,
TextualJMLSpecCase textualSpecCase)
Creates operation contracts out of the passed JML specification.
|
ProgramVariableCollection |
JMLSpecFactory.createProgramVariables(IProgramMethod pm) |
java.lang.String |
JMLSpecFactory.generateName(IProgramMethod pm,
Behavior originalBehavior,
java.lang.String customName) |
java.lang.String |
JMLSpecFactory.generateName(IProgramMethod pm,
TextualJMLSpecCase textualSpecCase,
Behavior originalBehavior) |
FunctionalOperationContract |
JMLSpecFactory.initiallyClauseToContract(InitiallyClause ini,
IProgramMethod pm)
Translate initially clause to a contract for the given constructor.
|
Modifier and Type | Method and Description |
---|---|
IProgramMethod |
ExecutionNodeReader.KeYlessOperationContract.getContractProgramMethod()
Returns the
IProgramMethod of the applied Contract . |
IProgramMethod |
ExecutionNodeReader.KeYlessMethodCall.getExplicitConstructorProgramMethod()
Returns the explicit constructor.
|
IProgramMethod |
ExecutionNodeReader.KeYlessMethodCall.getProgramMethod()
Returns the called
IProgramMethod . |
Modifier and Type | Method and Description |
---|---|
IProgramMethod |
IExecutionOperationContract.getContractProgramMethod()
Returns the
IProgramMethod of the applied Contract . |
IProgramMethod |
IExecutionMethodCall.getExplicitConstructorProgramMethod()
Returns the explicit constructor.
|
IProgramMethod |
IExecutionMethodCall.getProgramMethod()
Returns the called
IProgramMethod . |
Modifier and Type | Method and Description |
---|---|
IProgramMethod |
ExecutionOperationContract.getContractProgramMethod()
Returns the
IProgramMethod of the applied Contract . |
IProgramMethod |
ExecutionMethodCall.getExplicitConstructorProgramMethod()
Returns the explicit constructor.
|
IProgramMethod |
ExecutionMethodCall.getProgramMethod()
Returns the called
IProgramMethod . |
Modifier and Type | Method and Description |
---|---|
IProgramMethod |
ProgramMethodPO.getProgramMethod()
Returns the
IProgramMethod to call. |
static IProgramMethod |
ProgramMethodPO.getProgramMethod(InitConfig initConfig,
java.util.Properties properties)
Searches the
IProgramMethod defined by the given Properties . |
Modifier and Type | Method and Description |
---|---|
static java.lang.String |
ProgramMethodPO.getProgramMethodSignature(IProgramMethod pm,
boolean includeType)
Returns a human readable full qualified method signature.
|
Constructor and Description |
---|
ProgramMethodPO(InitConfig initConfig,
java.lang.String name,
IProgramMethod pm,
java.lang.String precondition)
Constructor.
|
ProgramMethodPO(InitConfig initConfig,
java.lang.String name,
IProgramMethod pm,
java.lang.String precondition,
boolean addUninterpretedPredicate,
boolean addSymbolicExecutionLabel)
Constructor.
|
ProgramMethodSubsetPO(InitConfig initConfig,
java.lang.String name,
IProgramMethod pm,
java.lang.String precondition,
Position startPosition,
Position endPosition)
Constructor.
|
ProgramMethodSubsetPO(InitConfig initConfig,
java.lang.String name,
IProgramMethod pm,
java.lang.String precondition,
Position startPosition,
Position endPosition,
boolean addUninterpretedPredicate,
boolean addSymbolicExecutionLabel)
Constructor.
|
Modifier and Type | Method and Description |
---|---|
IProgramMethod |
AbstractConditionalBreakpoint.getPm() |
Modifier and Type | Method and Description |
---|---|
void |
AbstractConditionalBreakpoint.setPm(IProgramMethod pm) |
Constructor and Description |
---|
AbstractConditionalBreakpoint(int hitCount,
IProgramMethod pm,
Proof proof,
boolean enabled,
boolean conditionEnabled,
int methodStart,
int methodEnd,
KeYJavaType containerType)
Creates a new
AbstractConditionalBreakpoint . |
LineBreakpoint(java.lang.String classPath,
int lineNumber,
int hitCount,
IProgramMethod pm,
Proof proof,
java.lang.String condition,
boolean enabled,
boolean conditionEnabled,
int methodStart,
int methodEnd)
Creates a new
LineBreakpoint . |
MethodBreakpoint(java.lang.String classPath,
int lineNumber,
int hitCount,
IProgramMethod pm,
Proof proof,
java.lang.String condition,
boolean enabled,
boolean conditionEnabled,
int methodStart,
int methodEnd,
boolean isEntry,
boolean isExit)
Creates a new
LineBreakpoint . |
Modifier and Type | Method and Description |
---|---|
static SymbolicExecutionUtil.SiteProofVariableValueInput |
SymbolicExecutionUtil.createExtractReturnVariableValueSequent(Services services,
TypeReference contextObjectType,
IProgramMethod contextMethod,
ReferencePrefix contextObject,
Node methodReturnNode,
Node methodCallEmptyNode,
IProgramVariable variable)
Creates a
Sequent which can be used in site proofs to
extract the return value of the given IProgramVariable from the
sequent of the given Node . |
static boolean |
SymbolicExecutionUtil.isNotImplicit(Services services,
IProgramMethod pm)
Checks if the given
IProgramMethod is not implicit. |
Modifier and Type | Method and Description |
---|---|
IProgramMethod |
ProofInfo.getMUT() |
Modifier and Type | Method and Description |
---|---|
static IProgramMethod |
KeYTypeUtil.findExplicitConstructor(Services services,
IProgramMethod implicitConstructor)
Returns the
IProgramMethod of the explicit constructor for
the given implicit constructor. |
static IProgramMethod |
HelperClassForTests.searchProgramMethod(Services services,
java.lang.String containerTypeName,
java.lang.String methodFullName)
Searches a
IProgramMethod in the given Services . |
Modifier and Type | Method and Description |
---|---|
static IProgramMethod |
KeYTypeUtil.findExplicitConstructor(Services services,
IProgramMethod implicitConstructor)
Returns the
IProgramMethod of the explicit constructor for
the given implicit constructor. |
static boolean |
KeYTypeUtil.isImplicitConstructor(IProgramMethod pm)
Checks if the given
IProgramMethod is an implicit constructor. |
Copyright © 2003-2019 The KeY-Project.