public static class ProofStarter.UserProvidedInput extends java.lang.Object implements ProofOblInput
Constructor and Description |
---|
UserProvidedInput(Sequent seq,
ProofEnvironment env) |
UserProvidedInput(Sequent seq,
ProofEnvironment env,
java.lang.String proofName) |
UserProvidedInput(Term formula,
ProofEnvironment env) |
Modifier and Type | Method and Description |
---|---|
KeYJavaType |
getContainerType()
Returns the
KeYJavaType in which the proven element is contained in. |
ProofAggregate |
getPO()
Returns the proof obligation term as result of the proof obligation
input.
|
boolean |
implies(ProofOblInput po)
If true, then this PO implies the passed one.
|
java.lang.String |
name()
Returns the name of the proof obligation input.
|
void |
readProblem() |
public UserProvidedInput(Sequent seq, ProofEnvironment env)
public UserProvidedInput(Sequent seq, ProofEnvironment env, java.lang.String proofName)
public UserProvidedInput(Term formula, ProofEnvironment env)
public java.lang.String name()
ProofOblInput
name
in interface ProofOblInput
public void readProblem() throws ProofInputException
readProblem
in interface ProofOblInput
ProofInputException
public ProofAggregate getPO() throws ProofInputException
ProofOblInput
getPO
in interface ProofOblInput
ProofInputException
public boolean implies(ProofOblInput po)
ProofOblInput
implies
in interface ProofOblInput
public KeYJavaType getContainerType()
KeYJavaType
in which the proven element is contained in.getContainerType
in interface ProofOblInput
KeYJavaType
in which the proven element is contained in or null
if not available.Copyright © 2003-2019 The KeY-Project.