| java.lang.Object
 de.uka.ilkd.key.proof.init.KeYFile
All known Subclasses: de.uka.ilkd.key.proof.init.KeYUserProblemFile, de.uka.ilkd.key.proof.init.KeYFileForTests,
| KeYFile | | public class KeYFile implements EnvInput(Code) | | represents an input from a .key file producing an environment.
|
| Constructor Summary | |
| public | KeYFile(String name, File file)
creates a new representation for a given file by indicating a name
and a file representing the physical source of the .key file. | | public | KeYFile(String name, File file, ProgressMonitor monitor)
creates a new representation for a given file by indicating a name
and a file representing the physical source of the .key file. | | public | KeYFile(String name, RuleSource file, ProgressMonitor monitor)
creates a new representation for a given file by indicating a name
and a RuleSource representing the physical source of the .key file. |
| file | | protected RuleSource file(Code) | | the RuleSource delivering the input stream for the file.
|
| initConfig | | protected InitConfig initConfig(Code) | | the initial configuration to be used (and modified) while reading.
|
| method2jmlspecs | | protected LinkedHashMap method2jmlspecs(Code) | | maps methods to their jml specifications.
|
| problemParser | | protected KeYParser problemParser(Code) | | |
| KeYFile | | public KeYFile(String name, File file)(Code) | | 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(String name, File file, ProgressMonitor monitor)(Code) | | creates a new representation for a given file by indicating a name
and a file representing the physical source of the .key file.
Parameters:
monitor - the progress monitor to notify on the state of reading |
| KeYFile | | public KeYFile(String name, RuleSource file, ProgressMonitor monitor)(Code) | | creates a new representation for a given file by indicating a name
and a RuleSource representing the physical source of the .key file.
Parameters:
monitor - the progress monitor to notify on the state of reading |
| close | | public void close()(Code) | | |
| getInitConfig | | public InitConfig getInitConfig()(Code) | | returns the initial configuration that is used to read and
that may be modified by reading.
|
| getNumberOfChars | | public int getNumberOfChars()(Code) | | returns the number of chars in the .key file.
|
| hashCode | | public int hashCode()(Code) | | |
| name | | public String name()(Code) | | returns the name of the .key file
|
| read | | public void read(ModStrategy mod) throws ProofInputException(Code) | | reads the whole .key file and modifies the initial configuration
assigned to this object according to the given modification strategy.
Throws an exception if no initial configuration has been set yet.
|
| readFuncAndPred | | public void readFuncAndPred(ModStrategy mod) throws ProofInputException(Code) | | reads the functions and predicates declared in the .key file only,
modifying the function namespaces of the respective taclet options.
|
| readRulesAndProblem | | public void readRulesAndProblem(ModStrategy mod) throws ProofInputException(Code) | | reads the rules and problems declared in the .key file only,
modifying the set of rules
of the initial configuration if allowed in the given
modification strategy.
|
| readSorts | | public void readSorts(ModStrategy mod) throws ProofInputException(Code) | | reads the sorts declaration of the .key file only,
modifying the sort namespace
of the initial configuration if allowed in the given
modification strategy.
|
| setupSchemaNamespace | | protected NamespaceSet setupSchemaNamespace(NamespaceSet normal)(Code) | | when reading in rules modal schema operators and schemavariables are
added to the namespace, but shall not occur in the normal function
namespaces. Therefore we take the given namespaces and use copies of
the normal function and variables namespace
TODO: extend the normal namespace by a generic sort and schema function
namespace and get rid of the schemaConfig...
Parameters:
normal - the Namespace containing the concrete symbols namespace for reading in rules etc. |
|
|