Package | Description |
---|---|
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 |
---|---|
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) |
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.
|
Modifier and Type | Method and Description |
---|---|
ProgramVariableCollection |
JMLSpecFactory.createProgramVariables(IProgramMethod pm) |
Modifier and Type | Method and Description |
---|---|
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.
|
Copyright © 2003-2019 The KeY-Project.