public final class SpecificationRepository
extends java.lang.Object
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.
|
private void |
createContractsFromInitiallyClause(InitiallyClause inv,
KeYJavaType kjt)
Adds initially clause as post-condition to contracts of constructors.
|
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.
|
private ImmutableSet<MethodWellDefinedness> |
getAllWdMethodChecks()
Returns all registered well-definedness checks for method contracts.
|
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.
|
private IObserverFunction |
getCanonicalFormForKJT(IObserverFunction obs,
KeYJavaType kjt) |
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.
|
private KeYJavaType |
getEnclosingKJT(KeYJavaType kjt)
Returns the kjt for the outer class, if the passed kjt is a member class,
and null otherwise.
|
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.
|
private static Taclet |
getLimitedToUnlimitedTaclet(IObserverFunction limited,
IObserverFunction unlimited,
TermServices services) |
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.
|
private static Modality |
getMatchModality(Modality modality) |
ImmutableSet<MergeContract> |
getMergeContracts(MergePointStatement mps) |
private ImmutableSet<ClassAxiom> |
getModelMethodAxioms() |
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.
|
private ImmutableSet<Pair<KeYJavaType,IObserverFunction>> |
getOverridingMethods(KeYJavaType kjt,
IProgramMethod pm) |
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).
|
private RepresentsAxiom |
getRepresentsAxiom(KeYJavaType kjt,
ClassAxiom ax) |
IObserverFunction |
getTargetOfProof(Proof proof)
Returns the target that the passed proof is about, or null.
|
private static java.lang.String |
getUniqueNameForObserver(IObserverFunction obs) |
private static Taclet |
getUnlimitedToLimitedTaclet(IObserverFunction limited,
IObserverFunction unlimited,
TermServices services) |
private ImmutableSet<ClassAxiom> |
getVisibleAxiomsOfOtherClasses(KeYJavaType visibleTo) |
private ImmutableSet<WellDefinednessCheck> |
getWdChecks(KeYJavaType kjt)
Returns all registered (atomic) well-definedness checks for the passed
kjt.
|
private ImmutableSet<WellDefinednessCheck> |
getWdChecks(KeYJavaType kjt,
IObserverFunction target)
Returns all registered (atomic) well-definedness checks for the passed
target and kjt.
|
private ImmutableSet<ClassWellDefinedness> |
getWdClassChecks(KeYJavaType kjt)
Returns all registered (atomic) well-definedness class checks for the
passed kjt.
|
private ImmutableSet<MethodWellDefinedness> |
getWdMethodChecks(KeYJavaType kjt)
Returns all registered (atomic) well-definedness method checks for the
passed kjt.
|
private ImmutableSet<MethodWellDefinedness> |
getWdMethodChecks(KeYJavaType kjt,
IObserverFunction target)
Returns all registered (atomic) well-definedness method checks for the
passed target and kjt.
|
Pair<IObserverFunction,ImmutableSet<Taclet>> |
limitObs(IObserverFunction obs) |
private Contract |
prepareContract(Contract contract) |
private void |
registerContract(Contract contract) |
private void |
registerContract(Contract contract,
ImmutableSet<Pair<KeYJavaType,IObserverFunction>> targets) |
private void |
registerContract(Contract contract,
Pair<KeYJavaType,IObserverFunction> targetPair) |
void |
registerProof(ProofOblInput po,
Proof proof)
Registers the passed proof.
|
private void |
registerWdCheck(WellDefinednessCheck check)
Registers a well-definedness check.
|
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.
|
private static ImmutableSet<Contract> |
removeWdChecks(ImmutableSet<Contract> contracts)
Remove well-definedness checks from a given set of contracts
|
ImmutableSet<Contract> |
splitContract(Contract contract)
Splits the passed contract into its atomic components.
|
IObserverFunction |
unlimitObs(IObserverFunction obs) |
private void |
unregisterContract(Contract contract)
Removes the contract from the repository, but keeps its target.
|
private void |
unregisterWdCheck(WellDefinednessCheck check)
Unregisters a well-definedness check.
|
public static final java.lang.String CONTRACT_COMBINATION_MARKER
private final ContractFactory cf
private final java.util.Map<Pair<KeYJavaType,IObserverFunction>,ImmutableSet<Contract>> contracts
private final java.util.Map<Pair<KeYJavaType,IProgramMethod>,ImmutableSet<FunctionalOperationContract>> operationContracts
private final java.util.Map<Pair<KeYJavaType,IObserverFunction>,ImmutableSet<WellDefinednessCheck>> wdChecks
private final java.util.Map<java.lang.String,Contract> contractsByName
private final java.util.Map<KeYJavaType,ImmutableSet<IObserverFunction>> contractTargets
private final java.util.Map<KeYJavaType,ImmutableSet<ClassInvariant>> invs
private final java.util.Map<KeYJavaType,ImmutableSet<ClassAxiom>> axioms
private final java.util.Map<KeYJavaType,ImmutableSet<InitiallyClause>> initiallyClauses
private final java.util.Map<ProofOblInput,ImmutableSet<Proof>> proofs
private final java.util.Map<Pair<LoopStatement,java.lang.Integer>,LoopSpecification> loopInvs
private final java.util.Map<Pair<StatementBlock,java.lang.Integer>,ImmutableSet<BlockContract>> blockContracts
private final java.util.Map<Pair<StatementBlock,java.lang.Integer>,ImmutableSet<LoopContract>> loopContracts
private final java.util.Map<Pair<LoopStatement,java.lang.Integer>,ImmutableSet<LoopContract>> loopContractsOnLoops
private java.util.Map<MergePointStatement,ImmutableSet<MergeContract>> mergeContracts
private final java.util.Map<IObserverFunction,IObserverFunction> unlimitedToLimited
private final java.util.Map<IObserverFunction,IObserverFunction> limitedToUnlimited
private final java.util.Map<IObserverFunction,ImmutableSet<Taclet>> unlimitedToLimitTaclets
private final java.util.Map<KeYJavaType,ImmutableSet<ClassAxiom>> allClassAxiomsCache
This Map
is used to store the result of
getClassAxioms(KeYJavaType)
to avoid that
RepresentsAxiom
and QueryAxiom
are instantiated multiple
times.
It is strongly required that always the same instances are returned
because Object.equals(Object)
and Object.hashCode()
is
not implemented in instances of ClassAxiom
and such the default
reference check is done which off cause always fails in case of different
references.
private final Services services
private final TermBuilder tb
private final java.util.Map<java.lang.String,java.lang.Integer> contractCounters
public SpecificationRepository(Services services)
private static java.lang.String getUniqueNameForObserver(IObserverFunction obs)
private static Taclet getLimitedToUnlimitedTaclet(IObserverFunction limited, IObserverFunction unlimited, TermServices services)
private static Taclet getUnlimitedToLimitedTaclet(IObserverFunction limited, IObserverFunction unlimited, TermServices services)
private IObserverFunction getCanonicalFormForKJT(IObserverFunction obs, KeYJavaType kjt)
private ImmutableSet<Pair<KeYJavaType,IObserverFunction>> getOverridingMethods(KeYJavaType kjt, IProgramMethod pm)
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.
private KeYJavaType getEnclosingKJT(KeYJavaType kjt)
private ImmutableSet<ClassAxiom> getVisibleAxiomsOfOtherClasses(KeYJavaType visibleTo)
private RepresentsAxiom getRepresentsAxiom(KeYJavaType kjt, ClassAxiom ax)
private void registerContract(Contract contract)
private void registerContract(Contract contract, ImmutableSet<Pair<KeYJavaType,IObserverFunction>> targets)
private void registerContract(Contract contract, Pair<KeYJavaType,IObserverFunction> targetPair)
private void unregisterContract(Contract contract)
private void createContractsFromInitiallyClause(InitiallyClause inv, KeYJavaType kjt) throws SLTranslationException
inv
- initially clausekjt
- constructors of this type are added a post-conditionSLTranslationException
- during contract construction from history constraintprivate static ImmutableSet<Contract> removeWdChecks(ImmutableSet<Contract> contracts)
contracts
- A set of contractsprivate void registerWdCheck(WellDefinednessCheck check)
registerContract(Contract, Pair)
).check
- The well-definedness check to be registeredprivate void unregisterWdCheck(WellDefinednessCheck check)
check
- The well-definedness check to be unregisteredprivate ImmutableSet<WellDefinednessCheck> getWdChecks(KeYJavaType kjt)
private ImmutableSet<WellDefinednessCheck> getWdChecks(KeYJavaType kjt, IObserverFunction target)
private ImmutableSet<MethodWellDefinedness> getAllWdMethodChecks()
private ImmutableSet<MethodWellDefinedness> getWdMethodChecks(KeYJavaType kjt)
private ImmutableSet<MethodWellDefinedness> getWdMethodChecks(KeYJavaType kjt, IObserverFunction target)
private ImmutableSet<ClassWellDefinedness> getWdClassChecks(KeYJavaType kjt)
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)
private ImmutableSet<ClassAxiom> getModelMethodAxioms()
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()