# Language Constructs

This description is an adapted version of the README for script commands in KeY by Mattias Ulbrich.

Proof scripts are textual representations of rule applications,
settings changes and macro invocations.
## Proof Commands

Proof commands start with an identifier followed by optional
arguments:

command argName="argument" "argument without name" ;

Every command is terminated with a semicolon. There are named
arguments in the form argName="argument" and unnamed argument without
name. Single '...'and double quotes "..." can both be used.

Single-line comments are start with //.
### KeY Rules/Taclets

All KeY rules can be used as proof command.
The following command structure is used to apply single KeY rules onto the sequent of a selected goal node.
If no argument is following the proof command the taclet corresponding to this command has to match at most once on the
sequent.
If more terms or formulas to which a proof command is applicable exist, arguments have to be
given that indicate the where to apply the rule to.

A rule command has the following syntax:

RULENAME (on="TERM")? (formula="TOP_LEVEL_FORMULA")? (occ="OCCURENCE_IN_SEQUENT")? (inst_="TERM")? (maxSteps=INT)

with:
- TERM: specific sub-term
- TOP_LEVEL_FORMULA: specific top level formula
- OCCURENCE_IN_SEQUENT: Number of occurence in the sequent
- maxSteps: the number of steps KEY should at most use until it terminateds teh proof search

If a rule has schema variables which must be instantiated manually,
such instantiations can be provided as arguments. A schema variable
named sv can be instantiated by setting the argument sv="..." or by
setting inst_sv="..." (the latter works also for conflict cases like
inst_occ="...").
#### Examples

- andRight;

Applicable iff there is only one matching spot on the sequent
- eqSymm formula="a=b";

This command changes the sequent "a=b ==> c=d" to "b=a ==> c=d"
Using only "eqSymm;" alone would have been ambiguous.
- eqSymm formula="a=b->c=d" occ=2;

This command changes sequent "a=b->c=d ==>" to "a=b->d=c ==>".
The occurrence number is needed since there are two possible applications on the formula
- eqSymm formula="a=b->c=d" on="c=d";

This command changes the sequent "a=b->c=d ==>" to "a=b->d=c ==>".
It is simialr to the example above, but here the option to specify a
subterm instead of an occurrence number is used.
- cut cutFormula="x > y";

This command is almost the same as 'cut "x>y"'

### Macro-Commands

In the KeY system macro commands are proof strategies tailored to specific proof tasks.
The available macro commands can be found using the command help.
Using them in a script is similar to using rule commands:

MACRONAME (PARAMETERS)?

Often used macro commands are:
- symbex : performs symbolic execution
- auto: invokes the automatic strategy of key
- heap_simp: performs heap simplification
- autopilot: full autopilot
- autopilot_prep: preparation only autopilot
- split_prop: propositional expansion w/ splits
- nosplit_prop: propositional expansion w/o splits
- simp_upd: update simplification
- simp_heap: heap simplification

Example:
auto;
## Selectors

As nited before proof commands are implemented as single goal statements.
Some proof commands split a proof into more than one goal.
To allow to apply proof commands in proof state with more than one proof goal, the language allows for
a selector statement *cases*. Such a *cases*-statement has the following structure:

cases {

case MATCHER:

STATEMENTS

[default:

STATEMENTS]?

}
## Control Flow Statements

The script language allows different statements for control-flow.
Control-Flow statements define blocks, therefor it is neccessary to use curly braces after a control-flow statement.
- foreach {STATEMENTS}
- theOnly {STATEMENTS}
- repeat {STATEMENTS}