public final class SpecificationRepository extends Object
Constructor and Description |
---|
SpecificationRepository(Services services) |
Modifier and Type | Method and Description |
---|---|
void |
addBlockContract(BlockContract contract) |
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 |
addLoopInvariant(LoopInvariant inv)
Registers the passed loop invariant, possibly overwriting an older
registration for the same loop.
|
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) |
ImmutableSet<BlockContract> |
getBlockContracts(StatementBlock block,
Modality 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(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) |
LoopInvariant |
getLoopInvariant(LoopStatement loop)
Returns the registered loop invariant for the passed loop, or null.
|
private static Modality |
getMatchModality(Modality modality) |
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 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 |
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.
|
private static final String CONTRACT_COMBINATION_MARKER
private final ContractFactory cf
private final Map<Pair<KeYJavaType,IObserverFunction>,ImmutableSet<Contract>> contracts
private final Map<Pair<KeYJavaType,IProgramMethod>,ImmutableSet<FunctionalOperationContract>> operationContracts
private final Map<Pair<KeYJavaType,IObserverFunction>,ImmutableSet<WellDefinednessCheck>> wdChecks
private final Map<KeYJavaType,ImmutableSet<IObserverFunction>> contractTargets
private final Map<KeYJavaType,ImmutableSet<ClassInvariant>> invs
private final Map<KeYJavaType,ImmutableSet<ClassAxiom>> axioms
private final Map<KeYJavaType,ImmutableSet<InitiallyClause>> initiallyClauses
private final Map<ProofOblInput,ImmutableSet<Proof>> proofs
private final Map<Pair<LoopStatement,Integer>,LoopInvariant> loopInvs
private final Map<Pair<StatementBlock,Integer>,ImmutableSet<BlockContract>> blockContracts
private final Map<IObserverFunction,IObserverFunction> unlimitedToLimited
private final Map<IObserverFunction,IObserverFunction> limitedToUnlimited
private final Map<IObserverFunction,ImmutableSet<Taclet>> unlimitedToLimitTaclets
private final 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
public SpecificationRepository(Services services)
private static 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(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 LoopInvariant getLoopInvariant(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(LoopInvariant inv)
public ImmutableSet<BlockContract> getBlockContracts(StatementBlock block)
public ImmutableSet<BlockContract> getBlockContracts(StatementBlock block, Modality modality)
public void addBlockContract(BlockContract contract)
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()