Debugging and refactoring tactics graphically
(JFR paper resources)
Authors : Yuhui Lin, Gudmund Grov and Rob Arthan
We present the use of a graph-based proof strategy language,
called PSGraph, in the re-implementation and refactoring of
several existing tactics. We show that the PSGraph implementation can
improve understandability and maintainability properties of the tactic.
This webpage presents the resources used in the paper. All the PSGraph
examples are available <here>, and the original resource of the case studies are
Tautology: this tactic is part of ProofPower, the ML file is <here>.
the FEF project: the project website can be found <here>, and the ML file which includes the definitions of the tactics is <here>.
Conversions: the paper for this case study is <here>, and the ML file which includes the definition of the tactic is <here>.
Installation
The example runs with Proof Power, to configure it, follow those steps :
assume that the quantomatics repo and the PSGraph are cloned in the
same folder, for example (TODO: can we provide a script to generate a ProofPower database, like the FEF example)
$SOME_PATH/tinker
we can check the readme file to make sure the path is correct, e.g. the readme for quantomatoics repo will be
$SOME_PATH/tinker/quantomatic/README
similarly, the readme for the psgtarph repo will be
$SOME_PATH/tinker/psgraph/Readme.md?
(SOME TEXT to show how to build or run the script to compile the database)
When the database is compiled, using the following command to run ProofPower containing the case studies in the heap:
xpp -d psgraph
The ML files of the examples of the paper are under
$SOME_PATH/tinker/psgraph/src/core/examples/JFR16
namely, simple.ML, taut.ML, fef_tac.ML and conv_tac.ML. We will give more details for each example in the following sections. There are two commands to invoke tinker,
PPIntf.apply_ps psgraph
and
PPIntf.apply_ps_i psgraph
The
first command is to apply a PSGraph to the current goal automatically,
while the second one is to apply a PSGraph interactively with the
Tinker GUI.
Also, there is another command to setup a goal in ProofPower and apply
a PSGraph interactively, which is
PPIntf.set_psg_goal goal psgraph
In the
interactive mode, the tinker GUI will be involved for evaluating and
debugging the current proof. More details for the GUI can be found
in Tinker's user guide.
A simple example
This is a simple example to show the use of Goaltype to guide the subgoal to the right subsequent tactic.
This
example re-engineers a tautology tactic into PSGraph. It contains the
details of how we a generalised version, followed by optimisations
through a set of refactorings. Tinker's debugging capabilities are
utilised to find and correct mistakes in the encoding.
The FEF Project was an early application of ProofPower to
verify the security properties of a multi-level secure database system
called SWORD. We will look at some very domain-specific tactics taken
from the FEF
proof scripts as an experiment in porting an existing application proof
to PSGraph with a view to making future maintenance easier by
presenting the proof at a higher level.
The
final case study addresses a more abstract example, which is an
implementation of a proof procedure that automates proofs that a
function formed from a given set of
atomic morphisms by composition and pairing is a morphism in a concrete category.
This case study includes more complex features of low-level term rewriting through
conversions with recursion.