COMMENT ⊗   VALID 00002 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002	
C00004 ENDMK
C⊗;

	VERIFY is an interactive verifier for Pascal programs.  It accepts
as input Pascal programs containing assertions about what the program is
supposed to do and tries to verify that the program is consistent with
these assertions.  The verifier has a built-in simplifier which is a
complete decision procedure for rationals, arrays, records, list structure
and uninterpreted function symbols under their usual functions and
predicates.  The user can augment the proof capabilities of the verifier
by giving it additional replacement rules (e.g. REPLACE F(X) BY G(X) ) and
rules of inference (e.g. INFER P(X) FROM Q(X) ∧ R(X) ).

        The current version of the system is VERIFY.  Documentation on the
verifier is on the directories [MAN,VER] and [DOC,VER].  The documentation
is incomplete and is being rewritten.  TOPLEV.XGP[MAN,VER] is an XGP format
set of syntax charts for the commands the verifier accepts.  The syntax
of programs and lemmas is in PAS1.XGP[DOC,VER].  An explanation of syntax
errors emitted by the parser is in ERRORS.MAN[DOC,VER].

	Help on using the verifier may be obtained from DCO (Derek Oppen).
If he's not around, do a FIND PV and try anyone who has a PV enclosed
in the little brackets when it prints out.