On this directory is the Fortran verification condition generator that
is described in detail in the article "A Verification Condition
Generator for FORTRAN" in the book "The Correctness Problem in
Computer Science", ed. R. S. Boyer and J S. Moore, Academic Press,
1981.

This program is written in Common Lisp and is intended to be run on
top of nqthm, the Common Lisp version of our theorem-prover with
partial recursive functions and quantifiers.

There are three test files on this directory:

    isqrt.lisp   An integer square root function.
    mjrty.lisp   A linear time majority voter.
    fsrch.lisp   A fast string searching algorithm.

To test the system on fsrch.lisp, for example, one uses the following
procedure:


%nqthm   ;  invoke nqthm
>(load "fortran-vcg") ; the compiled version of the file fortran-vcg.lisp
                      ; on this directory
>(load "fsrch.lisp")
>(add-fsrch)

The last command creates two files, fsrch.context and fsrch.vcs.  The
first file contains the FORTRAN code and the input and output
conditions.  The second file contains the verification condtions that
must be proved to know that the code satisfied the input and output
conditions.

To check the verification conditions, procede to:

>(note-lib FORTRAN)
>(load "fsrch.vcs")
>(do-events vcs)

If no errors or failures are reported, the vcs will have been proved.

The library pair FORTRAN.LIB and FORTRAN.LISP is created from the
events in xxxs.fortran.  This library is used both by the fortran-vcg
during the verification condition generation process and as the
starting point from which verification conditions are to be proved.
