[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

LISP code for ground evaluation?


Is it possible to have PVS generated stand-alone LISP code corresponding 
to the executable version of a function in a theory?  That is, code that 
would produce the same results as M-x pvs-ground-evaluator does in the 
PVS shell.  I am working on a  project which aims to use PVS to verify 
some critical portions of code for a prototype.