The NASALib also provides a collection of scripts that automates several tasks.
proveit- Runs PVS in batch modeprovethem- Runsproveiton several librariespvsio- Command-line utility to run the PVSio ground evaluator.prove-all- Runsproveiton each library in the NASALib by wrappingprovethemin order to provide a specific kind of run.cleanbin-all- Clean.pvscontextand binary files from PVS libraries.find-all- Searches strings matching a given regular expressions in PVS libraries.dependencygraph- Generates a library dependency graph for libraries in the current directory.dependency-all- Generates the dependency graphs for the PVS libraries in the current folder.
Runs PVS in batch mode
proveit [ <option> ... ] [ <file>[.pvs] | [<ctxt>]@<thf1>,..,<thfn> ... | <dir> ]where <thfi> has the form <th>[.<f1>:..:<fm>]
Prove all theories in the input files, e.g.,
- To prove all theories imported in
<dir>/top.pvs, use
$ proveit <dir>- To prove all theories in
<file>.pvs, use
$ proveit <file>.pvs- To prove all theories in
<file>.pvsand their dependencies, use
$ proveit -a <file>.pvsIn the more general form, a context, a list of theories, and a list of formulas are specified using the syntax <[ctxt]@thf1,..,thfn>, where <ctxt> is a directory and each <thfi> has the form <th[.f1:..:fm]> with <th> being a theory and <f1:..:fn> a list of formulas in <th>.
Only formulas specified this way are proven by PVS.
In this case, the proof status is saved in <th.f1:..:fm>.summary in <ctxt>.
For example, to prove formulas <f1> and <f2> in theory <theory> in the current context, type:
$ proveit @<theory>.<f1>:<f2>Note that, when the target is a directory (as in the first example in the Typical Usage section), all the files in its pvsbin subfolder are overwritten.
Options are processed in the order they appear. One letter options can be combined.
| Option | Description |
|---|---|
-a | --all |
equivalent to -ciq |
--auto-fix [<num>] |
try sibling proofs on unfinished branches (<num> is the maximum acceptable distance between the current branch and the sibling which proof is to be tried; default value is 2) |
-c | --clean |
remove .pvscontext and binary files in the pvsbin folder before proving |
-C | --clean-only |
just remove .pvscontext and binary files in the pvsbin folder (do not typecheck nor prove) |
--clean-all |
just remove .pvscontext and all files in the pvsbin folder (do not typecheck nor prove) |
-d | --dir <dir> |
use <dir> as default directory of summary files |
--dependencies |
compute theory dependencies and save them in pvsbin/<file>.dep |
--default-script <proof script> |
default ProofLite script to be tried on unfinished branches |
--disable <o1,..,on> |
disable external oracles o1,...,on |
--disable-oracles |
disable any external oracle |
--enable <o1,..,on> |
enable external oracles o1,..,on. Overwrite --disable |
.<ext> |
use <ext> as default extension of summary files |
-f | --force |
force proof reruns (default) |
~f | --no-force |
do not force proof reruns |
-h | --help |
print help message |
-i | --importchain |
prove chain of imported theories (set --no-scripts) |
~i | --no-importchain |
do not prove chain of imported theories (default) |
--lisp <lisp> |
specify lisp version; <lisp> is one of allegro, cmulisp |
-l | --log |
log all information generated by PVS in <outfile>.log |
~l | --no-log |
don't log PVS information (default) |
-o | --out <outfile> |
save the proof status summary in <outfile>. |
-p | --prelude-ext <p1,..,pn> |
load prelude extensions p1,..,pn |
~p | --no-prelude-ext |
don't load any prelude extension |
-q | --quiet |
print only untried and unfinished proofs per theory, and grand total |
-s | --scripts |
install ProofLite scripts (default) |
~s | --no-scripts |
don't install ProofLite scripts |
--tex |
generate LaTeX proof files in directory pvstex |
--no-tex |
don't generate LaTeX proof files (default) |
--txt |
generate text proof files in directory pvstxt |
--no-txt |
don't generate text proof files (default) |
-t | --top <topfile> |
use <topfile>.pvs instead of top.pvs when the input is a directory |
--timeout <secs> |
timeout in seconds for each proof |
--traces |
include proof traces in log file |
--no-traces |
don't include proof traces in log file (default) |
-T | --typecheck-only |
typecheck but do not prove the theory |
-v | --verbose |
print proof status information per theory and grand total (default) |
--version |
print version information and exit |
Runs proveit on a collection of libraries.
provethem [--help | <option> ...] <file>File <file> must contain an ordered list of libraries to be processed by proveit.
If <file> is not provided, the file name all-theories is assumed.
Each line in <file> must have the form
<lib> [: <proveit params>]
where <lib> is a directory name and <proveit params> are parameters to proveit.
If <lib> is empty, options apply to all libraries thenceforth.
Output is saved in a text file whose default name has the form <file><postfix>.grandtotals.
The <postfix> depends on the options --do, --but, --from, --to, --after, and --before given to the script.
A different name can be specified using the option --out.
Unless the option --out is explicitly use, an output file is not created when the options --clean-all, --clean-bin, --execute or --dry-run are given.
| Option | Description |
|---|---|
--addpath |
add current directory to PVS_LIBRARY_PATH (default when --clearpath) |
--after=<dir> |
prove all libraries after <dir>, exclusive |
--before=<dir> |
prove all libraries before <dir>, exclusive |
--but=<dir1>,..,<dirn> |
do not process libraries <dir1>,...,<dirn> |
--no-color |
do not use colors |
--clean-only |
remove .pvscontext and binary files in the pvsbin folder but do not prove the libraries |
--clean-all |
remove .pvscontext and all files in the pvsbin folder but do not prove the libraries |
--clearpath |
clear PVS_LIBRARY_PATH |
--dir <dir> |
use <dir> as default directory of summary files |
--do=<dir1>,..,<dirn> |
process libraries <dir1>,...,<dirn> |
--disable <o1,...on> |
disable external oracles o1,...,on |
--disable-oracles |
disable any external oracle |
--enable <o1,..,on> |
enable external oracles o1,...,on. Overwrite --disable |
--ext <ext> |
use <ext> as default extension of summary files |
--execute <command> |
execute Unix <command> on all libraries; Command may refer to %DIR% and %FILE% |
--force |
force provethem to go even if there is a proveit error |
--from=<dir> |
prove all libraries from <dir>, inclusive |
--lisp <lisp> |
lisp image to be used; <lisp> can be allegro, cmulisp, or sbcl |
--log |
log all information generated by PVS in <file>.log |
--out <outfile> |
save output to <outfile> |
--test |
process <file> but do not call proveit |
--to=<dir> |
prove all libraries to <dir>, inclusive |
--top <th> |
use <th>.pvs instead of top.pvs as the top theory |
--typecheck-only |
typecheck but do not prove the libraries |
--verbose |
print summary information for all theories |
--version |
print version information and exit |
Command-line utility to run the PVSio ground evaluator. PVSio is a PVS package that extends the ground evaluator with a predefined library of imperative programming language features such as side effects, unbounded loops, input/output operations, floating point arithmetic, exception handling, pretty printing, and parsing. The PVSio input/output library is implemented via semantic attachments.
$ pvsio <options> [<pvsfile>][@<theory>[:[<function> [<arguments>]]]]| Option | Description |
|---|---|
-h | --help |
Print help message |
-p | --packages <P1>,..,<Pn> |
Load packages (prelude libraries) <P1>,..,<Pn> |
-promptin <string> |
Change prompt <PVSio> to <string> |
-promptout <string> |
Change prompt ==>~% to <string> |
-t | --tccs |
Generate TCCs |
-T | --timing |
Print timing information for each evaluation |
-v | --version |
Print PVSio version |
-V | --verbose |
Print type checking information |
-l | --lisp allegro|cmulisp|sbclisp |
Specify a particular PVS binary to execute PVSio. Use this option only if you know what you are doing. |
- Load PVS file
pvsfile.pvsand start PVSio read-and-eval loop
$ pvsio <pvsfile.pvs>- Load PVS theory
<theory>from file<theory>.pvsand start PVSio read-and-eval loop
$ pvsio @<theory>- Load PVS theory
<theory>from file<theory>.pvsand ground evaluate functionmain
$ pvsio @<theory>:- Load PVS theory
<theory>from file<theory>.pvsand ground evaluate function applicationf(a1,...,an)
$ pvsio @<theory>:<f> <a1> ... <an>- Load PVS theory
<theory>from file<file>.pvsand ground evaluate function applicationf(a1,...,an)
$ pvsio <file>@<theory>:<f> <a1> ... <an>Runs proveit on each library in the NASALib by wrapping provethem in order to provide a specific kind of run.
By default, it removes .pvscontext and the binary files from the pvsbin folder in each library directory, replaces the PVS library path by the current directory, and runs proveit as indicated by the nasalib.all file.
As a side effect, it generates the dependency and .tptp files as needed by each library.
To supersede this particular configuration, the same options accepted by provethem can be used on this script.
prove-all <options>Clean .pvscontext and binary files from PVS libraries.
By default, it iterates over all the libraries which are reachable from every directory mentioned in the PVS_LIBRARY_PATH environment variable.
A library is considered reachable in a given directory <dir> if it is one of its direct subfolders and:
- there is a text file named
all-theoriesin<dir>and the library is mentioned there or - there is no such a file in
<dir>.
The scope of application of cleanbin-all can be restricted using the options --after, --before, --but, --do, --from, and --to detailed below.
The order implicitly referred to by all these options is the one induced by the applicable all-theories file or the default order imposed by the operating system, when no all-theories file exists in the directory.
cleanbin-all <options>| Option | Description |
|---|---|
--bin |
remove .pvscontext and binary files (default). |
--all |
remove .pvscontext and all files in the pvsbin folders. |
--clearpath |
clean the libraries in the current path only |
--addpath |
clean over PVS_LIBRARY_PATH and the current path |
--after=<dir> |
prove all libraries after <dir>, exclusive |
--before=<dir> |
prove all libraries before <dir>, exclusive |
--but=<dir1>,..,<dirn> |
do not process libraries <dir1>,...,<dirn> |
--do=<dir1>,..,<dirn> |
process libraries <dir1>,...,<dirn> |
--from=<dir> |
prove all libraries from <dir>, inclusive. |
--to=<dir> |
prove all libraries to <dir>, inclusive. |
-h | --help |
print help message |
--version |
print version information and exit |
Searches strings matching a given regular expressions in PVS libraries.
find-all [--help | <option>* ] <regexpr>By default, it finds in all the libraries which are reachable from the current directory.
A library is considered reachable in a given directory <dir> if it is one of its direct subfolders and there is a text file named all-theories in <dir> and the library is mentioned there.
The scope of application of find-all can be restricted using the options --after, --before, --but, --do, --from, and --to detailed below.
The order implicitly referred to by all these options is the one induced by the applicable all-theories file.
| Option | Description |
|---|---|
--pvs |
find in .pvs files (default) |
--prf |
find in .prf files |
--strategies |
find in pvs-strategies files |
--attachment |
find in pvs-attachment files |
--after=<dir> |
find in all libraries after <dir>, exclusive |
--before=<dir> |
find in all libraries before <dir>, exclusive |
--but=<dir1>,..,<dirn> |
exclude libraries <dir1>,...,<dirn> |
--do=<dir1>,..,<dirn> |
find in libraries <dir1>,...,<dirn> |
--from=<dir> |
find in libraries from <dir>, inclusive |
--to=<dir> |
find in libraries up to <dir>, inclusive |
--help |
print help message |
Generates a library dependency graph for libraries in the current directory.
dependencygraph [<option> ...] [<file>]File <file> contains the list of libraries to be processed.
| Option | Description |
|---|---|
--dot |
generate a DOT file. Do not generate PDF unless --pdf is specified |
--pdf |
generate a PDF file (default) |
--svg |
generate a SVG file |
--title=<string> |
use <string> as the title of the graph |
--out=<outfile> |
use <outfile> as name of the output file |
The scope of the visited libraries can be controlled with the following options
| Option | Description |
|---|---|
--do=<dir1>,..,<dirn> |
process libraries <dir1>,...,<dirn> |
--but=<dir1>,..,<dirn> |
do not process libraries <dir1>,...,<dirn> |
--after=<dir> |
process all libraries after <dir>, exclusive |
--from=<dir> |
process all libraries from <dir>, inclusive |
--before=<dir> |
process all libraries before <dir>, exclusive |
--to=<dir> |
process all libraries to <dir>, inclusive |
--reach-from=<lib>@<th> |
print (only) every reachable theory from <lib> |
--centered-in=<lib> |
show only elements related directly to <lib> |
--closure=[lib|theory] |
automatically grows the scope in order to: (lib) include every library reachable from theories in it; or (theory) zoom into those theories. |
| Option | Description |
|---|---|
--top=<topfile> |
specify name of the top file directory (default: "top") |
--zoom=<dir1>,...,<dirn> |
zoom into libraries <dir1>,...,<dirn> |
| Option | Description |
|---|---|
--full-path |
print library full paths (short paths are shown by default) |
--show-top |
show top file in the graph (not shown by default) |
--splines=<mode> |
control the way in which edges are drawn. For details, see Vizgraph documentation |
--rankdir=<mode> |
control the direction in which nodes are displayed |
--collection-label="<collection>=<label>" |
Replace collection names (folder of path, according to the full-path parameter) with user provided labels. This parameter can be used several times: once for each collection to be relabeled |
| Option | Description |
|---|---|
--force |
force regeneration of .dep files |
--help |
print help message |
This script builds a dot graph of library dependencies.
If <file> is not provided, the file name all-theories is assumed.
Particular libraries in <file> can be selected using the options: --do, --after, --before, --from, --to. The option --but unselect a list of developments.
If <outfile> is not specified, <file><postfix> is used. The <postfix> depends on library selection option, i.e., --do,--but,--from,--to,--after,--before,--zoom.
DependencyGraph depends on Graphviz's dot utility to produce a pdf or SVG output.
When the option --zoom is used, the specified developments are zoomed such that the each theory in those developments in represented by a node in the dependency graph.
The --reach-from=<lib>@<th> option allows to print only the theories which are reachable from <lib>@<th>.
Note, also, that <lib> will be added to the visible scope if not already part of it.
Additionally, DependencyGraph will zoom into <lib> as if it were mentioned in the --zoom option.
Theories from other libraries are explicitly mentioned in the resulting graph only if they belong to a zoomed library, otherwise only the referenced library is mentioned.
Generates the dependency graphs for the PVS libraries in the current folder.
dependency-all [<option> ...]| Option | Description |
|---|---|
--force |
forces regeneration of .dep files |
--after=<dir> |
find in all libraries after <dir>, exclusive |
--before=<dir> |
find in all libraries before <dir>, exclusive |
--but=<dir1>,..,<dirn> |
exclude libraries <dir1>,...,<dirn> |
--do=<dir1>,..,<dirn> |
find in libraries <dir1>,...,<dirn> |
--from=<dir> |
find in libraries from <dir>, inclusive |
--to=<dir> |
find in libraries up to <dir>, inclusive |
--help |
print help message |
Uses provethem to iterate dependency-graph over all the libraries in the current directory.
As in provethem, the scope of application of dependency-all can be controlled using the options --after, --before, --but, --do, --from, and --to detailed below. The order implicitly referred to by all these options is the one induced by the applicable all-theories file.