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

Re: LISP code for ground evaluation?

Hi Ajay,

The pvs-lisp-theory command generates a foo.lisp file corresponding to the
foo theory, the function you want will be in there.

Regards,
Sam

> Hello,
> 
> 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.
> 
> Thanks,