- Macros
- Full Auto Pilot (autopilot)
- Auto pilot (preparation only) (autopilot-prep)
- Full Information Flow Auto Pilot (infflow-autopilot)
- Propositional expansion (w/o splits) (nosplit-prop)
- One Single Proof Step (onestep)
- Heap Simplification (simp-heap)
- Update Simplification Only (simp-upd)
- Propositional expansion (w/ splits) (split-prop)
- Finish symbolic execution (symbex)
- Close provable goals below (tryclose)

Generated on: ${new Date()} by `gendoc.groovy`

.

Covering the macros of KeY.

`autopilot`

)¶Auto Pilot

- Finish symbolic execution
- Separate proof obligations
- Expand invariant definitions
- Try to close all proof obligations

`autopilot-prep`

)¶Auto Pilot

- Finish symbolic execution
- Separate proof obligations
- Expand invariant definitions

`infflow-autopilot`

)¶Information Flow

- Search exhaustively for applicable position, then
- Start auxiliary computation
- Finish symbolic execution
- Try to close as many goals as possible
- Apply macro recursively
- Finish auxiliary computation
- Use information flow contracts
- Try to close as many goals as possible

`nosplit-prop`

)¶Propositional

Apply rules to decompose propositional toplevel formulas; does not split the goal.

`onestep`

)¶Simplification

One single proof step is applied

`simp-heap`

)¶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.

`simp-upd`

)¶Simplification

Applies only update simplification rules

`split-prop`

)¶Propositional

Apply rules to decompose propositional toplevel formulas; splits the goal if necessary

`symbex`

)¶Auto Pilot

Continue automatic strategy application until no more modality is on the sequent.

`tryclose`

)¶null

Closes closable goals, leave rest untouched (see settings AutoPrune). Applies only to goals beneath the selected node.