[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
[PVS-Help] problem with theory interpretations in PVS
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:
* Type "presentation_widget" is declared and interpreted in
* 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
I'm using PVS 5.0 with the Allegro Lisp Binaries.
My OS is Linux (Ubuntu 12.04).
Many thanks for any help.