perm filename VERIFY[3,2]8 blob
sn#391424 filedate 1978-10-29 generic text, type C, neo UTF8
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] to find other members of the
verification group.