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
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
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