Three of the *.events files in this directory were generated by our Fortran verification condition generator (vcg). The algorithms, specifications, and invariants are included at the end of these *.events files. `isqrt.events' is a Newton-style integer square root algorithm. `mjrty.events' is our majority vote algorithm. `fsrch.events' is a version of our fast string algorithm. The file `fortran.events' is used both in the verification condition generation process, and in the process of proving those conditions. Also this directory is our FORTRAN verification condition generator, whose basic principles of operation are described in gory detail in our article `A Verification Condition Generator for FORTRAN' by R. S. Boyer and J S. Moore in the book `The Correctness Problem in Computer Science', eds. R. S. Boyer and J S. Moore, Academic Press, 1981. The vcg source code, in the file `fortran-vcg.lsp', is documented only by (a) the aforementioned article, (b) several pages of comments in file fortran-vcg.lsp itself, (c) this README file, and (d) the other *.lsp files on this directory, which are examples for processing by the vcg. We offer this vcg Lisp source code to the public for the curious, who may wish to see how a c. 1980 vcg works. As usual, no warranty, etc. The vcg program is written in Common Lisp, and is intended to be run from within Nqthm-1992, the Boyer-Moore prover, which we assume has already been installed. Here are the basic operating instructions for the vcg. 1. From within Nqthm-1992, one time only, while connected to this subdirectory `fortran-vcg' one should first (load "fortran-vcg.lsp") (compile-file "fortran-vcg.lsp") 2. From within Nqthm-1992, one time only, while connected to this subdirectory, one should (load "fortran.events") which will create the library file `fortran', i.e., files `fortran.lib' and `fortran.lisp', from the events in `fortran.events'. (Because fortran.events is one of the standard Nqthm-1992 example files, this library will also be created in the running of those examples.) This fortran library is used both by the vcg and as the starting point from which verification conditions (vcs) are to be proved. 3. To process particular examples with the vcg, from within Nqthm-1992, first execute, while connected to this subdirectory, (load "fortran-vcg") (note-lib "fortran") There are three example files for generating FORTRAN vcs on this directory: isqrt.lsp An integer square root function. mjrty.lsp A linear time majority voter. fsrch.lsp A fast string searching algorithm. To test the system on `fsrch.lsp', for example, one then executes (load "fsrch.lsp") (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 conditions that must be proved to show that the code satisfies the input and output conditions. To check the verification conditions, proceed, within Nqthm-1992, to (load "fortran-vcg") (note-lib "fortran") (load "fsrch.vcs") (do-events vcs) If no errors or failures are reported, then the vcs will have been proved, and hence, we believe, the FORTRAN code satisfies its specification. It is *very important* to understand that the vcg generates the text of the verified FORTRAN code, not the user!! We have no FORTRAN parser!! Instead, the user provides Lisp-like input, which is quite reminiscent of the FORTRAN code to be generated, and which the vcg processes with extreme care. The vcg prints, from what the user has provided, the actual FORTRAN code, which will be found in the *.context files produced. Real tests (blush) of the verified code, with the bsd Fortran processor f77, are given in the the files *.f, which contain instructions for their own execution. The file fsrch.f illustrates the instantiation of a global parameter, ASIZE& in the file fsrch.context, with a specific value, i.e., 128. The Fortran in the *.f files was extracted from the corresponding *.context files. The resulting vcs from the three examples provided can be checked under Nqthm-1992, with the Nqthm-1992 function DO-EVENTS, but not under the more draconian function PROVE-FILE because of the presence of FORTRAN-COMMENT forms, which macro expand into axiomatic no-ops. DO-EVENTS handles the macro expansion happily, but PROVE-FILE will have none of it. See the files nqthm-1992/examples/fortran-vcg/*.events for an illustration of the simple transformation necessary to run the vcs under PROVE-FILE. It is those *.events files that are officially part of the Nqthm-1992 examples distribution. The *.lsp files we provide here are unannounced freebies for the curious. The reason we have named some files *.lsp rather than *.lisp on this directory is only to protect those files from being deleted by the "make clean-giant-examples" command, which deletes all *.lisp files from subdirectories of the examples directory. The easiest way, under unix, assuming that nqthm-1992 is in your executable path, to run this system is simply to execute, when connected to this subdirectory, make all which loads the file `all.lsp', which in turn does all the loading and compiling necessary to run the vcg and the prover on the three example files provided.