public final class SpecificationRepository
extends java.lang.Object
Modifier and Type | Field and Description |
---|---|
static java.lang.String |
CONTRACT_COMBINATION_MARKER |
static java.lang.String |
LIMIT_SUFFIX |
Constructor and Description |
---|
SpecificationRepository(Services services) |
Modifier and Type | Method and Description |
---|---|
void |
addBlockContract(BlockContract contract)
Adds a new
BlockContract and a new FunctionalBlockContract
to the repository. |
void |
addBlockContract(BlockContract contract,
boolean addFunctionalContract)
Adds a new
BlockContract to the repository. |
void |
addClassAxiom(ClassAxiom ax)
Registers the passed class axiom.
|
void |
addClassAxioms(ImmutableSet<ClassAxiom> toAdd)
Registers the passed class axioms.
|
void |
addClassInvariant(ClassInvariant inv)
Registers the passed class invariant, and inherits it to all subclasses
if it is public or protected.
|
void |
addClassInvariants(ImmutableSet<ClassInvariant> toAdd)
Registers the passed class invariants.
|
void |
addContract(Contract contract)
Registers the passed (atomic) contract, and inherits it to all overriding
methods.
|
void |
addContractNoInheritance(Contract contract)
Registers the passed (atomic) contract without inheriting it.
|
void |
addContracts(ImmutableSet<Contract> toAdd)
Registers the passed contracts.
|
void |
addInitiallyClause(InitiallyClause ini)
Registers the passed initially clause.
|
void |
addInitiallyClauses(ImmutableSet<InitiallyClause> toAdd)
Registers the passed initially clauses.
|
void |
addLoopContract(LoopContract contract)
Adds a new
LoopContract and a new FunctionalLoopContract
to the repository. |
void |
addLoopContract(LoopContract contract,
boolean addFunctionalContract)
Adds a new
LoopContract to the repository. |
void |
addLoopInvariant(LoopSpecification inv)
Registers the passed loop invariant, possibly overwriting an older
registration for the same loop.
|
void |
addMergeContract(MergeContract mc)
Registers a
MergeContract . |
void |
addRepresentsTermToWdChecksForModelFields(KeYJavaType kjt)
Represent terms belong to model fields, so the well-definedness check
considers both of them together.
|
void |
addSpecs(ImmutableSet<SpecificationElement> specs) |
void |
addWdStatement(StatementWellDefinedness swd)
Registers a well-definedness check for a jml statement.
|
FunctionalOperationContract |
combineOperationContracts(ImmutableSet<FunctionalOperationContract> toCombine)
Creates a combined contract out of the passed atomic contracts.
|
void |
copyLoopInvariant(LoopStatement from,
LoopStatement to)
Copies a loop invariant from a loop statement to another.
|
void |
createContractsFromInitiallyClauses()
Adds postconditions raising from initially clauses to all constructors.
|
ImmutableSet<Contract> |
getAllContracts()
Returns all registered contracts.
|
ImmutableSet<Proof> |
getAllProofs()
Returns all proofs registered with this specification repository.
|
ImmutableSet<WellDefinednessCheck> |
getAllWdChecks()
Returns all registered well-definedness checks.
|
ImmutableSet<BlockContract> |
getBlockContracts(StatementBlock block)
Returns all block contracts for the specified block.
|
ImmutableSet<BlockContract> |
getBlockContracts(StatementBlock block,
Modality modality)
Returns block contracts for according block statement
and modality.
|
ImmutableSet<ClassAxiom> |
getClassAxioms(KeYJavaType selfKjt)
Returns all class axioms visible in the passed class, including the
axioms induced by invariant declarations.
|
ImmutableSet<ClassInvariant> |
getClassInvariants(KeYJavaType kjt)
Returns all known class invariants for the passed type.
|
Contract |
getContractByName(java.lang.String name)
Returns the registered (atomic or combined) contract corresponding to the
passed name, or null.
|
ContractPO |
getContractPOForProof(Proof proof)
Returns the PO that the passed proof is about, or null.
|
ImmutableSet<Contract> |
getContracts(KeYJavaType kjt,
IObserverFunction target)
Returns all registered (atomic) contracts for the passed target.
|
ImmutableSet<IObserverFunction> |
getContractTargets(KeYJavaType kjt)
Returns all functions for which contracts are registered in the passed
type.
|
ImmutableSet<Contract> |
getInheritedContracts(Contract contract)
Returns a set encompassing the passed contract and all its versions
inherited to overriding methods.
|
ImmutableSet<Contract> |
getInheritedContracts(ImmutableSet<Contract> contractSet)
Returns a set encompassing the passed contracts and all its versions
inherited to overriding methods.
|
ImmutableSet<LoopContract> |
getLoopContracts(LoopStatement loop)
Returns all loop contracts for the specified loop.
|
ImmutableSet<LoopContract> |
getLoopContracts(LoopStatement loop,
Modality modality)
Returns loop contracts for according loop statement
and modality.
|
ImmutableSet<LoopContract> |
getLoopContracts(StatementBlock block)
Returns all loop contracts for the specified block.
|
ImmutableSet<LoopContract> |
getLoopContracts(StatementBlock block,
Modality modality) |
LoopSpecification |
getLoopSpec(LoopStatement loop)
Returns the registered loop invariant for the passed loop, or null.
|
ImmutableSet<MergeContract> |
getMergeContracts(MergePointStatement mps) |
ImmutableSet<FunctionalOperationContract> |
getOperationContracts(KeYJavaType kjt,
IProgramMethod pm)
Returns all registered (atomic) operation contracts for the passed
operation.
|
ImmutableSet<FunctionalOperationContract> |
getOperationContracts(KeYJavaType kjt,
IProgramMethod pm,
Modality modality)
Returns all registered (atomic) operation contracts for the passed
operation which refer to the passed modality.
|
ImmutableSet<Pair<KeYJavaType,IObserverFunction>> |
getOverridingTargets(KeYJavaType kjt,
IObserverFunction target) |
ContractPO |
getPO(Contract c)
Returns the PO that the passed contract is about, or null.
|
ContractPO |
getPOForProof(Proof proof) |
ProofOblInput |
getProofOblInput(Proof proof)
Returns the
ProofOblInput from which the given Proof was
created. |
ImmutableSet<Proof> |
getProofs(Contract atomicContract)
Returns all proofs registered for the passed atomic contract, or for
combined contracts including the passed atomic contract
|
ImmutableSet<Proof> |
getProofs(KeYJavaType kjt,
IObserverFunction target)
Returns all proofs registered for the passed target and its overriding
targets.
|
ImmutableSet<Proof> |
getProofs(ProofOblInput po)
Returns all proofs registered for the passed PO (or stronger POs).
|
IObserverFunction |
getTargetOfProof(Proof proof)
Returns the target that the passed proof is about, or null.
|
Pair<IObserverFunction,ImmutableSet<Taclet>> |
limitObs(IObserverFunction obs) |
void |
map(java.util.function.UnaryOperator<Term> op,
Services services)
Applies the specified operator to every contract in this repository.
|
void |
registerProof(ProofOblInput po,
Proof proof)
Registers the passed proof.
|
void |
removeBlockContract(BlockContract contract)
Removes a
BlockContract from the repository. |
void |
removeLoopContract(LoopContract contract)
Removes a
LoopContract from the repository. |
void |
removeMergeContracts(MergePointStatement mps)
Deletes the
MergeContract s for a given
MergePointStatement . |
void |
removeProof(Proof proof)
Unregisters the passed proof.
|
ImmutableSet<Contract> |
splitContract(Contract contract)
Splits the passed contract into its atomic components.
|
IObserverFunction |
unlimitObs(IObserverFunction obs) |
public static final java.lang.String CONTRACT_COMBINATION_MARKER
public static final java.lang.String LIMIT_SUFFIX
public SpecificationRepository(Services services)
public ImmutableSet<Pair<KeYJavaType,IObserverFunction>> getOverridingTargets(KeYJavaType kjt, IObserverFunction target)
public ImmutableSet<ClassInvariant> getClassInvariants(KeYJavaType kjt)
Returns all known class invariants for the passed type.
This method is used by Visual DbC and has to be public.
public void map(java.util.function.UnaryOperator<Term> op, Services services)
op
- an operator.services
- services.SpecificationElement.map(java.util.function.UnaryOperator, Services)
public ImmutableSet<Contract> getAllContracts()
public ImmutableSet<Contract> getContracts(KeYJavaType kjt, IObserverFunction target)
public ImmutableSet<FunctionalOperationContract> getOperationContracts(KeYJavaType kjt, IProgramMethod pm)
public ImmutableSet<FunctionalOperationContract> getOperationContracts(KeYJavaType kjt, IProgramMethod pm, Modality modality)
public Contract getContractByName(java.lang.String name)
public ImmutableSet<Contract> getInheritedContracts(Contract contract)
public ImmutableSet<Contract> getInheritedContracts(ImmutableSet<Contract> contractSet)
public ImmutableSet<IObserverFunction> getContractTargets(KeYJavaType kjt)
public void addContract(Contract contract)
public void addContractNoInheritance(Contract contract)
public void addContracts(ImmutableSet<Contract> toAdd)
public FunctionalOperationContract combineOperationContracts(ImmutableSet<FunctionalOperationContract> toCombine)
public ImmutableSet<Contract> splitContract(Contract contract)
public void addClassInvariant(ClassInvariant inv)
public void addClassInvariants(ImmutableSet<ClassInvariant> toAdd)
public void createContractsFromInitiallyClauses() throws SLTranslationException
SLTranslationException
- may be thrown during contract extractionpublic void addInitiallyClause(InitiallyClause ini)
createContractsFromInitiallyClauses
adds
them to the contracts of respective constructors (or adds a contract if
there is none yet).ini
- initially clausepublic void addInitiallyClauses(ImmutableSet<InitiallyClause> toAdd)
public ImmutableSet<ClassAxiom> getClassAxioms(KeYJavaType selfKjt)
public void addClassAxiom(ClassAxiom ax)
public void addClassAxioms(ImmutableSet<ClassAxiom> toAdd)
public ImmutableSet<Proof> getProofs(ProofOblInput po)
public ImmutableSet<Proof> getProofs(Contract atomicContract)
public ImmutableSet<Proof> getProofs(KeYJavaType kjt, IObserverFunction target)
public ImmutableSet<Proof> getAllProofs()
public ContractPO getContractPOForProof(Proof proof)
public ContractPO getPO(Contract c)
public ContractPO getPOForProof(Proof proof)
public ProofOblInput getProofOblInput(Proof proof)
ProofOblInput
from which the given Proof
was
created.proof
- The Proof
.ProofOblInput
of the given Proof
or
null
if not available.public IObserverFunction getTargetOfProof(Proof proof)
public void registerProof(ProofOblInput po, Proof proof)
public void removeProof(Proof proof)
public LoopSpecification getLoopSpec(LoopStatement loop)
public void copyLoopInvariant(LoopStatement from, LoopStatement to)
from
- the loop with the original contractloop
- the loop for which the contract is to be copiedpublic void addLoopInvariant(LoopSpecification inv)
public ImmutableSet<BlockContract> getBlockContracts(StatementBlock block)
block
- a block.public ImmutableSet<LoopContract> getLoopContracts(StatementBlock block)
block
- a block.public ImmutableSet<LoopContract> getLoopContracts(LoopStatement loop)
loop
- a loop.public ImmutableSet<MergeContract> getMergeContracts(MergePointStatement mps)
public ImmutableSet<BlockContract> getBlockContracts(StatementBlock block, Modality modality)
block
- the given block.modality
- the given modality.public ImmutableSet<LoopContract> getLoopContracts(StatementBlock block, Modality modality)
public ImmutableSet<LoopContract> getLoopContracts(LoopStatement loop, Modality modality)
loop
- the given loop.modality
- the given modality.public void addBlockContract(BlockContract contract)
BlockContract
and a new FunctionalBlockContract
to the repository.contract
- the BlockContract
to add.public void addBlockContract(BlockContract contract, boolean addFunctionalContract)
BlockContract
to the repository.contract
- the BlockContract
to add.addFunctionalContract
- whether or not to add a new FunctionalBlockContract
based on contract
.public void removeBlockContract(BlockContract contract)
Removes a BlockContract
from the repository.
The associated FunctionalBlockContract
is not removed.
contract
- the BlockContract
to remove.public void addLoopContract(LoopContract contract)
LoopContract
and a new FunctionalLoopContract
to the repository.contract
- the LoopContract
to add.public void addLoopContract(LoopContract contract, boolean addFunctionalContract)
LoopContract
to the repository.contract
- the LoopContract
to add.addFunctionalContract
- whether or not to add a new FunctionalLoopContract
based on contract
.public void removeLoopContract(LoopContract contract)
Removes a LoopContract
from the repository.
The associated FunctionalLoopContract
is not removed.
contract
- the LoopContract
to remove.public void addMergeContract(MergeContract mc)
MergeContract
.mc
- The MergeContract
to register.public void removeMergeContracts(MergePointStatement mps)
MergeContract
s for a given
MergePointStatement
.mps
- The MergePointStatement
to delete the registered
contracts for.public void addSpecs(ImmutableSet<SpecificationElement> specs)
public Pair<IObserverFunction,ImmutableSet<Taclet>> limitObs(IObserverFunction obs)
public IObserverFunction unlimitObs(IObserverFunction obs)
public void addRepresentsTermToWdChecksForModelFields(KeYJavaType kjt)
kjt
- The relevant KeYJavaTypepublic void addWdStatement(StatementWellDefinedness swd)
swd
- The well-definedness checkpublic ImmutableSet<WellDefinednessCheck> getAllWdChecks()
Copyright © 2003-2019 The KeY-Project.