public final class ProofCorrectnessMgt
extends java.lang.Object
Modifier and Type | Class and Description |
---|---|
private class |
ProofCorrectnessMgt.DefaultMgtProofListener |
private class |
ProofCorrectnessMgt.DefaultMgtProofTreeListener |
Modifier and Type | Field and Description |
---|---|
private java.util.Set<RuleApp> |
cachedRuleApps |
private Proof |
proof |
private ProofCorrectnessMgt.DefaultMgtProofListener |
proofListener |
private ProofStatus |
proofStatus |
private ProofCorrectnessMgt.DefaultMgtProofTreeListener |
proofTreeListener |
private SpecificationRepository |
specRepos |
Constructor and Description |
---|
ProofCorrectnessMgt(Proof p) |
Modifier and Type | Method and Description |
---|---|
private boolean |
allHaveMeasuredBy(ImmutableList<Contract> contracts) |
boolean |
contractApplicableFor(KeYJavaType kjt,
IObserverFunction target)
Deprecated.
|
protected void |
finalize() |
RuleJustification |
getJustification(RuleApp r) |
ProofStatus |
getStatus() |
ImmutableSet<Contract> |
getUsedContracts() |
boolean |
isContractApplicable(Contract contract)
Tells whether a contract for the passed target may be applied
in the passed goal without creating circular dependencies.
|
void |
removeProofListener() |
void |
ruleApplied(RuleApp r) |
void |
ruleUnApplied(RuleApp r) |
void |
updateProofStatus() |
private final Proof proof
private final SpecificationRepository specRepos
private final ProofCorrectnessMgt.DefaultMgtProofListener proofListener
private final ProofCorrectnessMgt.DefaultMgtProofTreeListener proofTreeListener
private java.util.Set<RuleApp> cachedRuleApps
private ProofStatus proofStatus
public ProofCorrectnessMgt(Proof p)
private boolean allHaveMeasuredBy(ImmutableList<Contract> contracts)
public RuleJustification getJustification(RuleApp r)
public boolean isContractApplicable(Contract contract)
@Deprecated public boolean contractApplicableFor(KeYJavaType kjt, IObserverFunction target)
public void updateProofStatus()
public void ruleApplied(RuleApp r)
public void ruleUnApplied(RuleApp r)
public ImmutableSet<Contract> getUsedContracts()
public void removeProofListener()
public ProofStatus getStatus()
protected void finalize() throws java.lang.Throwable
finalize
in class java.lang.Object
java.lang.Throwable