de.uka.ilkd.key.proof.io

Class KeYFile

java.lang.Object

de.uka.ilkd.key.proof.io.KeYFile

All Implemented Interfaces:

EnvInput

Direct Known Subclasses:

KeYUserProblemFile

public class KeYFile
extends java.lang.Object
implements EnvInput

Represents an input from a .key file producing an environment.

Field Summary

Fields

Modifier and Type	Field and Description
private java.lang.String	bootClassPath
private java.lang.String	chooseContract
private ImmutableList<java.lang.String>	classPaths
protected RuleSource	file the RuleSource delivering the input stream for the file.
private Includes	includes
protected InitConfig	initConfig
private java.io.InputStream	input
private java.lang.String	javaPath
private boolean	javaPathAlreadyParsed
protected ProgressMonitor	monitor the graphical entity to notify on the state of reading.
private java.lang.String	name
private Profile	profile
private java.lang.String	proofObligation

Constructor Summary

Constructors

Constructor and Description
KeYFile(java.lang.String name, java.io.File file, ProgressMonitor monitor, Profile profile) creates a new representation for a given file by indicating a name and a file representing the physical source of the .key file.
KeYFile(java.lang.String name, java.io.File file, ProgressMonitor monitor, Profile profile, boolean compressed) Creates a new representation for a given file by indicating a name and a file representing the physical source of the .key file.
KeYFile(java.lang.String name, RuleSource file, ProgressMonitor monitor, Profile profile) creates a new representation for a given file by indicating a name and a RuleSource representing the physical source of the .key file.

Method Summary

Modifier and Type	Method and Description
java.lang.String	chooseContract()
void	close()
private KeYParserF	createDeclParser(java.io.InputStream is)
boolean	equals(java.lang.Object o)
java.io.File	getInitialFile() Returns the initial File which is loaded if available.
protected java.io.InputStream	getNewStream()
int	getNumberOfChars() Returns the total numbers of chars that can be read in this input.
protected ProofSettings	getPreferences()
Profile	getProfile() Returns the Profile to use.
java.lang.String	getProofObligation()
int	hashCode()
java.lang.String	name() Returns the name of this input.
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.
java.io.File	readBootClassPath() gets the boot classpath element, null if none set.
java.util.List<java.io.File>	readClassPath() gets the classpath elements to be considered here.
void	readFuncAndPred() reads the functions and predicates declared in the .key file only, modifying the function namespaces of the respective taclet options.
Includes	readIncludes() Reads the include section and returns an Includes object.
java.lang.String	readJavaPath() Reads the Java path.
ProofSettings	readPreferences()
void	readRulesAndProblem() reads the rules and problems declared in the .key file only, modifying the set of rules of the initial configuration
void	readSorts() reads the sorts declaration of the .key file only, modifying the sort namespace of the initial configuration
void	setInitConfig(InitConfig conf) Sets the initial configuration the read environment input should be added to.
java.lang.String	toString()

Methods inherited from class java.lang.Object

clone, finalize, getClass, notify, notifyAll, wait, wait, wait

Field Detail

name

private final java.lang.String name

file

protected final RuleSource file

the RuleSource delivering the input stream for the file.

monitor

protected final ProgressMonitor monitor

the graphical entity to notify on the state of reading.

javaPath

private java.lang.String javaPath

javaPathAlreadyParsed

private boolean javaPathAlreadyParsed

input

private java.io.InputStream input

initConfig

protected InitConfig initConfig

chooseContract

private java.lang.String chooseContract

proofObligation

private java.lang.String proofObligation

profile

private final Profile profile

classPaths

private ImmutableList<java.lang.String> classPaths

bootClassPath

private java.lang.String bootClassPath

includes

private Includes includes

Constructor Detail

KeYFile

public KeYFile(java.lang.String name,
               RuleSource file,
               ProgressMonitor monitor,
               Profile profile)

creates a new representation for a given file by indicating a name and a RuleSource representing the physical source of the .key file.

KeYFile

public KeYFile(java.lang.String name,
               java.io.File file,
               ProgressMonitor monitor,
               Profile profile)

creates a new representation for a given file by indicating a name and a file representing the physical source of the .key file.

