[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
Re: LISP code for ground evaluation?
The pvs-lisp-theory command generates a foo.lisp file corresponding to the
foo theory, the function you want will be in there.
> 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.