Package | Description |
---|---|
de.uka.ilkd.key.proof.mgt |
This package contains classes for proof environments and proof management.
|
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.speclang.translation | |
de.uka.ilkd.key.symbolic_execution.strategy.breakpoint |
Modifier and Type | Method and Description |
---|---|
void |
SpecificationRepository.createContractsFromInitiallyClauses()
Adds postconditions raising from initially clauses to all constructors.
|
Modifier and Type | Method and Description |
---|---|
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<SpecificationElement> |
SpecExtractor.extractClassSpecs(KeYJavaType kjt)
Returns the class invariants for the passed type.
|
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)
|
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.
|
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.
|
ClassAxiom |
JMLSpecFactory.createJMLRepresents(KeYJavaType kjt,
TextualJMLRepresents textualRep) |
ClassAxiom |
JMLSpecFactory.createJMLRepresents(KeYJavaType kjt,
VisibilityModifier visibility,
LabeledParserRuleContext originalRep,
boolean isStatic) |
protected SLExpression |
JMLBuiltInPropertyResolver.doResolving(SLExpression receiver,
java.lang.String name,
SLParameters parameters) |
FunctionalOperationContract |
JMLSpecFactory.initiallyClauseToContract(InitiallyClause ini,
IProgramMethod pm)
Translate initially clause to a contract for the given constructor.
|
Modifier and Type | Class and Description |
---|---|
class |
SLWarningException |
Modifier and Type | Method and Description |
---|---|
SLTranslationException |
SLExceptionFactory.convertException(org.antlr.runtime.RecognitionException e)
Converts an ANTLRException into an SLTranslationException with the same
message and stack trace, and with current absolute position information.
|
SLTranslationException |
SLExceptionFactory.convertException(java.lang.String message,
org.antlr.runtime.RecognitionException e) |
SLTranslationException |
SLExceptionFactory.createException(java.lang.String message)
Creates an SLTranslationException with current absolute position
information.
|
SLTranslationException |
SLExceptionFactory.createException(java.lang.String message,
java.lang.Throwable cause)
Creates an SLTranslationException with current absolute position
information.
|
SLTranslationException |
SLExceptionFactory.createException(java.lang.String message,
org.antlr.runtime.Token t)
Creates an SLTranslationException with the position information of the
passed token.
|
SLTranslationException |
SLExceptionFactory.createException(java.lang.String message,
org.antlr.runtime.Token t,
java.lang.Throwable cause)
Creates an SLTranslationException with the position information of the
passed token.
|
SLTranslationException |
SLExceptionFactory.createWarningException(java.lang.String message)
Creates an SLWarningException with current absolute position
information.
|
SLTranslationException |
SLExceptionFactory.createWarningException(java.lang.String message,
org.antlr.runtime.Token t) |
Modifier and Type | Method and Description |
---|---|
void |
AbstractConditionalBreakpoint.setCondition(java.lang.String condition)
Sets the condition to the Term that is parsed from the given String.
|
Constructor and Description |
---|
KeYWatchpoint(int hitCount,
Proof proof,
java.lang.String condition,
boolean enabled,
boolean conditionEnabled,
KeYJavaType containerType,
boolean suspendOnTrue)
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 . |
Copyright © 2003-2019 The KeY-Project.