Making interactive persistent using proof scripts

Mattias Ulbrich ulbrich@kit.edu, 2015

Experimental feature: Proof scripts are currently only visible in the GUI if KeY is launched with the --experimental option. Concrete syntax is subject to change.

Every KeY user knows the pain of manually redoing an interactive proof over and over again even though only a tiny bit of the program or specification have changed. NOW you can use proof scripts which will alleviate your worries with repeating proofs.

Proof scripts are textual representations of rule applications, settings changes and macro invocations. They are notated in linear order. The target of a script command is usually the first open goal in the proof tree, i.e., the first reached when traversing the proof tree (not necessarily the first in the Goal pane in the GUI).

Syntax of proof scripts

Proof commands start with an identifier followed by optional arguments:

command argName="argument" "argument without name" ;

Every command is terminated with a semicolon. There are named arguments in the form argName="argument" and unnamed argument without name. Single '...' and double quotes "..." can both be used. If "argument" is an identifier itself, the quotes can optionally be dropped, like in

rule andRight ;

The character # begins a comment which extends to the end of the line. Currently, there are no multi-line comments in proof scripts. Proof scripts are case sensitive.

How can scripts be loaded

  1. In the GUI: Open a proof obligation. Currently proof scripts work only reliably if applied to the root of a fresh proof obligation (no rule applications, prune steps). The open the context menu (sequent or proof tree), choose "Strategy macros" and then "Run proof script ...". In the file dialog that appears, choose the script file to load. The script is automatically applied. You can follow the process in a logging window.

  2. From within key input files: At the very end of key files INSTEAD of a \proof object, you can now attach a proof script directly in double quotes following the keyword \proofScript. An very simple example reads:

\predicates {a; b;}
\problem { a & b -> a }

\proofScript "
   rule 'impRight';
   rule 'andLeft';
   rule 'close';"

Since the script is no enclosed in "...", only single quotes '...' can be used in the script. You can also load a script from an external file by writing

\proofScript "script 'some_filename.script';"

Commands in scripts

This list of available script commands is subject to change and to extension. If you write your own script commands (s. below), please add an explanation to this list here. The list is sorted alphabetically.

Apply the automatic KeY strategy on the current goal. Optinally you can specify the number of steps to run.

auto steps=30000; # run at most 30000 steps automatically.

Performs a cut and thus splits the sequent into two goals. The unnamed argument is the formula to cut with

cut "value1 = value2";

Terminate the script prematurely at that point. Used mainly for debug purposes.

exit;

Write your on proof script commands

to be done. Contact Mattias, if you are interested.