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.translation |
Modifier and Type | Method and Description |
---|---|
void |
SpecificationRepository.addInitiallyClause(InitiallyClause ini)
Registers the passed initially clause.
|
Modifier and Type | Method and Description |
---|---|
void |
SpecificationRepository.addInitiallyClauses(ImmutableSet<InitiallyClause> toAdd)
Registers the passed initially clauses.
|
Modifier and Type | Class and Description |
---|---|
class |
InitiallyClauseImpl
Standard implementation of the InitiallyClause interface.
|
Modifier and Type | Method and Description |
---|---|
InitiallyClause |
InitiallyClauseImpl.map(java.util.function.UnaryOperator<Term> op,
Services services) |
InitiallyClause |
InitiallyClause.map(java.util.function.UnaryOperator<Term> op,
Services services) |
InitiallyClause |
InitiallyClauseImpl.setKJT(KeYJavaType newKjt) |
InitiallyClause |
InitiallyClause.setKJT(KeYJavaType newKjt) |
Modifier and Type | Method and Description |
---|---|
FunctionalOperationContract |
ContractFactory.addPost(FunctionalOperationContract old,
InitiallyClause ini)
Add the specification contained in InitiallyClause as a postcondition.
|
FunctionalOperationContract |
ContractFactory.func(IProgramMethod pm,
InitiallyClause ini)
|
Modifier and Type | Method and Description |
---|---|
InitiallyClause |
JMLSpecFactory.createJMLInitiallyClause(KeYJavaType kjt,
TextualJMLInitially textualInv) |
InitiallyClause |
JMLSpecFactory.createJMLInitiallyClause(KeYJavaType kjt,
VisibilityModifier visibility,
LabeledParserRuleContext original) |
Modifier and Type | Method and Description |
---|---|
FunctionalOperationContract |
JMLSpecFactory.initiallyClauseToContract(InitiallyClause ini,
IProgramMethod pm)
Translate initially clause to a contract for the given constructor.
|
Copyright © 2003-2019 The KeY-Project.