Package | Description |
---|---|
de.uka.ilkd.key.api |
This package gives an high-level entry point to the KeY world.
|
de.uka.ilkd.key.macros.scripts |
Proof script commands are a simple proof automation facility.
|
de.uka.ilkd.key.macros.scripts.meta |
Modifier and Type | Method and Description |
---|---|
ProofScriptCommand<?> |
ProofScriptCommandApi.getScriptCommands(java.lang.String name)
Searches for the proof script command in the registered commands by its name.
|
Modifier and Type | Method and Description |
---|---|
java.util.Collection<ProofScriptCommand> |
ProofScriptCommandApi.getScriptCommands()
Returns a collection of all registered proof script commands.
|
Modifier and Type | Method and Description |
---|---|
<T> ProofScriptCommandCall<T> |
ScriptApi.instantiateCommand(ProofScriptCommand<T> command,
java.util.Map<java.lang.String,java.lang.String> arguments)
Evaluate the arguments passed to a command
|
Constructor and Description |
---|
ProofScriptCommandCall(ProofScriptCommand<T> command,
T arguments) |
Modifier and Type | Class and Description |
---|---|
class |
AbstractCommand<T>
Inheritance:
|
class |
ActivateCommand
Command for re-activating the first open (not necessarily enabled)
Goal after a "leave" command. |
class |
AssertCommand
Halts the script if some condition is not met.
|
class |
AssumeCommand
The assume command takes one argument: * a formula to which the command is
applied
|
class |
AutoCommand
The AutoCommand invokes the automatic strategy "Auto".
|
class |
AxiomCommand
The axiom command takes one argument: a formula to which the command is
applied.
|
class |
CutCommand
The command object CutCommand has as scriptcommand name "cut"
As parameters:
a formula with the id "#2"
|
class |
EchoCommand
A simple "echo" command for giving feedback to human observers during lengthy
executions.
|
class |
ExitCommand |
class |
FocusOnSelectionAndHideCommand
Hide all formulas that are not selected
Parameter:
* The sequent with those formulas that should not be hidden
Created by sarah on 1/12/17.
|
class |
InstantiateCommand
instantiate var=a occ=2 with="a_8" hide
|
class |
JavascriptCommand |
class |
LeaveCommand |
class |
LetCommand |
class |
MacroCommand |
class |
NoArgumentCommand |
class |
RewriteCommand
This class provides the command
rewrite . |
class |
RuleCommand
Command that applies a calculus rule All parameters are passed as strings and
converted by the command.
|
class |
SaveInstCommand
Special "Let" usually to be applied immediately after a manual rule
application.
|
class |
SaveNewNameCommand
Special "Let" usually to be applied immediately after a manual rule
application.
|
class |
SchemaVarCommand |
class |
ScriptCommand |
class |
SelectCommand |
class |
SetCommand |
class |
SetEchoCommand
A simple "echo" command for giving feedback to human observers during lengthy
executions.
|
class |
SetFailOnClosedCommand
Sets the behavior if an already closed proof is encountered: Either throw an
exception (default behavior, sensible for specially tailored scripts for
which a prematurely closed proof is unexpected) or peacefully terminate (if
the script addresses different problems of different complexity in a
try-and-error manner, etc.).
|
class |
SkipCommand |
class |
SMTCommand |
class |
TryCloseCommand
The script command tryclose" has two optional arguments:
steps: INTEGER number of steps to use
#2: STRING the number of the branch which should be closed
If #2 is not given or not a number, the TryClose macro is applied to all open
goals.
|
Modifier and Type | Method and Description |
---|---|
ProofScriptCommand<T> |
ProofScriptArgument.getCommand() |
Modifier and Type | Method and Description |
---|---|
static java.lang.String |
DescriptionFacade.getDocumentation(ProofScriptCommand<?> cmd)
Looks up the documentation for the given command in the properties file.
|
static java.util.List<ProofScriptArgument> |
ArgumentsLifter.inferScriptArguments(java.lang.Class<?> clazz,
ProofScriptCommand<?> command) |
<T> T |
ValueInjector.inject(ProofScriptCommand<?> command,
T obj,
java.util.Map<java.lang.String,java.lang.String> arguments)
Injects the converted version of the given
arguments in the given obj . |
static <T> T |
ValueInjector.injection(ProofScriptCommand<?> command,
T obj,
java.util.Map<java.lang.String,java.lang.String> arguments)
Injects the given
arguments in the obj . |
ProofScriptArgument<T> |
ProofScriptArgument.setCommand(ProofScriptCommand<T> command) |
Copyright © 2003-2019 The KeY-Project.