perm filename VERIFY.HLP[1,3]1 blob sn#255498 filedate 1976-12-31 generic text, type C, neo UTF8
C00001 00001
C00002 00002	HELP
C00015 ENDMK
"This program is designed to be used as a tool for verification
of properties of PASCAL programs presented to it, along with
lemmas about those programs.  The most commonly used upper level
command is PARSE.  Type (HELP WHAT) for a list of help commands.
For help on topic X, assuming help data exists, type (HELP X)."

"HELP messages are available for the following:

"The BUG feature is provided to help verifier hackers make changes
to syntax, semantics, etc.  There are two user commands,
(SETBUG <number>) and (RESETBUG <number>), which set and then reset
the bug with the appropriate number.  See MEMO[VCG,RAK] to see which
bugs currently exist and what they do."

"The DEDUCE instruction is designed to assist checking out the
provers in the verifier.  It operates at the highest level like
PARSE; i.e. (DEDUCE) will expect input from the terminal and
(DEDUCE <file>) looks for <file> (HELP PARSE) will tell you about
file formats.  DEDUCE expects a single basis expression terminated
with a ';.'(note that there is no keyword at the start and that both
the semicolon and period, in that order, must be at the end). It will
process this into internal format, call INFER, and print out the
result on the terminal.  If BUG#4 is set, it will also print out the
internal format being passed to INFER."

"The call (DELETEVCS names) deletes the VCs for names, if any are
present, i.e. (DELETEVCS FOO BAZ).   Note that parsing another
procedure with the same name causes the old VCs with that name to be
replaced, so DELETEVCS may not be necessary except when there are
free storage problems."

"Documentation on the verifier or portions thereof exists on the
following files (at least):
MEMO[VCG,RAK] about the parser, Pascal, etc.
SSEM[VCG,RAK] --page 2 explains the structure of the symbol table
SYNTAX.N[VER,WLS]--rulefile syntax, internal tree structure

"The command (INTEGERS) tells the verifier that all the numbers it
will be dealing with henceforth in this session are integers or 
subsets (not reals).  This may permit some deductions that are not
valid for general real arithmetic, and thus facilitates integer

"(LIMERICK) prints out a randomly chosen and invariably tasteless
limerick.   You are adivsed to hide your channel before using the
limerick generator.   Limericks may also be automatically generated
during simplification; see (SETLIMERICK)"

"Although this is primarily a program verifier, it exists in a
LISP 1.6 environment.  This means that the general facilities of
such LISP are available.  Some that may be of interest are (GCGAG T),
which causes a printout every time a garbage collection takes place.
This may help indicate the need for running in a larger core image.
It can be turned off by (GCGAG NIL).  Also, (GCTIME) prints out
the processor time thus far spent in garbage collection."

"In manual mode, type any of the following:
↓     : Prove formula without interactive guidance.
↑     : Leave formula as is; back up and continue.
↑↑    : Leave formula as is; back up to top level.
?FACTS: Print out facts known in this context.
( <toplevel command to VERIFY> )
      : Execute the command, then continue the proof.  For example,
	in the middle of a proof you can add a new rule as in


	The rule is added and the proof continues.  Hopefully no
	VERIFY command can cause problems, but to avoid confusion,
	INFER does not allow you to (SIMPLIFY) or (DEDUCE).

<rulename> ( <list of expressions> ) .
      : Apply the inference rule with name <rulename>.   The 
	( <list of expressions> ) is optional; if it appears, the
	expressions are used to instantiate those free variables 
	specified in the definition of the rule.  For instance, given

		R1(Y): INFER P(X) FROM Q(X,Y);

	then if you type R1(A). Y is instantiated to A.  If you type 
	R1. then the pattern matcher will try to find an appropriate 
	instantiation for Y.  
	NOTE: a period must always come at the end."
"The command (PARSE) accepts input from the teletype. (PARSE X)
will try to take input from the file X.  Here are some examples
for taking files with two word names and from another directory
(here p,pn is programmer,project): (PARSE (X.Y)), (PARSE (P,PN)X),
and (PARSE (P,PN)(X.Y))  .
The parser calls the verification condition generator, but does
not do simplification.  For this, the command SIMPLIFY must be
used. The syntactic scan and semantic routines should NEVER
bomb out, no matter what string you give them.  If they do,
send a note to RAK and SAVE the program!!!"

"The command (PREVIOUS <positive integer>) has meaning when a
syntax scan finds a syntax error.  It will print out as many
tokens preceding the syntax error as it is asked (if there are
that many).  (PREVIOUS 10) is called in the errorhandling.  As
the number of tokens requested increases, time to find them can
go up alarmingly. After an error and before parsing something
else, previous may be called as many times as desired."

"The command PRINTVC is used to output unsimplified verfication
conditions.  (PRINTVC) prints out all of these on the
terminal.  (PRINTVC X) prints out all of the VC's for procedure
X.  (PRINTVC X 3) prints the third VC for procedure X.
(PRINTVC (F)) prints out all VC's to file F, which is replaced
if it was previously present.  (PRINTVC (F) X) prints out all
VC's for procedure X on file F.
The outer block of a program is currently called MAIN. It will
remove VC's for a procedure named MAIN, if one is present!"

"(RESIMPLIFY) sends the most-recently simplified formula back
through the prover for (hopefully) further simplification."

"(SETAUTO) is the default mode for the prover.   It is non-interactive.
The alternative mode of proof is (SETMANUAL)"

"(SETLIMERICK) turns on the automatic limerick generator.   After the
first eight CPU seconds of simplification, a randomly chosen limerick
in distinctly questionable taste is printed out.   Further limericks
are printed out at exponentially increasing intervals, i.e. 16 CPU secs,
32 secs, 64 secs, etc.    (UNSETLIMERICK) turns off the generator."

"(SETMANUAL) is the interactive mode of proof.   The default mode is
(SETAUTO).   In manual mode, you are only asked for guidance if
the prover is unable to prove an atomic formula using everything
at its disposal except inference rules.  The possible commands in
manual mode can be seen by typing ? in manual mode or (HELP MANUAL)"

"The command (SETGOALDEPTH <integer>) controls how deep inference
rule applications are made in attempting to prove something.  
The default is 5.  If the verifier does not seem to be proving 
a complex fact for which adequate axioms are available, increasing
GOALDEPTH may help (generally at a considerable increase in 
execution time)."

"The command SIMPLIFY is used to call the simplifier and output
simplified verification conditions.  The procedure and output
file specifications are the same as for PRINTVC.  Use
(HELP PRINTVC) to see these conventions."

"The command (TRACEPROOF) prints out trace information keeping
it to a mininum. It presently prints out the known facts
(antecedent) only when a new context is entered.   Other than that,
it just prints out the atomic formulas to be proved and why they
are proved or rejected.   (UNTRACEPROOF) turns the tracer off."

"(UNSETLIMERICK) turns off the limerick generator.   See (SETLIMERICK)"

"(UNTRACEPROOF) turns off the printing of trace information during
simplification.  (HELP TRACEPROOF) for details on trace routine"