Package | Description |
---|---|
de.uka.ilkd.key.control | |
de.uka.ilkd.key.core | |
de.uka.ilkd.key.gui |
This package contains classes forming the graphical user interface of KeY.
|
de.uka.ilkd.key.gui.lemmatagenerator | |
de.uka.ilkd.key.java |
This package contains classes that cover the Java programming language.
|
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.speclang |
This package contains the specification language frontends of KeY.
|
de.uka.ilkd.key.symbolic_execution.profile | |
de.uka.ilkd.key.taclettranslation.lemma | |
de.uka.ilkd.key.ui | |
de.uka.ilkd.key.util |
This package is a grab bag of miscellaneous useful code fragments.
|
Modifier and Type | Method and Description |
---|---|
Profile |
KeYEnvironment.getProfile() |
Modifier and Type | Method and Description |
---|---|
protected ProblemInitializer |
AbstractUserInterfaceControl.createProblemInitializer(Profile profile)
Creates a new
ProblemInitializer instance which is configured
for this UserInterfaceControl . |
static java.util.List<Name> |
TermLabelVisibilityManager.getSortedTermLabelNames(Profile profile)
Returns a sorted list of all term label names supported by the given
Profile . |
static KeYEnvironment<DefaultUserInterfaceControl> |
KeYEnvironment.load(Profile profile,
java.io.File location,
java.util.List<java.io.File> classPaths,
java.io.File bootClassPath,
java.util.List<java.io.File> includes,
boolean forceNewProfileOfNewProofs)
Loads the given location and returns all required references as
KeYEnvironment . |
AbstractProblemLoader |
AbstractUserInterfaceControl.load(Profile profile,
java.io.File file,
java.util.List<java.io.File> classPath,
java.io.File bootClassPath,
java.util.List<java.io.File> includes,
java.util.Properties poPropertiesToForce,
boolean forceNewProfileOfNewProofs)
Opens a java file in this
UserInterfaceControl and returns the instantiated AbstractProblemLoader
which can be used to instantiated proofs programmatically. |
AbstractProblemLoader |
UserInterfaceControl.load(Profile profile,
java.io.File file,
java.util.List<java.io.File> classPaths,
java.io.File bootClassPath,
java.util.List<java.io.File> includes,
java.util.Properties poPropertiesToForce,
boolean forceNewProfileOfNewProofs)
Opens a java file in this
UserInterfaceControl and returns the instantiated AbstractProblemLoader
which can be used to instantiated proofs programmatically. |
static KeYEnvironment<DefaultUserInterfaceControl> |
KeYEnvironment.load(Profile profile,
java.io.File location,
java.util.List<java.io.File> classPaths,
java.io.File bootClassPath,
java.util.List<java.io.File> includes,
java.util.Properties poPropertiesToForce,
RuleCompletionHandler ruleCompletionHandler,
boolean forceNewProfileOfNewProofs)
Loads the given location and returns all required references as
KeYEnvironment . |
Modifier and Type | Method and Description |
---|---|
Profile |
KeYMediator.getProfile()
return the chosen profile
|
Modifier and Type | Method and Description |
---|---|
AbstractProblemLoader |
WindowUserInterfaceControl.load(Profile profile,
java.io.File file,
java.util.List<java.io.File> classPath,
java.io.File bootClassPath,
java.util.List<java.io.File> includes,
java.util.Properties poPropertiesToForce,
boolean forceNewProfileOfNewProofs)
Opens a java file in this
UserInterfaceControl and returns the instantiated AbstractProblemLoader
which can be used to instantiated proofs programmatically. |
static KeYEnvironment<WindowUserInterfaceControl> |
WindowUserInterfaceControl.loadInMainWindow(Profile profile,
java.io.File location,
java.util.List<java.io.File> classPaths,
java.io.File bootClassPath,
java.util.List<java.io.File> includes,
boolean forceNewProfileOfNewProofs,
boolean makeMainWindowVisible)
Loads the given location and returns all required references as
KeYEnvironment
with KeY's MainWindow . |
Constructor and Description |
---|
LemmataHandler(LemmataAutoModeOptions options,
Profile profile) |
Modifier and Type | Method and Description |
---|---|
Profile |
Services.getProfile()
Returns the sued
Profile . |
Modifier and Type | Method and Description |
---|---|
Services |
Services.copy(Profile profile,
boolean shareCaches)
|
Constructor and Description |
---|
JavaReduxFileCollection(Profile profile)
Instantiates a new file collection.
|
Services(Profile profile)
creates a new Services object with a new TypeConverter and a new
JavaInfo object with no information stored at none of these.
|
Modifier and Type | Class and Description |
---|---|
class |
AbstractProfile |
class |
JavaProfile
This profile sets up KeY for verification of JavaCard programs.
|
Modifier and Type | Method and Description |
---|---|
Profile |
JavaProfileDefaultProfileResolver.getDefaultProfile()
Returns the default
Profile instance. |
protected Profile |
KeYUserProblemFile.getDefaultProfile()
Returns the default
Profile which was defined by a constructor. |
Profile |
DefaultProfileResolver.getDefaultProfile()
Returns the default
Profile instance. |
Profile |
JavaProfileWithPermissionsDefaultProfileResolver.getDefaultProfile()
Returns the default
Profile instance. |
static Profile |
AbstractProfile.getDefaultProfile()
Returns the default profile which is used if no profile is defined in custom problem files (loaded via
KeYUserProblemFile ). |
static Profile |
ProofInitServiceUtil.getDefaultProfile(java.lang.String profileName)
Returns the
Profile for the given name. |
Profile |
KeYUserProblemFile.getProfile()
Returns the
Profile to use. |
Profile |
InitConfig.getProfile() |
protected Profile |
KeYUserProblemFile.readProfileFromFile()
Tries to read the
Profile from the file to load. |
Modifier and Type | Method and Description |
---|---|
static void |
AbstractProfile.setDefaultProfile(Profile defaultProfile)
Sets the default profile which is used if no profile is defined in custom problem files (loaded via
KeYUserProblemFile ). |
Constructor and Description |
---|
KeYUserProblemFile(java.lang.String name,
java.io.File file,
FileRepo fileRepo,
ProgressMonitor monitor,
Profile profile,
boolean compressed)
Instantiates a new user problem file.
|
KeYUserProblemFile(java.lang.String name,
java.io.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.
|
KeYUserProblemFile(java.lang.String name,
java.io.File file,
ProgressMonitor monitor,
Profile profile,
boolean compressed)
Instantiates a new user problem file.
|
ProblemInitializer(Profile profile) |
Modifier and Type | Field and Description |
---|---|
protected Profile |
AbstractEnvInput.profile |
Modifier and Type | Method and Description |
---|---|
Profile |
AbstractEnvInput.getProfile() |
Profile |
LDTInput.getProfile() |
Profile |
KeYFile.getProfile() |
Profile |
EnvInput.getProfile()
Returns the
Profile to use. |
Modifier and Type | Method and Description |
---|---|
java.lang.String |
OutputStreamProofSaver.writeProfile(Profile profile) |
Constructor and Description |
---|
AbstractEnvInput(java.lang.String name,
java.lang.String javaPath,
java.util.List<java.io.File> classPath,
java.io.File bootClassPath,
Profile profile,
java.util.List<java.io.File> includes) |
AbstractProblemLoader(java.io.File file,
java.util.List<java.io.File> classPath,
java.io.File bootClassPath,
java.util.List<java.io.File> includes,
Profile profileOfNewProofs,
boolean forceNewProfileOfNewProofs,
ProblemLoaderControl control,
boolean askUiToSelectAProofObligationIfNotDefinedByLoadedFile,
java.util.Properties poPropertiesToForce)
Constructor.
|
KeYFile(java.lang.String name,
java.io.File file,
FileRepo fileRepo,
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,
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.
|
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.
|
LDTInput(KeYFile[] keyFiles,
LDTInput.LDTInputListener listener,
Profile profile)
creates a representation of the LDT files to be used as input
to the KeY prover.
|
ProblemLoader(java.io.File file,
java.util.List<java.io.File> classPath,
java.io.File bootClassPath,
java.util.List<java.io.File> includes,
Profile profileOfNewProofs,
boolean forceNewProfileOfNewProofs,
KeYMediator mediator,
boolean askUiToSelectAProofObligationIfNotDefinedByLoadedFile,
java.util.Properties poPropertiesToForce,
ProverTaskListener ptl) |
SingleThreadProblemLoader(java.io.File file,
java.util.List<java.io.File> classPath,
java.io.File bootClassPath,
java.util.List<java.io.File> includes,
Profile profileOfNewProofs,
boolean forceNewProfileOfNewProofs,
ProblemLoaderControl control,
boolean askUiToSelectAProofObligationIfNotDefinedByLoadedFile,
java.util.Properties poPropertiesToForce)
Constructor.
|
Constructor and Description |
---|
SLEnvInput(java.lang.String javaPath,
java.util.List<java.io.File> classPath,
java.io.File bootClassPath,
Profile profile,
java.util.List<java.io.File> includes) |
SLEnvInput(java.lang.String javaPath,
Profile profile) |
Modifier and Type | Class and Description |
---|---|
class |
SimplifyTermProfile
An extended
JavaProfile used in side proofs to simplify a Term . |
class |
SymbolicExecutionJavaProfile
An extended
JavaProfile used by the symbolic execution API. |
Modifier and Type | Method and Description |
---|---|
Profile |
SymbolicExecutionJavaProfileDefaultProfileResolver.getDefaultProfile()
Returns the default
Profile instance. |
Modifier and Type | Method and Description |
---|---|
static boolean |
SymbolicExecutionJavaProfile.isTruthValueEvaluationEnabled(Profile profile)
Checks if predicate evaluation is enabled in the given
Profile . |
Modifier and Type | Field and Description |
---|---|
protected Profile |
TacletLoader.profile |
Constructor and Description |
---|
EmptyEnvInput(Profile profile) |
KeYsTacletsLoader(ProgressMonitor monitor,
ProblemInitializer.ProblemInitializerListener listener,
Profile profile) |
TacletFromFileLoader(ProgressMonitor pm,
ProblemInitializer.ProblemInitializerListener listener,
ProblemInitializer problemInitializer,
Profile profile,
java.io.File fileForTaclets,
java.util.Collection<java.io.File> filesForAxioms) |
TacletLoader(ProgressMonitor monitor,
ProblemInitializer.ProblemInitializerListener listener,
Profile profile) |
Modifier and Type | Method and Description |
---|---|
ProblemInitializer |
ConsoleUserInterfaceControl.createProblemInitializer(Profile profile) |
Modifier and Type | Method and Description |
---|---|
static OneStepSimplifier |
MiscTools.findOneStepSimplifier(Profile profile)
Returns the
OneStepSimplifier used in the given Profile . |
ProofAggregate |
HelperClassForTests.parse(java.io.File file,
Profile profile) |
ProofAggregate |
HelperClassForTests.parseThrowException(java.io.File file,
Profile profile) |
Copyright © 2003-2019 The KeY-Project.