Operating VeriFun

VeriFun's main system window is separated into 2 sub-windows, viz.

the Program Window, which displays the actual program, and
the Proof Window, which alternatively displays proof trees, the navigation for symbolic evaluations or the interface of the interpreter.

Data structures, procedures and lemmas of the actual program may be organized in program folders. Using the drag&drop-feature, program items may be rearranged in the Program Window and moved to or out of program folders. These arrangements are irrelevant for verification and for the system’s language parser.

The Program Menu provides commands

to edit the actual program,
to inspect items of the actual program in the Program Viewer,
to guide the generation of termination hypotheses for procedures,
to open a proof tree of a lemma in the Proof Window,
to disprove a lemma, and
to initiate the verification of a lemma.

The Proof Menu provides commands

to copy a proof tree,
to prune a proof tree,
to display symbolic evaluations in the Evaluation Viewer,
to inspect the nodes of a proof tree in the Proof Viewer,
to disprove a proof node sequent,
to generalize a proof node sequent, and
to develop a proof tree.

A proof tree is developed by

selecting a leaf in the proof tree,
choosing a proof rule from the Proof Rules submenu of the Proof Menu, and
providing further input for the chosen proof rule.

When applying a proof rule to a leaf of a proof tree, the system expands the proof tree at that leaf by computing the descendant nodes for the leaf according to the chosen proof rule. The descendant nodes created by some of the proof rules are computed by a first-order theorem prover, called the Symbolic Evaluator. This tool uses the hypotheses and induction hypotheses of a proof node sequent, the definitions of the data structures and procedures as well as the verified lemmas of the actual program for computing a symbolic evaluation. The Symbolic Evaluator is a completely automated tool on which the user has no influence, except to stop or to cancel the computation of a symbolic evaluation.

VeriFun provides several automated features:

By calling the Verify command from the Program Menu, the system develops a proof tree by successively applying proof rules to the leaves of the tree. The automatic computation of proof trees is implemented by the so-called next-rule heuristic. This heuristic determines which of the proof rules is useful to be applied to a leaf of a proof tree. In case of a parameterized proof rule, this heuristic also computes the required input. For example, if the system selects Induction, it also “guesses” the induction axiom and the variables to induct upon. Having developed a proof tree with the selected rule, the next-rule-heuristic is applied to all leaves created by this rule application and so on, until the proof tree becomes closed or the heuristic fails to choose a rule for some leaf. In such a case, the user has to support the system by some proof tree edit or the formulation of a lemma needed to complete the proof. In the former case, the user selects a node in the Proof Window for pruning some unwanted branch of the proof tree, if necessary, and then choses a proof rule to be applied at a user selected leaf. After the proof tree is developed by the chosen proof rule, the system takes over control again, the user may step in another time etc., until eventually verification succeeds. VeriFun provides no control commands for the creation of proofs thus leaving the proof rules as the only means to guide the development of proof trees.
Upon the definition of a procedure, the system’s automated termination analysis is activated by computing termination hypotheses which are sufficient for the procedure's termination and are proved like lemmas. If the system fails to generate termination hypotheses, a termination function has to be provided by the user, and then the system computes termination hypotheses for the procedure based on the submitted termination function. Afterwards induction axioms are computed from the terminating procedures' recursion structure to be on stock for future use.
Also the work of the Symbolic Evaluator is supported by heuristics. For example, the lemma-filter heuristic excludes verified lemmas from the computation of a symbolic evaluation if they do not seem to contribute to a proof, the execute/unfold heuristic decides whether it is useful to "open up" a procedure call, etc. Equality reasoning is implemented by matching modulo AC and conditional term rewriting, where the orientation of equations is computed by appropriate heuristics.

Files

The File Menu provides the usual commands to save and reload intermediate work and to open the Import Window for working with proof libraries. VeriFun supports three file formats:

VeriFun data files (vf-files) store the whole system state and are the primary input/output medium of the system. When opening a vf-file, the system state is just reloaded.
OMDoc files (omd-files) store all user interactions (definitions and proof rule applications) which had been performed for creating the actual program. When opening an omd-file, the actual program is restored by recomputing all proofs. omd-files can be used for reading case studies which had been computed with former system versions, for exchanging data with other reasoning systems or for post processing.
Functional Program files (fp-files) store all user definitions (but no proofs) as plain text (Unicode UTF8). When opening an fp-file, the actual program is restored by reading only the stored definitions. fp-files can also be opened with text editors capable of processing Unicode.
For all file types, backup files with extension vf.bak, omd.bak and fp.bak may exist which hold the former file contents. When trying to write to an existing file name.ex, the existing file is renamed to name.ex.bak before (thus overwriting an already existing file name.ex.bak).
Only vf- and vf.bak-files can be used for importing program items into the actual program.

_______________________________

Last update 2016-03-02