perm filename VERIFY[3,2]1 blob
sn#207088 filedate 1976-03-24 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
the assertions. The verifier can do some simplifications on its own
(over the integers and the propositional calculus), and also understands
the basic properties of arrays, pointers, functions, procedures, etc.
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 user may interactively interact with the verifier: for instance
the user may at any time add new rules, delete old ones, print out
out partially-simplified verification conditions, etc.
The system is presently being completely reprogrammed. The stable
version is VERIFY, the newest version is VERIFY.NEW. Documentation
on the verifier is on MANUAL[SYS,DCO], a pox version ready for xspooling
is on MANUAL.XGP[SYS,DCO]. This manual only details the differences
between VERIFY and its predecessor WEAK. A new manual is being written.
Help on using the verifier may be obtained from DCO (Derek Oppen).