Skip to content

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
Back to top