Package | Description |
---|---|
de.uka.ilkd.key.proof.init |
This package contains classes handling prover initialisation.
|
de.uka.ilkd.key.proof.io |
Classes related to loading and saving proof files.
|
de.uka.ilkd.key.proof.io.consistency |
Modifier and Type | Method and Description |
---|---|
RuleSource |
Includes.get(java.lang.String name)
returns the corresponding RuleSource to the filename
name |
RuleSource |
RuleCollection.getTacletBase()
returns the rule source containg all taclets for this profile
|
Modifier and Type | Method and Description |
---|---|
java.util.Collection<RuleSource> |
Includes.getRuleSets() |
Modifier and Type | Method and Description |
---|---|
void |
Includes.put(java.lang.String name,
RuleSource source)
adds a "normal" include.
|
void |
Includes.putLDT(java.lang.String name,
RuleSource source)
adds a LDT include.
|
Constructor and Description |
---|
RuleCollection(RuleSource standardTaclets,
ImmutableList<BuiltInRule> standardBuiltInRules) |
Modifier and Type | Class and Description |
---|---|
class |
FileRuleSource |
class |
GZipFileRuleSource
This file rule source derivative wraps its input stream into a
GZIPInputStream thus allowing decompressing gnu-zipped proof files. |
class |
UrlRuleSource |
Modifier and Type | Field and Description |
---|---|
protected RuleSource |
KeYFile.file
the RuleSource delivering the input stream for the file.
|
Modifier and Type | Method and Description |
---|---|
static RuleSource |
RuleSourceFactory.fromBuiltInRule(java.lang.String ruleFileName) |
static RuleSource |
RuleSourceFactory.fromDefaultLocation(java.lang.String ruleFileName) |
static RuleSource |
RuleSourceFactory.initRuleFile(java.io.File file) |
static RuleSource |
RuleSourceFactory.initRuleFile(java.io.File file,
boolean compressed)
Initialise this object from a file
|
static RuleSource |
RuleSourceFactory.initRuleFile(java.net.URL url) |
Constructor and Description |
---|
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(java.lang.String name,
RuleSource file,
ProgressMonitor monitor,
Profile profile,
FileRepo fileRepo)
creates a new representation for a given file by indicating a name
and a RuleSource representing the physical source of the .key file.
|
Modifier and Type | Method and Description |
---|---|
java.io.InputStream |
AbstractFileRepo.getInputStream(RuleSource ruleSource) |
java.io.InputStream |
MemoryFileRepo.getInputStream(RuleSource ruleSource) |
java.io.InputStream |
TrivialFileRepo.getInputStream(RuleSource ruleSource) |
java.io.InputStream |
FileRepo.getInputStream(RuleSource ruleSource)
Provides access to the InputStream of a RuleSource.
|
Copyright © 2003-2019 The KeY-Project.