[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
[PVS-Help] Re: problem with theory interpretations in PVS
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
PVS-5.0, on the other hand, is still not generating proof obligations.
Not sure whether this is a bug.
On 31/10/12 10:25, paolo masci wrote:
PVS is not generating proof obligations when using theory
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.