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