public class ProofInfo extends Object
Modifier and Type | Field and Description |
---|---|
private Proof |
proof |
private Services |
services |
Modifier and Type | Method and Description |
---|---|
Term |
getAssignable() |
String |
getCode() |
Contract |
getContract() |
JavaBlock |
getJavaBlock(Term t) |
IProgramMethod |
getMUT() |
Term |
getPO() |
Term |
getPostCondition() |
Term |
getPostCondition2() |
Term |
getPreConTerm() |
void |
getProgramVariables(Term t,
Set<Term> vars) |
KeYJavaType |
getReturnType() |
KeYJavaType |
getTypeOfClassUnderTest() |
String |
getUpdate(Term t) |
private boolean |
isFalseConstant(Operator o) |
private boolean |
isRelevantConstant(Term c) |
private boolean |
isTrueConstant(Operator o) |
private String |
processUpdate(Term update) |
public ProofInfo(Proof proof)
public IProgramMethod getMUT()
public KeYJavaType getTypeOfClassUnderTest()
public KeYJavaType getReturnType()
public Contract getContract()
public Term getPostCondition2()
public Term getPostCondition()
public Term getPreConTerm()
public Term getAssignable()
public String getCode()
private boolean isRelevantConstant(Term c)
private boolean isTrueConstant(Operator o)
private boolean isFalseConstant(Operator o)
public Term getPO()