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

[PVS-Help] Re: problem with theory interpretations in PVS



Hi,

With PVS-4.2 I managed to figured out the problem: I had to provide an interpretation for all uninterpreted terms *in the axioms* in order to correctly generate proof obligations -- the warnings provided by PVS-4.2 made this crystal clear.

PVS-4.2 is generating my proof obligations correctly now with a revised theory interpretation.

PVS-5.0, on the other hand, is still not generating proof obligations. Not sure whether this is a bug.

Paolo


On 31/10/12 10:25, paolo masci wrote:
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