KeYFile

public KeYFile(java.lang.String name,
               java.io.File file,
               ProgressMonitor monitor,
               Profile profile,
               boolean compressed)

Creates a new representation for a given file by indicating a name and a file representing the physical source of the .key file.

Parameters:

name - the name of the resource

file - the file to find it

monitor - a possibly null reference to a monitor for the loading progress

profile - the KeY profile under which the file is to be load

compressed - true iff the file has compressed content

Method Detail

createDeclParser

private KeYParserF createDeclParser(java.io.InputStream is)
                             throws java.io.IOException

Throws:

java.io.IOException

getNewStream

protected java.io.InputStream getNewStream()
                                    throws java.io.FileNotFoundException

Throws:

java.io.FileNotFoundException

getPreferences

protected ProofSettings getPreferences()
                                throws ProofInputException

Throws:

ProofInputException

readPreferences

public ProofSettings readPreferences()
                              throws ProofInputException

Throws:

ProofInputException

name

public java.lang.String name()

Description copied from interface: EnvInput

Returns the name of this input.

Specified by:

name in interface EnvInput

getNumberOfChars

public int getNumberOfChars()

Description copied from interface: EnvInput

Returns the total numbers of chars that can be read in this input.

Specified by:

getNumberOfChars in interface EnvInput

setInitConfig

public void setInitConfig(InitConfig conf)

Description copied from interface: EnvInput

Sets the initial configuration the read environment input should be added to. Must be called before calling any of the read* methods.

Specified by:

setInitConfig in interface EnvInput

readIncludes

public Includes readIncludes()
                      throws ProofInputException

Description copied from interface: EnvInput

Reads the include section and returns an Includes object.

Specified by:

readIncludes in interface EnvInput

Throws:

ProofInputException

readBootClassPath

public java.io.File readBootClassPath()
                               throws java.io.IOException

Description copied from interface: EnvInput

gets the boot classpath element, null if none set.

Specified by:

readBootClassPath in interface EnvInput

Throws:

java.io.IOException

readClassPath

public java.util.List<java.io.File> readClassPath()

Description copied from interface: EnvInput

gets the classpath elements to be considered here.

Specified by:

readClassPath in interface EnvInput

readJavaPath

public java.lang.String readJavaPath()
                              throws ProofInputException

Description copied from interface: EnvInput

Reads the Java path.

Specified by:

readJavaPath in interface EnvInput

Throws:

ProofInputException

read

public ImmutableSet<PositionedString> read()
                                    throws ProofInputException

Description copied from interface: EnvInput

Reads the input using the given modification strategy, i.e., parts of the input do not modify the initial configuration while others do.

Specified by:

read in interface EnvInput

Returns:

The found warnings or an empty ImmutableSet if no warnings occurred.

Throws:

ProofInputException

readSorts

public void readSorts()
               throws ProofInputException

reads the sorts declaration of the .key file only, modifying the sort namespace of the initial configuration

Throws:

ProofInputException

readFuncAndPred

public void readFuncAndPred()
                     throws ProofInputException

reads the functions and predicates declared in the .key file only, modifying the function namespaces of the respective taclet options.

Throws:

ProofInputException

readRulesAndProblem

public void readRulesAndProblem()
                         throws ProofInputException

reads the rules and problems declared in the .key file only, modifying the set of rules of the initial configuration

Throws:

ProofInputException

close

public void close()

chooseContract

public java.lang.String chooseContract()

getProofObligation

public java.lang.String getProofObligation()

toString

public java.lang.String toString()

Overrides:

toString in class java.lang.Object

equals

public boolean equals(java.lang.Object o)

Overrides:

equals in class java.lang.Object

hashCode

public int hashCode()

Overrides:

hashCode in class java.lang.Object

getProfile

public Profile getProfile()

Description copied from interface: EnvInput

Returns the Profile to use.

Specified by:

getProfile in interface EnvInput

Returns:

The Profile to use.

getInitialFile

public java.io.File getInitialFile()

Description copied from interface: EnvInput

Returns the initial File which is loaded if available.

Specified by:

getInitialFile in interface EnvInput

Returns:

The initial File which is loaded or null otherwise.