[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
Question about typecheck-formula
Hello,
I am trying to incorporate PVS as a back-end into our Java verification tool.
To do that, I am starting PVS in batch mode and connect PVS via a socket
connection to our front-end. An emacs lisp programs receives commands from the
front-end and invokes the appropriate PVS function.
To typecheck formulas, I am using the lisp function typecheck-formula, which
works fine for type-correct formulas. However, if a formula contains a type
error, typecheck-formula prints out an error message but does not terminate.
Does anybody have experience in applying this function?
Best regards,
Peter
--
_/_/_/_/_/_/_/_/_/_/_/_/_/_/_/_/_/_/_/_/_/_/_/_/_/_/_/_/_/_/_/_/_/
_/ Peter Mueller _/
_/ Fernuniversitaet Hagen, Lehrgebiet Praktische Informatik V _/
_/ 58084 Hagen, Feithstr. 142, Raum 1.F13 _/
_/ _/
_/ Tel: 02331-987 4870 _/
_/ Fax: 02331-987 4487 _/
_/ E-Mail: peter.mueller@fernuni-hagen.de _/
_/ WWW: www.informatik.fernuni-hagen.de/pi5/mueller _/
_/_/_/_/_/_/_/_/_/_/_/_/_/_/_/_/_/_/_/_/_/_/_/_/_/_/_/_/_/_/_/_/_/