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.  A user manual is
available as CSD Report No. CS-79-731.  The system provides on-line
documentation through a help feature.  The file ERRORS.MAN[DOC,VER]
contains explanations of syntax error messages emitted by the parser.