de.uka.ilkd.key.util

Class ProofStarter.UserProvidedInput

java.lang.Object

de.uka.ilkd.key.util.ProofStarter.UserProvidedInput

All Implemented Interfaces:

ProofOblInput

Enclosing class:

ProofStarter

public static class ProofStarter.UserProvidedInput
extends java.lang.Object
implements ProofOblInput

Proof obligation for a given formula or sequent

Field Summary

Fields

Modifier and Type	Field and Description
private static java.lang.String	EMPTY_PROOF_HEADER
private ProofEnvironment	env
private java.lang.String	proofName
private Sequent	seq

Constructor Summary

Constructors

Constructor and Description
UserProvidedInput(Sequent seq, ProofEnvironment env)
UserProvidedInput(Sequent seq, ProofEnvironment env, java.lang.String proofName)
UserProvidedInput(Term formula, ProofEnvironment env)

Method Summary

Modifier and Type	Method and Description
private Proof	createProof(java.lang.String proofName)
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()

Methods inherited from class java.lang.Object

clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait

Field Detail

EMPTY_PROOF_HEADER

private static final java.lang.String EMPTY_PROOF_HEADER

See Also:

Constant Field Values

env

private final ProofEnvironment env

seq

private final Sequent seq

proofName

private final java.lang.String proofName

Constructor Detail

UserProvidedInput

public UserProvidedInput(Sequent seq,
                         ProofEnvironment env)

UserProvidedInput

public UserProvidedInput(Sequent seq,
                         ProofEnvironment env,
                         java.lang.String proofName)

UserProvidedInput

public UserProvidedInput(Term formula,
                         ProofEnvironment env)

Method Detail

name

public java.lang.String name()

Description copied from interface: ProofOblInput

Returns the name of the proof obligation input.

Specified by:

name in interface ProofOblInput

readProblem

public void readProblem()
                 throws ProofInputException

Specified by:

readProblem in interface ProofOblInput

Throws:

ProofInputException

createProof

private Proof createProof(java.lang.String proofName)

getPO

public ProofAggregate getPO()
                     throws ProofInputException

Description copied from interface: ProofOblInput

Returns the proof obligation term as result of the proof obligation input. If there is still no input available because nothing has been read yet null is returned.

Specified by:

getPO in interface ProofOblInput

Throws:

ProofInputException

implies

public boolean implies(ProofOblInput po)

Description copied from interface: ProofOblInput

If true, then this PO implies the passed one.

Specified by:

implies in interface ProofOblInput

getContainerType

public KeYJavaType getContainerType()

Returns the KeYJavaType in which the proven element is contained in.

Specified by:

getContainerType in interface ProofOblInput

Returns:

The KeYJavaType in which the proven element is contained in or null if not available.