public final class KeYUserProblemFile extends KeYFile implements ProofOblInput
Modifier and Type | Field and Description |
---|---|
private KeYParserF |
lastParser |
private String |
problemHeader |
private Term |
problemTerm |
file, initConfig, monitor
Constructor and Description |
---|
KeYUserProblemFile(String name,
File file,
ProgressMonitor monitor,
Profile profile)
Creates a new representation of a KeYUserFile with the given name,
a rule source representing the physical source of the input, and
a graphical representation to call back in order to report the progress
while reading.
|
Modifier and Type | Method and Description |
---|---|
boolean |
equals(Object o) |
KeYJavaType |
getContainerType()
Returns the
KeYJavaType in which the proven element is contained in. |
protected Profile |
getDefaultProfile()
Returns the default
Profile which was defined by a constructor. |
ProofAggregate |
getPO()
Returns the proof obligation term as result of the proof obligation
input.
|
Profile |
getProfile()
Returns the
Profile to use. |
int |
hashCode() |
boolean |
hasProofScript() |
boolean |
implies(ProofOblInput po)
If true, then this PO implies the passed one.
|
ImmutableSet<PositionedString> |
read()
Reads the input using the given modification strategy, i.e.,
parts of the input do not modify the initial configuration while
others do.
|
void |
readProblem() |
protected Profile |
readProfileFromFile()
Tries to read the
Profile from the file to load. |
void |
readProof(IProofFileParser prl)
Reads a saved proof of a .key file.
|
Triple<String,Integer,Integer> |
readProofScript() |
chooseContract, close, getInitialFile, getNewStream, getNumberOfChars, getPreferences, getProofObligation, name, readBootClassPath, readClassPath, readFuncAndPred, readIncludes, readJavaPath, readPreferences, readRulesAndProblem, readSorts, setInitConfig, toString
clone, finalize, getClass, notify, notifyAll, wait, wait, wait
name
private Term problemTerm
private String problemHeader
private KeYParserF lastParser
public KeYUserProblemFile(String name, File file, ProgressMonitor monitor, Profile profile)
public ImmutableSet<PositionedString> read() throws ProofInputException
EnvInput
read
in interface EnvInput
read
in class KeYFile
ImmutableSet
if no warnings occurred.ProofInputException
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 boolean hasProofScript()
public Triple<String,Integer,Integer> readProofScript() throws ProofInputException
ProofInputException
public void readProof(IProofFileParser prl) throws ProofInputException
ProofInputException
public Profile getProfile()
Profile
to use.getProfile
in interface EnvInput
getProfile
in class KeYFile
Profile
to use.protected Profile readProfileFromFile() throws Exception
Profile
from the file to load.protected Profile getDefaultProfile()
Profile
which was defined by a constructor.Profile
.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.