Commit 0ca93625 authored by Alexander Weigl's avatar Alexander Weigl

site regenerated

parent 6bc9bfa1
# Commands
Generated on: Mon Sep 11 17:22:08 CEST 2017by `gendoc.groovy`.
Covering the proof script commands of [KeY](http://key-project.org).
## 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*)
## auto
> Synopsis: `auto [all=<BOOLEAN>] [steps=<INT>]`
The AutoCommand invokes the automatic strategy "Auto"
**Arguments:**
* `all` : *BOOLEAN*
* `steps` : *INT*
## cut
> Synopsis: `cut <TERM>`
* The command object CutCommand has as scriptcommand name "cut"
* As parameters:
* a formula with the id "#2"
**Arguments:**
* `#2` : *TERM* (*R*)
## exit
> Synopsis: `exit`
**Arguments:**
## focus
> Synopsis: `focus <SEQUENT>`
**Arguments:**
* `#2` : *SEQUENT* (*R*)
## instantiate
> Synopsis: `instantiate [formula=<TERM>] [var=<STRING>] [occ=<INT>] [<STRING>] [with=<TERM>]`
instantiate var=a occ=2 with="a_8" hide
<p>
instantiate formula="\forall int a; phi(a)" with="a_8"
**Arguments:**
* `formula` : *TERM*
* `var` : *STRING*
* `occ` : *INT*
* `#2` : *STRING*
* `with` : *TERM*
## javascript
> Synopsis: `javascript <STRING>`
**Arguments:**
* `#2` : *STRING* (*R*)
## leave
> Synopsis: `leave`
**Arguments:**
## let
> Synopsis: `let`
**Arguments:**
## macro
> Synopsis: `macro <STRING>`
**Arguments:**
* `#2` : *STRING* (*R*)
## rule
> Synopsis: `rule <STRING> [on=<TERM>] [formula=<TERM>] [occ=<INT>]`
* Command that applies a calculus rule
* All parameters are passed as strings and converted by the command.
* The parameters are:
* <ol>
* <li>#2 = <String>rule name</String></li>
* <li>on= key.core.logic.Term on which the rule should be applied to as String (find part of the rule) </li>
* <li>formula= toplevel formula in which term appears in</li>
* <li>occ = occurrence number</li>
* <li>inst_= instantiation</li>
* </ol>
**Arguments:**
* `#2` : *STRING* (*R*)
* `on` : *TERM*
* `formula` : *TERM*
* `occ` : *INT*
## schemaVar
> Synopsis: `schemaVar <STRING> <STRING>`
**Arguments:**
* `#2` : *STRING* (*R*)
* `#3` : *STRING* (*R*)
## script
> Synopsis: `script <STRING>`
**Arguments:**
* `#2` : *STRING* (*R*)
## select
> Synopsis: `select formula=<TERM>`
**Arguments:**
* `formula` : *TERM* (*R*)
## set
> Synopsis: `set [oss=<BOOLEAN>]`
**Arguments:**
* `oss` : *BOOLEAN*
## skip
> Synopsis: `skip`
**Arguments:**
## smt
> Synopsis: `smt solver=<STRING>`
**Arguments:**
* `solver` : *STRING* (*R*)
## tryclose
> Synopsis: `tryclose [steps=<INTEGER>] [<STRING>]`
**Arguments:**
* `steps` : *INTEGER*
* `#2` : *STRING*
# Macros
Generated on: Mon Sep 11 14:19:11 CEST 2017 by `gendoc.groovy`.
Generated on: ${new Date()} by `gendoc.groovy`.
Covering the macros of [KeY](http://key-project.org).
## Full Information Flow Auto Pilot (`infflow-autopilot`)
## Full Auto Pilot (`autopilot`)
Information Flow
Auto Pilot
<html><ol><li>Search exhaustively for applicable position, then<li>Start auxiliary computation<li>Finish symbolic execution<li>Try to close as many goals as possible<li>Apply macro recursively<li>Finish auxiliary computation<li>Use information flow contracts<li>Try to close as many goals as possible</ol>
<html><ol><li>Finish symbolic execution<li>Separate proof obligations<li>Expand invariant definitions<li>Try to close all proof obligations</ol>
## Close provable goals below (`tryclose`)
## Auto pilot (preparation only) (`autopilot-prep`)
null
Auto Pilot
Closes closable goals, leave rest untouched (see settings AutoPrune). Applies only to goals beneath the selected node.
<html><ol><li>Finish symbolic execution<li>Separate proof obligations<li>Expand invariant definitions</ol>
## Update Simplification Only (`simp-upd`)
## Full Information Flow Auto Pilot (`infflow-autopilot`)
Simplification
Information Flow
Applies only update simplification rules
<html><ol><li>Search exhaustively for applicable position, then<li>Start auxiliary computation<li>Finish symbolic execution<li>Try to close as many goals as possible<li>Apply macro recursively<li>Finish auxiliary computation<li>Use information flow contracts<li>Try to close as many goals as possible</ol>
## Full Auto Pilot (`autopilot`)
## Propositional expansion (w/o splits) (`nosplit-prop`)
Auto Pilot
Propositional
<html><ol><li>Finish symbolic execution<li>Separate proof obligations<li>Expand invariant definitions<li>Try to close all proof obligations</ol>
Apply rules to decompose propositional toplevel formulas; does not split the goal.
## Finish symbolic execution (`symbex`)
## One Single Proof Step (`onestep`)
Auto Pilot
Simplification
Continue automatic strategy application until no more modality is on the sequent.
One single proof step is applied
## Propositional expansion (w/ splits) (`split-prop`)
## Heap Simplification (`simp-heap`)
Propositional
Simplification
Apply rules to decompose propositional toplevel formulas; splits the goal if necessary
This macro performs simplification of Heap and LocSet terms.
It applies simplification rules (including the "unoptimized" select rules), One Step Simplification, alpha, and delta rules.
## Heap Simplification (`simp-heap`)
## Integer Simplification (`simp-int`)
Simplification
This macro performs simplification of Heap and LocSet terms.
It applies simplification rules (including the "unoptimized" select rules), One Step Simplification, alpha, and delta rules.
This macro performs simplification of integers and terms with integers.
It applies only non-splitting simplification rules.
## Auto pilot (preparation only) (`autopilot-prep`)
## Update Simplification Only (`simp-upd`)
Auto Pilot
Simplification
<html><ol><li>Finish symbolic execution<li>Separate proof obligations<li>Expand invariant definitions</ol>
Applies only update simplification rules
## Propositional expansion (w/o splits) (`nosplit-prop`)
## Propositional expansion (w/ splits) (`split-prop`)
Propositional
Apply rules to decompose propositional toplevel formulas; does not split the goal.
Apply rules to decompose propositional toplevel formulas; splits the goal if necessary
## One Single Proof Step (`onestep`)
## Finish symbolic execution (`symbex`)
Simplification
Auto Pilot
One single proof step is applied
Continue automatic strategy application until no more modality is on the sequent.
## Integer Simplification (`simp-int`)
## Close provable goals below (`tryclose`)
Simplification
null
This macro performs simplification of integers and terms with integers.
It applies only non-splitting simplification rules.
Closes closable goals, leave rest untouched (see settings AutoPrune). Applies only to goals beneath the selected node.
This diff is collapsed.
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment