PORTING m-EVES TO COMMON LISP

Authors
  1. Pase, B.
  2. Kromodimoeljo, S.
  3. Summerskill, K.
Corporate Authors
Sharp (I P) Associates Ltd, Ottawa ONT (CAN);Chief of Research and Development, Ottawa ONT (CAN)
Abstract
m-EVES is a program verification system developed by I.P. Sharp Associates Limited with funding from the Canadian Department of National Defence. m-EVES supports the formal development of mathematical theories and programs written in the m-Verdi language. The main component of the system consists of an interactive theorem prover and an m-ECL interface. A user develops a theory or program interactively by adding declarations to the theorem prover database and directing the theorem prover to perform proofs. The user may also undo declarations, print the status of the database, freeze the state of the database into a file, and thaw the state of the database from a file. The user interacts with m-EVES by using m-ECL (the m-EVES Command Language), which consists of m-Verdi declarations augmented with theorem prover heuristic information, commands to direct the theorem prover to perform proofs, and commands to perform various database operations.
Report Number
FR-89-5437-04 — Final Report
Date of publication
15 Mar 1989
Number of Pages
17
DSTKIM No
90-01126
CANDIS No
63397
Format(s):
Hardcopy;Originator's fiche received by DSIS

Permanent link

Document 1 of 1

Date modified: