Package | Description |
---|---|
de.uka.ilkd.key.speclang |
This package contains the specification language frontends of KeY.
|
de.uka.ilkd.key.speclang.jml.pretranslation | |
de.uka.ilkd.key.speclang.jml.translation |
Constructor and Description |
---|
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.
|
Modifier and Type | Method and Description |
---|---|
Behavior |
TextualJMLSpecCase.getBehavior() |
static Behavior |
Behavior.valueOf(java.lang.String name)
Returns the enum constant of this type with the specified name.
|
static Behavior[] |
Behavior.values()
Returns an array containing the constants of this enum type, in
the order they are declared.
|
Constructor and Description |
---|
TextualJMLSpecCase(ImmutableList<java.lang.String> mods,
Behavior behavior) |
Modifier and Type | Method and Description |
---|---|
java.lang.String |
JMLSpecFactory.generateName(IProgramMethod pm,
Behavior originalBehavior,
java.lang.String customName) |
java.lang.String |
JMLSpecFactory.generateName(IProgramMethod pm,
TextualJMLSpecCase textualSpecCase,
Behavior originalBehavior) |
Copyright © 2003-2019 The KeY-Project.