Commands

Generated on: Tue Sep 19 17:10:07 CEST 2017by gendoc.groovy.

Covering the proof script commands of KeY.

assume

Synopsis: assume <TERM>

The assume command is an unsound taclet rule and takes one argument:

The command adds the formula passed as argument to the antecedent a formula #2 to which the command is applied

Arguments:

• #2 : TERM (R)null

auto

Synopsis: auto [all=<BOOLEAN>] [steps=<INT>]

Arguments:

• all : BOOLEAN null
• steps : INT null

cut

Synopsis: cut <TERM>

Arguments:

• #2 : TERM (R)null

exit

Synopsis: exit

Arguments:

focus

Synopsis: focus <SEQUENT>

Arguments:

• #2 : SEQUENT (R)null

instantiate

Synopsis: instantiate formula=<TERM> var=<STRING> occ=<INT> with=<TERM>

Arguments:

• formula : TERM (R)null
• var : STRING (R)null
• occ : INT (R)null
• with : TERM (R)null

javascript

Synopsis: javascript <STRING>

Arguments:

• #2 : STRING (R)null

leave

Synopsis: leave

Arguments:

let

Synopsis: let

Arguments:

macro

Synopsis: macro <STRING>

Arguments:

• #2 : STRING (R)null

rule

Synopsis: rule <STRING> [on=<TERM>] [formula=<TERM>] [occ=<INT>] [inst_=<TERM>]

Arguments:

• #2 : STRING (R)null
• on : TERM null
• formula : TERM null
• occ : INT null
• inst_ : TERM null

schemaVar

Synopsis: schemaVar <STRING> <STRING>

Arguments:

• #2 : STRING (R)null
• #3 : STRING (R)null

script

Synopsis: script <STRING>

Arguments:

• #2 : STRING (R)null

select

Synopsis: select formula=<TERM>

Arguments:

• formula : TERM (R)null

set

Synopsis: set [oss=<BOOLEAN>] [=<STRING>]

Arguments:

• oss : BOOLEAN null
• `` : STRING null

skip

Synopsis: skip

Arguments:

smt

Synopsis: smt solver=<STRING>

Arguments:

• solver : STRING (R)null

tryclose

Synopsis: tryclose steps=<INTEGER> <STRING>

Arguments:

• steps : INTEGER (R)null
• #2 : STRING (R)null