public final class ProofCorrectnessMgt
extends java.lang.Object
Constructor and Description |
---|
ProofCorrectnessMgt(Proof p) |
Modifier and Type | Method and Description |
---|---|
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() |
public ProofCorrectnessMgt(Proof p)
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
Copyright © 2003-2019 The KeY-Project.