Package | Description |
---|---|
de.uka.ilkd.key.speclang.jml.pretranslation | |
de.uka.ilkd.key.speclang.jml.translation |
Modifier and Type | Method and Description |
---|---|
TextualJMLSpecCase |
TextualJMLSpecCase.merge(TextualJMLSpecCase other)
Merge clauses of two spec cases.
|
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.
|
ImmutableSet<Contract> |
JMLSpecFactory.createJMLOperationContracts(IProgramMethod pm,
TextualJMLSpecCase textualSpecCase)
Creates operation contracts out of the passed JML specification.
|
java.lang.String |
JMLSpecFactory.generateName(IProgramMethod pm,
TextualJMLSpecCase textualSpecCase,
Behavior originalBehavior) |
Copyright © 2003-2019 The KeY-Project.