Macros

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

Covering the macros of KeY.

Full Auto Pilot (autopilot)

Auto Pilot

1. Finish symbolic execution
2. Separate proof obligations
3. Expand invariant definitions
4. Try to close all proof obligations

Auto pilot (preparation only) (autopilot-prep)

Auto Pilot

1. Finish symbolic execution
2. Separate proof obligations
3. Expand invariant definitions

Full Information Flow Auto Pilot (infflow-autopilot)

Information Flow

1. Search exhaustively for applicable position, then
2. Start auxiliary computation
3. Finish symbolic execution
4. Try to close as many goals as possible
5. Apply macro recursively
6. Finish auxiliary computation
7. Use information flow contracts
8. Try to close as many goals as possible

Propositional expansion (w/o splits) (nosplit-prop)

Propositional

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

One Single Proof Step (onestep)

Simplification

One single proof step is applied

Heap Simplification (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.

Update Simplification Only (simp-upd)

Simplification

Applies only update simplification rules

Propositional expansion (w/ splits) (split-prop)

Propositional

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

Finish symbolic execution (symbex)

Auto Pilot

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

Close provable goals below (tryclose)

null

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