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 system is presently being completely reprogrammed.  The old
version is VERIFY, the newest version is VERIFY.NEW.  Documentation on the
verifier is on MANUAL[MAN,DCO], a pox version ready for xspooling is on
MANUAL.XGP[MAN,DCO].  The manual is incomplete and is being rewritten.  An
XGP format listing of the syntax accepted is 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).