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

Question about typecheck-formula


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 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        _/