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

[PVS-Help] problem with theory interpretations in PVS



Hi,

PVS is not generating proof obligations when using theory interpretations.
My theories typecheck correctly, but PVS complains about an uninterpreted type "presentation_widget" in my specification. That type is interpreted as far as I can tell. Probably I'm doing something silly somewhere, but have no clue at the moment.

The PVS dump file of the PVS theories can be found at the following link:
http://www.eecs.qmul.ac.uk/~masci/PVS/infusion_pump_refinement.dump

* Type "presentation_widget" is declared and interpreted in "bbraun_types_and_constants.pvs"
* The axioms are in "reference_model_th.pvs"
* Theory interpretation is used in "refined_model_th.pvs"

PVS generates the warnings when typechecking "refined_model_th.pvs".

Here's what I get:
Warnings for theory refined_model_th
Axiom R1 is not a TCC because 'presentation_widget' is not interpreted
Axiom R2 is not a TCC because 'presentation_widget' is not interpreted
etc...

I'm using PVS 5.0 with the Allegro Lisp Binaries.
My OS is Linux (Ubuntu 12.04).

Many thanks for any help.

Paolo