Skip to content

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.